Two Independent Routes to the SingleExp Khovanskii Bound

Three days ago we shipped a constructive Khovanskii reduction for polynomials in (x, eˣ). That route — call it ExpPolyBridge — goes through an embedding ExpPoly → PfaffianFn over SingleExpChain and closes via three explicit resolution paths.

This release ships a second, independent proof of the same SingleExp bound. We call this one path-c. It does not use the ExpPolyBridge embedding. It goes through a polynomial canonicalizer, a multi-poly reconstruction bridge, and a new chain-preserving rewrite constructor in the reduction calculus.

Two routes, one bound, same axiom footprint. The code lives at agent-maestro/machlib.

Why a Second Route

The honest reason: while building the SDR (stepwise-decrease reducer) framework for arbitrary triangular Pfaffian chains, we discovered that the ExpPolyBridge route couldn’t be lifted as a generic recipe. The embedding is specific to the ExpPoly representation; the MultiPoly-over-chain representation is the one the rest of the library uses, and the SDR infrastructure is parametric in it.

So we needed a closure that goes directly through MultiPoly, without detouring through ExpPoly. That is path-c.

The bonus is a stronger statement: the SingleExp SDR plugs into the existing khovanskii_bound_via_sdr capstone, which means the same infrastructure will accept second-chain, third-chain reducers without re-proving the bookkeeping.

The Canonicalizer

polySimplify — MachLib’s pre-existing polynomial simplifier — does not do ring cancellation at the syntactic level. The lex measure that proves strict descent of scaledReduction needs a true degree, not a syntactic upper bound. That gap is what blocked closing the original h_bridge side condition directly.

The fix is a new module, PolynomialCanonical, shipped in seven phases:

Phase A  polyCoeffs : Poly → List Real            (zip-arithmetic recursion)
Phase B  evalCoeffs + polyCoeffs_eval             (semantic faithfulness)
Phase D  ring laws at eval level
         evalCoeffs_listSubR_listAddR_self        ((P + Q) - Q = P)
Phase E  polynomial identity theorem (PIT)
         (∀ x, evalCoeffs L x = 0) → all coeffs = 0
Phase F  polyDerivativeCoeffs + HasDerivAt correspondence
Phase G  polyTrueDegree via nat_least_element     (Mathlib-free well-ordering)
         strict-decrease under derivative
         polyTrueDegreeStrict — distinguishes canonically-constant
         from canonically-zero leading coefficients

Phase E is the technically interesting one. The polynomial identity theorem — if a polynomial vanishes everywhere on the reals, all its coefficients are zero — is a Mathlib one-liner. We don’t have Mathlib in MachLib’s analytic base. So path-c reaches PIT via a Horner reconstruction (polyFromCoeffs), the existing PolynomialRootCount.poly_root_count_bound (roots ≤ degree, already in foundations), and Real.natCast strict-monotonicity to contradict infinite roots in finite degree. The result is PIT proved from ingredients MachLib already had — no new analytic axioms.

The Bridge Theorem

polyTrueDegreeStrict lives on List Real, but the SDR’s lex measure has to descend on MultiPoly. The bridge is a module called MultiPolyReconstruct (~1100 lines), and the load-bearing theorem is

eval_leadingCoeffY_eq_eval_yCoeffsAt_getLast :
  ∀ x, eval (leadingCoeffY p) x = eval (yCoeffsAt p x).getLast _ x

— informally, the leading y-coefficient (as a polynomial in remaining variables) evaluates to the last entry of the per-x y-coefficient list.

This theorem was an axiom in MachLib for exactly two commits (dd9c22e through 9d39b7d) while we got the rest of the chain wired up. It is now a proven theorem by structural induction on p, built on top of three listAddN/SubN/MulN_getLast_eval distributivity lemmas (3-way if-then-else on lengths, with a negation cascade in the subtraction case) plus an exact yCoeffsAt_length_eq (= degreeY + 1).

The bridge is generic over n, then specialized to MultiPoly 1 for the consumer.

The trim Constructor

IsKhovanskiiReducible — the inductive predicate that witnesses a reduction chain — got a new case:

| trim (f g : PfaffianFn) (p' : MultiPoly f.n) (k : Nat)
    (h_eval : ∀ x, f.eval x = (PfaffianFn.mk f.n f.chain p').eval x)
    (h_next : IsKhovanskiiReducible (PfaffianFn.mk f.n f.chain p') g k) :
    IsKhovanskiiReducible f g k

It’s a chain-preserving, Rolle-counter-preserving polynomial swap. The reason we needed it: when polyTrueDegreeStrict (leadingCoeffY_last p) = 0 — canonically-zero leading y-coefficient — the natural rewrite is to drop that y-term. The eval is preserved, the chain is preserved, the formal degree-in-y drops. That’s a real reduction step, but it doesn’t fit step (which derives a new chain) or drop (which lowers f.n).

zero_count_khovanskii_bound and IsKhovanskiiReducible.trans both pick up a new case for trim and discharge it transparently — the zero counts pass through under eval-equality.

The Dispatch + End-to-End Capstone

Two ReduceStep variants — the standard one (singleExp_reduceStep_closed, using scaledReduction) and the canonical-trim one (singleExp_canonicalTrim_step, using dropLeadingY + the trim constructor). A dispatch reducer case-splits on polyTrueDegreeStrict > 0:

singleExp_dispatch_step :
  if polyTrueDegreeStrict (leadingCoeffY_last p) > 0
    then singleExp_reduceStep_closed
    else singleExp_canonicalTrim_step

— the bridge theorem is what makes the else branch’s precondition discharge. The result composes into a SingleExpStepwiseDecreaseReducer, then wraps into a generic PfaffianFn.StepwiseDecreaseReducer via Classical.propDecidable on chain equality. The end-to-end capstone:

theorem singleExp_khovanskii_bound
    (p : MultiPoly 1)
    (sdr_other : PfaffianFn.StepwiseDecreaseReducer)
    (a b : Real) (hab : a < b)
    (terminal_nonzero : …) :
    ∃ N : Nat, ∀ zeros : List Real, zeros.Nodup →
      (∀ z ∈ zeros, a < z ∧ z < b ∧
        (⟨1, SingleExpChain, p⟩ : PfaffianFn).eval z = 0) →
      zeros.length ≤ N

sdr_other is a fallback for non-SingleExp shapes — never invoked at runtime for a SingleExp input, but typed in so the wrapper is total. It also gives the next workstream a place to plug in real reducers for IterExpChain and friends without touching the SingleExp closure.

Axiom Audit

#print axioms singleExp_khovanskii_bound in foundations/AxiomAudit.lean reports 40 axioms total. All 40 are in MachLib’s documented foundations:

No new path-c-specific axioms. The axiom footprint is indistinguishable from the older expPoly_khovanskii_bound (ExpPolyBridge) and PfaffianFn.khovanskii_bound_full (SDR generic) capstones — same documented MachLib foundations.

The strongest individual lemma axiom-wise is the bridge theorem eval_leadingCoeffY_eq_eval_yCoeffsAt_getLast: 10 axioms, pure structural — no HasDerivAt, no rolle, no exp. That’s encouraging: the new infrastructure leans on the algebraic side of the foundations only.

Honest Foundations

The same caveats from the ExpPolyBridge release apply here. MachLib’s analytic base remains axiomatized rather than proven from a smaller core. Path-c does not change that. What path-c does change:

None of those touch the axiomatized analytic base. The “modulo the documented foundations” caveat is unchanged.

Non-Claims

Path-c does not claim:

It is a second, independent constructive proof of the same SingleExp bound, with a more reusable framework underneath.

What’s In The Repo

Headline files build clean with zero sorry. The singleExp_khovanskii_bound import closure does not touch the work-in-progress modules from the prior release.

Why This Matters

The headline isn’t a new theorem. It’s a more reusable proof.

The ExpPolyBridge route gave us the SingleExp bound by routing through a representation specific to (x, eˣ). Path-c gives us the same bound by routing through MultiPoly-over-chain, which is the representation the rest of the library is built on. That means a fourth chain class — say IterExpChain for (x, eˣ, eᵉˣ) — gets a Khovanskii bound by writing one per-chain SDR and plugging into the same wrapper. The bookkeeping is amortized.

There is also a small methodological dividend. The polynomial identity theorem, proved without Mathlib, is the kind of foundational piece we expect to reuse anywhere we need to bridge “vanishes everywhere” to “all coefficients zero.” Phase E is now its own callable lemma.

The next rung on the ladder is a real reducer for a non-SingleExp chain class — that’s the test of whether path-c’s reusability claim survives contact with a second case. The work after that is grounding the analytic base in mathlib, which is still open and still the lever that turns “modulo the documented foundations” into something unconditional.

We’ll write that post when it’s done.

Monogate Research (2026). “Two Independent Routes to the SingleExp Khovanskii Bound.” monogate research blog. https://monogate.org/blog/two-routes-to-the-khovanskii-bound

React