Climbing the Exponential Tower

Last month we wrote about a constructive Khovanskii reduction for the single-exponential case — polynomials in (x, eˣ). That post ended on an honest caveat: the finite zero-count was proven modulo an axiomatized analytic base.

Two things have changed since.

The bound is now unconditional and the Khovanskii-citation axiom is gone — the zero-count is derived from Rolle’s theorem, not asserted by citation.
It no longer stops at one exponential. It reaches three.

The result

For the iterated-exponential (Pfaffian) chain

y₀ = eˣ        y₁ = e^{eˣ}        y₂ = e^{e^{eˣ}}

let p be any polynomial in x, y₀, y₁, y₂, and let chain3Fn p be the real function you get by substituting those tower values. The theorem, in Lean:

theorem chain3_khovanskii_bound_unconditional
    (p : MultiPoly 3) (a b : Real) (hab : a < b)
    (hne : ∃ z, a < z ∧ z < b ∧ (chain3Fn p).eval z ≠ 0) :
    ∃ N : Nat, ∀ zeros : List Real, zeros.Nodup →
      (∀ z ∈ zeros, a < z ∧ z < b ∧ (chain3Fn p).eval z = 0) → zeros.length ≤ N

In words: if p is nonzero at even a single interior point of (a, b), then chain3Fn p has only finitely many zeros there. The one hypothesis — nonzero somewhere — is the honest minimum: a function that is identically zero has infinitely many zeros, so no finite bound could exist.

There is no terminal_nonzero side condition. And, most importantly, there is no appeal to the axiom that used to do the heavy lifting.

What “the axiom is gone” means

MachLib does not build real analysis from scratch. It works over an axiomatized real-number interface — the reals with their field and order structure, plus a small number of trusted analytic facts, chief among them Rolle’s theorem and its immediate corollary: a continuously-differentiable function whose derivative has at most N zeros has at most N+1 zeros. Those are standard, load-bearing, and we take them as given.

What we do not take as given is Khovanskii’s bound itself. Earlier Pfaffian work in the library carried an axiom — call it the citation axiom — that simply stated the finite zero-count for Pfaffian functions, on the authority of Khovanskii’s 1991 book. It is real mathematics, but in a formalization it is a promissory note: it asserts the conclusion instead of proving it.

#print axioms chain3_khovanskii_bound_unconditional now lists only the honest interface — rolle, the derivative-based zero-count, the ring/order axioms — plus Lean’s own three (propext, Classical.choice, Quot.sound). No sorryAx. No citation axiom. The bound is counted, not quoted.

How the climb works

The proof is a well-founded recursion that peels the tower one variable at a time. Each step is an integrating-factor / Rolle argument: multiply the function by a nowhere-zero factor so that the derivative of the product is a reduced polynomial in a strictly smaller measure; Rolle then says the original has at most one more zero than the reduct. Recurse until the top exponential is gone, and land on the depth-2 bound — which we had already closed the same honest way.

The subtle part is the measure. A naïve reduction inflates the syntactic degree of the leading coefficient even when the true (semantic) degree drops, so the recursion has to be measured by a canonical, evaluation-invariant degree at every level of nesting. Getting that right — and proving that the one genuinely awkward case (a “phantom” leading term that vanishes on the chain but not syntactically) still descends — is most of the work. The dispatch has four arms: reduce, two kinds of trim, and a base case that hands off to the level below.

The upshot is structural, and it is the point worth making: the depth-2 closure extends to depth-3 by the same argument, applied one level up. Depth-N would look the same again, with one more layer of nesting in the measure. The tower is climbable by induction on its height.

Honest scope — what this is and isn’t

It is a fully machine-checked, unconditional finiteness bound for a specific, important family of transcendental functions — the low tower of iterated real exponentials — resting only on Rolle’s theorem and the real-number axioms.
It is not a new theorem of mathematics. The finiteness is classical (Khovanskii; Wilkie’s o-minimality of the real exponential field). The contribution is the formalization: a proof that counts rather than cites, unconditional, and shown to lift by depth.
The analytic base is still axiomatized. Rolle and the derivative-zero-count are trusted inputs, not proven from an ε-δ construction of the reals. That is a deliberate, clearly-scoped boundary of MachLib, not a hidden gap — you can read exactly what is assumed in #print axioms.
We do not claim depth-N for general N. We claim depth-3, and we claim that the argument is structured to recurse. Turning “structured to recurse” into a single theorem quantified over N is future work.

The code is public in machlib/foundations/MachLib/IterExpDepth3Bound.lean, and the whole arc — the top-level identity, the vehicle/Rolle steps, the canonical measures, the inner-trim, and the final assembly — sits alongside it, each piece #print axioms-clean.

Counting, not quoting. One exponential at a time.

React