# Reproduction — Iterated-exponential Khovanskii finiteness (depth 2)

Machine-checked result `MachLib.ChainExp2NoZeros.chain2_khovanskii_bound_unconditional` in `MachLib.ChainExp2NoZeros` — a proof, not a codegen kernel. Regenerate with `make all`.

> Depth-2 shown here (proof + zero-count witness). Depth-3 is ALSO proven clean (MachLib.IterExpDepth3Bound.chain3_khovanskii_bound_unconditional); the ∀N generalization is in progress (lemma-1 + the reduce seam are done, machine-checked). General-depth PfaffianFunction.zero_bound STILL cites the classical Khovanskii axiom — only depths 1–3 are counted, not quoted.

| stage | artifact | tier |
|---|---|---|
| proof | `MachLib.ChainExp2NoZeros.chain2_khovanskii_bound_unconditional` — ✓ clean (`proof/chain2_khovanskii_bound_unconditional.axioms.txt`) | REPLAY (re-derive: TOOLCHAIN — Lean) |
| simulate | `sim/trace.csv`, `sim/khovanskii_zeros.png` — zeros of (x³−3x)·e^(e^x) on (-2.0,2.0) = 3 = 3 | LOCAL |
| hardware | — (a pure finiteness theorem; the sim is a numerical zero-count witness, not hardware) | NONE |

**The same claim, two ways.** The Lean theorem `MachLib.ChainExp2NoZeros.chain2_khovanskii_bound_unconditional` proves a polynomial in the tower (x, eˣ, e^{eˣ}) that is nonzero at even one interior point has only FINITELY many zeros on (a,b) — the count derived from Rolle's theorem, not cited from Khovanskii; the simulation shows `zeros of (x³−3x)·e^(e^x) on (-2.0,2.0) = 3 = 3` (count stable under 100× grid refinement ⇒ finite; e^(e^x) never vanishes so adds no zeros — consistent with the machine-checked bound); Proved, simulated.