Formalization · iterated exponentials · Lean 4

Constructive Khovanskii in Lean

Khovanskii’s theorem says a function built from iterated exponentials has only finitely many real zeros. We give that counting bound a fully constructive, machine‑checked proof at every depth — an explicit ceiling reduced to a single analytic fact: Rolle’s theorem.

Classical statement Constructive architecture Explicit recurrence Dependency graph Axiom footprint Beyond the exponential

01 — Classical statement

A tower of exponentials has finitely many zeros

Fix a height n and build the iterated‑exponential tower

y₀ = eˣ, y₁ = e^(y₀) = e^(eˣ), \dots, yₖ₊₁ = e^(yₖ).

Let p be an ordinary polynomial in the variable x and the tower variables y₀, …, yₙ₋₁, and evaluate it along the tower:

f(x) = p(x, eˣ, e^(eˣ), \dots).

This is a Pfaffian function: each tower variable satisfies a first‑order differential equation polynomial in the earlier ones (yₖ′ = yₖ·⋯). Khovanskii’s theory of fewnomials (1980) proves that any such f has only finitely many real zeros on an interval, with a bound depending only on the degree of p and the height of the tower. Classically this is a landmark of real‑analytic geometry — but the usual arguments interleave the induction on the chain with analytic and integral‑geometric machinery, and the “explicit” constant is left abstract.

The statement proved here, in a proof assistant, is:

For every height and every polynomial p whose syntactic degrees are bounded by D, the function f above has at most Ndep(m, D) zeros on any interval where it is not identically zero — where Ndep is an explicit closed‑form recurrence in D.

No existence quantifier hides the constant; Ndep is written down in §03. At the base of the tower (a single nested exponential) the ceiling is a concrete number — and now a machine-checked theorem: e^(eˣ) − x·eˣ crosses zero at most 47 times on any interval containing a point where it is nonzero (the ceiling Ndep(0, 1) evaluates to 47, and the count is discharged in the kernel — no floating-point, no external oracle). The finer per-barrier recurrence sharpens this further — x·e^(eˣ) − e^(2x) to at most 71 — though that tighter figure is read off the canonical measure rather than the degree-class ceiling, so it stays a computation rather than a theorem.

02 — Constructive architecture

Everything is Rolle, twice nested

The proof turns zero‑counting into repeated applications of Rolle’s theorem. There is no measure theory, no analytic continuation, no transcendence input — just the ordered real field, the exponential, a differentiation calculus, and Rolle. Two nested inductions carry it:

Within a level — reduce and trim

Suppose the top tower variable genuinely appears in p. A reduce step forms a new polynomial by eliminating the leading power of that top variable — a chain‑total‑derivative, the algebraic shadow of differentiating f. By Rolle, f has at most one more zero than the reduced function. When instead the top variable’s leading coefficient vanishes identically, a trim lowers the top degree at no analytic cost. A measure on the polynomial strictly decreases under both moves, so a well‑founded recursion terminates; the number of reduces it performs is the zero budget for that level.

Down the tower — induction on height

Once the top exponential is eliminated entirely, the problem drops to a tower one shorter, and the bound for that shorter tower — the induction hypothesis — supplies the leaf. The base case is a single nested exponential, proved by the very same reduce/Rolle loop.

The subtlety that makes it close

A flat numeric rank on the measure does not survive the descent. A reduce may raise an exponential’s degree by one, forcing a larger degree budget; but a flat rank is monotone in that budget, so enlarging it fights the very drop the reduce is supposed to buy. The fix is a recursive rank: a level‑indexed budget whose per‑level cap is itself a lower‑depth budget, mirroring the recursive shape of the tower. Each digit of the measure then behaves as its own level index — non‑increasing on its own descent — rather than as a bounded high digit fighting the growth. This is what lifts the chain‑2 argument to arbitrary depth.

03 — Explicit recurrence

The ceiling, written down

The whole bound rests on one level‑indexed budget. With an x‑degree budget B, a level count d, an inner rank r, and a growth budget g:

L(B, 0,   G) = (G+1)(B+1)
L(B, d+1, G) = (G+1)(B+1) + L(B, d, G + (G+1)(B+1))

Φ(B, 0,   r, g) = r
Φ(B, d+1, r, g) = r + L(B, d, g + r + 1)

At the base of the tower (a single nested exponential) the zero count of p(x, eˣ, e^(eˣ)) is exactly Φ read off the degrees. This is the engine; the depth recurrence wraps it.

The depth recurrence

Write budgetMax(m, D) for the largest reduce‑budget of any depth‑m polynomial with degrees ≤ D. Then the ceiling is:

Ndep(0,   D) = Φ(D+2, D, D(D+3) + (D+2), D)

    writing  b = budgetMax(m, D+2):
Ndep(m+1, D) = b + Ndep(m, (D+2) + b)

The first term counts the reduces that peel the top exponential; the second is the bound for the tower one shorter, evaluated at the larger degree those peels can produce. The two terms are kept separate — a leaf added beside the budget, not folded into it — which is what removes the circularity that a single fused constant would create.

The recursive per‑level cap

The cap inside budgetMax is where the recursion lives. It is the same level‑indexed shape as Φ, but with the per‑level weight replaced by a strictly‑lower‑depth budget:

ℓ(κ, 0,   B) = κ(B)
ℓ(κ, d+1, B) = κ(B) + ℓ(κ, d, B + κ(B) + 1)

descentBound(0,   B) = B + 1
descentBound(n+1, B) = ℓ(descentBound(n), B, B)

budgetMax(m, D) is Φ evaluated with κ = descentBound(m+2) as its per‑level cap. One level of the budget per digit of the nested measure — exactly the structure that lets the rank drop thread through the descent.

On the size of the number

Unrolled, Ndep(m, D) is a tower of exponentials of height m. That growth is intrinsic to iterated exponentials, not an artifact of the proof — and the point was never that the number is small. It is that the number is explicit, finite, and machine‑checked, from Rolle alone. At depth two it is a plain numeral (47, 71 above); deeper, it is a closed‑form recurrence rather than a digit one would print.

04 — Dependency graph

What rests on what

Every rung is a mathematical result, and each depends only on the ones above it. Read top to bottom: a single analytic axiom at the summit, the constructive bound at the foot.

axiom Rolle’s theorem The sole analytic input. A zero of the derivative between any two zeros of the function.

lemma Single‑exponential bound A polynomial in x and eˣ has at most (degree + number of reduction steps) real zeros.

lemma Reduce step + well‑founded measure Eliminating the top exponential costs one zero (Rolle) and strictly lowers a terminating measure.

theorem Chain‑2 explicit bound The level‑indexed budget Φ counts the zeros of p(x, eˣ, e^(eˣ)) exactly, from degrees alone.

lemma Recursive descent rank A nested, level‑indexed rank whose per‑level cap is a lower‑depth budget — strictly bounded, and it drops on every reduce.

lemma Degree‑evolution accounting Under reduce and trim, x‑degree never rises and each exponential degree grows by at most one.

theorem One‑level recursion A single well‑founded recursion over one exponential level: reduce, trim, and lift arms, budgeted by Φ with the recursive cap.

theorem Depth induction Induct on the height of the tower. Base: chain‑2. Step: peel the top exponential; the shorter tower supplies the leaf.

headline Constructive Khovanskii bound For every depth and every polynomial, an explicit finite ceiling Ndep(m, D) on the zero count — machine‑checked, from Rolle alone.

05 — Exact axiom footprint

What the proof trusts

The theorem’s complete axiom footprint is 45 axioms — no more, no less. Three are Lean’s logical core. The rest specify the real line as an ordered field with an exponential and a differentiation calculus. Exactly one — Rolle’s theorem — carries the analysis.

Logical core 3

Lean’s three standard axioms — shared by essentially every formal proof.

propextClassical.choiceQuot.sound

The real line — ordered field 30

The carrier type and its field & order structure. Nothing analytic yet.

RealaddRmulRnegRsubRdivRoneRzeroRnatCastadd_assocadd_commadd_zeroadd_negmul_assocmul_commmul_one_axmul_distribmul_invsub_defnatCast_succnatCast_zeroleRltRle_iff_lt_or_eqlt_irrefl_axlt_totallt_trans_axadd_lt_add_leftzero_lt_one_axzero_ne_one_ax

The exponential 2

exp exists and is strictly positive. That is all the tower is built from.

expexp_pos

Differentiation calculus 9

The derivative relation and its rules: sum, difference, product, composition, constant, identity, exp, and uniqueness.

HasDerivAtHasDerivAt_addHasDerivAt_subHasDerivAt_mulHasDerivAt_compHasDerivAt_constHasDerivAt_idHasDerivAt_expHasDerivAt_unique

The analytic engine 1

Rolle’s theorem — between two zeros of a differentiable function lies a zero of its derivative. The single nontrivial analytic input; the only place completeness of the reals does any work.

rolle

Verified absent

No sorry anywhere in the proof or its dependencies. And crucially, no classical zero‑counting axiom: the earlier result gave only “finitely many” with an unnamed bound, and could have leaned on such an axiom — this one does not. Every zero is accounted for by construction.

These real‑analysis axioms are an interface, not an appeal to authority: each is discharged against the standard real numbers in a companion soundness check — see A Model for the Axioms. So the footprint above is genuinely the whole of it: an ordered field, exp, differentiation, and Rolle.

06 — Beyond the exponential

Logarithms and reciprocals, on the same descent

The tower above is exponentials alone. But the reduce/Rolle architecture never depended on which Pfaffian functions the chain is made of — only that each variable satisfies a first‑order differential equation in the earlier ones. Logarithms and reciprocals do too. Carrying the same two nested inductions across a chain that mixes all three closes the general case:

Any function assembled from x, exponentials, logarithms, and reciprocals — the whole class an expression language produces — has finitely many real zeros on any interval where it is not identically zero. Machine‑checked.

Two things make the mixed chain harder than the pure tower, and both are now discharged. A logarithm can lower the top degree under differentiation, so the plain reduce is replaced by a Wronskian against the leading coefficient — an elimination whose leading term provably cancels. A reciprocal makes the naïve chain measure grow instead of shrink; the remedy is to recurse on the top variable’s degree — a bare natural number — rather than on a measure of the whole chain, so a reciprocal level is never descended, and its zeros enter only through the bound for the shorter chain beneath it. This was the one step the classical descent left open; it is now filled in.

The honest footprint of the general case

Two caveats, stated plainly. The mixed bound is qualitative — a finite ceiling exists, without the closed‑form Ndep the pure tower carries. And its analytic footprint is larger than Rolle: the degenerate cases, where two functions in the chain turn out proportional, are retired by the standard theorem that a real‑analytic function has finitely many zeros on a compact interval unless it vanishes identically. The descent itself is still Rolle; the identity theorem enters only to close those degenerate leaves — and the interface gains the logarithm and the reciprocal alongside the exponential. No classical zero‑counting axiom, and no sorry, in either result.

Theorem catalog → Proofs → Tight zeros bound → Machine‑checked source (Lean 4) →