Tower Zero-Counter

One rung up from the single exponential: functions f(x) = p(eˣ, e^{eˣ}) — polynomials in y₀ = eˣ and y₁ = e^{eˣ}. That they have only finitely many zeros is proven, rolle-only, in MachLib. But the explicit constant grows exponentially in the tower degree — climb the presets and watch the actual count barely move while the bound's growth takes off.

Depth 1: no e^{eˣ}. The classic single-exp case — bound is polynomial. Interval [-3, 3]. Amber dots = numerically-found sign changes.

tower degree · D₁ (in y₁ = e^{eˣ})0
inner degree · in y₀ = eˣ1
actual real zeros (numeric)1
PROVEN
Finitely many zeros — machine-checked, no sorry, single analytic axiom rolle.
EXPLICIT CONSTANT — OPEN
Grows exponentially in D₁. The tight value is an open problem; only the shape is proven.

y₀ = eˣ = 2 at x = ln 2 ≈ 0.69. This one is y₁-free — a pure single-exponential (depth 1).

Why the bound explodes up the tower

The constructive proof counts zeros by repeatedly reducing f to a simpler function and adding +1 per step (Rolle). Two facts about those steps — both machine-checked this session — set the growth:

  • The reduce multiplier carries a y₀ = eˣ factor, so each reduce raises the inner (y₀) degree by exactly 1 (degreeY0_chain2Reduce_le).
  • A y₁-degree-dropping trim then switches to a lower coefficient those reduces have already grown — so the per-level work compounds across the D₁ tower levels.

The step-count recurrence S(j+1) ≤ (dₓ+2)·S(j) + c over the tower levels solves to exp(D₁). Contrast the single-exponential case (Khovanskii Counter), whose bound length + Σ deg is merely polynomial. The finiteness was recently lifted to any exponential-type Pfaffian chain — the write-up.