A Constructive Khovanskii Reduction — the SingleExp (eˣ) Case

MachLib’s current foundations capstone is a constructive zero-count bound for functions of the form

f(x) = Σ_{k=0}^d a_k(x) · exp(k·x)

— polynomials in (x, eˣ) — on any open interval (a, b). The bound is finite, explicit, and the framework ships with three resolution paths and a worked Forge-kernel application on top.

The theorem itself is classical — it is the standard Rolle/derivative reduction behind Khovanskii’s fewnomial bounds for exponential polynomials. The contribution here is the Lean formalization, the proof architecture, and the application to a real safety-critical kernel obligation.

This post is the research record for the closure. The code lives at agent-maestro/machlib.

The Reduction

The reduction runs through a Rolle vehicle:

mulNegExpX ep c := f(x) · exp(-c·x)

whose derivative is exp(-c·x) · scaledReduction(ep, c) and which shares zeros with f (since exp > 0). That gives the chain-step inequality

zeros(f) ≤ zeros(scaledReduction f c) + 1

One thing worth flagging because it cost real time: the operator that works is scaledReduction c f := f' - c·f, not the textbook f' - c·yₙ'·f. The textbook variant does not drop degree in single-exp chains. We documented the discovery in the git history; if anyone recognizes the textbook operator from a chain setup where it is the right thing, we’d genuinely like to know what we were missing.

Three Resolution Paths

All three converge on the same bound.

Parametric capstone — expPoly_khovanskii_bound. The user supplies an IsKhovanskiiReducibleExp witness (a chain of step and drop constructors) and gets the explicit numeric bound.

Auto-bound with propagation — expPoly_auto_bound_with_propagation_aux. A strong induction over

length + Σ degreeUpper(polySimplify coeffs)

handles the algebra given a propagation hypothesis.

ODE corner case — expPoly_ode_no_zeros. When f' - c·f ≡ 0 on (a, b), an MVT argument shows f is a pure exponential, hence zero-free. This covers the case the propagation hypothesis can’t.

Three paths, one bound.

A Forge Kernel Closes On Top

The Forge kernel-emission pipeline ships verify obligations as sorry stubs for downstream Lean discharge. One such kernel is butler_volmer/current_density:

i(η) = i₀ · (exp(α_a · F·η/RT) - exp(-α_c · F·η/RT))

— the Butler-Volmer electrode-kinetics rate equation. Domain: battery management systems, fuel cell controllers, corrosion engineering. The Forge verify obligation is butler_volmer_zero_at_zero_overpotential. The clinically meaningful statement is the iff:

current = 0 ↔ overpotential = 0

This is a zero-count obligation. The framework closes it. A BMS or fuel-cell controller observing zero current can now rely on the equilibrium reading because the contradiction direction is proven, not assumed.

The proof lives at foundations/MachLib/Applications/ButlerVolmerKhovanskii.lean and replaces the True placeholder in MachLib/Discovered/butler_volmer.lean.

Honest Foundations

We need to be plain about what is and isn’t done.

MachLib axiomatizes its analytic layer rather than proving it from a smaller base. The closure session added no assumptions beyond that documented base, but the base itself includes:

zero_count_bound_by_deriv   (Rolle zero-counting corollary, N(f) ≤ N(f') + 1)
HasDerivAt + HasDerivAt_unique + the rule axioms
exp_pos, exp_zero
MachLib.Real arithmetic and order

In mathlib every one of those is a theorem. The first one, zero_count_bound_by_deriv, is doing the core analytic work of the reduction. The Khovanskii layer added here is the reduction structure and the explicit-bound bookkeeping on top of it.

Grounding the analytic base in mathlib is open work, not done in this release.

foundations/AxiomAudit.lean makes the full dependency set visible. Run via lake env lean AxiomAudit.lean; it prints #print axioms for every headline theorem. The reader does not have to take our word.

A second honesty note: expPoly_ode_no_zeros does not invoke Classical.choice in its Lean dependency closure. We are not claiming it is constructive in the analyst’s sense — the MVT it rests on is classical in spirit and only escapes the dependency list because the MVT itself is axiomatized here.

Non-Claims

The Khovanskii closure does not claim:

It is a bounded formalization with one named kernel application.

What’s In The Repo

Headline files build clean with zero sorry. The repo contains 3 sorry-warnings in two non-headline modules (MachLib.ForgeTest and MachLib.HighDimensional — work-in-progress queues unrelated to this release). The transitive-import closure of the headline theorems and the audit does not touch either; verified by import walk.

Why This Matters

The constructive Khovanskii reduction is one rung on a longer ladder. The ladder is:

axiomatized analytic base
  -> constructive zero-count framework over poly-in-(x, eˣ)
  -> Forge-kernel verify obligation closures
  -> downstream safety-critical certification evidence

This release moves one rung. The next is grounding the analytic base in mathlib, which converts the modulo-the-base claim into an unconditional one. That work is not done, and we want to be plain about it.

The Butler-Volmer kernel is one application. Other Forge kernels with the same shape — multi-exp pharmacokinetics, control-loop oscillators, corrosion sensors — share the same proof structure, which is part of why the framework was worth building rather than the kernel alone.

Monogate Research (2026). “A Constructive Khovanskii Reduction — the SingleExp (eˣ) Case.” monogate research blog. https://monogate.org/blog/constructive-khovanskii

React