hex

13.7. The Mathlib correspondence🔗

The split between HexRealRoots and HexRealRootsMathlib is a trust and dependency boundary. HexRealRoots performs exact integer and dyadic computation without importing Mathlib. HexRealRootsMathlib interprets the result in Mathlib's language of Polynomial ℝ and real roots. Its abstract Sturm theorem is connected to the executable signed pseudo-remainder chain by the following headline correspondence.

🔗theorem
HexRealRootsMathlib.sturmChain_isSturmChain (p : Hex.ZPoly)
  (hp : 1 ≤ Hex.DensePoly.natDegree p) (hsq : p.SquareFreeRat) :
  Sturm.IsSturmChain (HexRealRootsMathlib.toPolyℝ p.primitivePart)
    (List.map HexRealRootsMathlib.toPolyℝ p.sturmChain.toList)
HexRealRootsMathlib.sturmChain_isSturmChain
  (p : Hex.ZPoly)
  (hp : 1 ≤ Hex.DensePoly.natDegree p)
  (hsq : p.SquareFreeRat) :
  Sturm.IsSturmChain
    (HexRealRootsMathlib.toPolyℝ
      p.primitivePart)
    (List.map HexRealRootsMathlib.toPolyℝ
      p.sturmChain.toList)

The executable Sturm chain is a Sturm chain. For a positive-degree, rationally squarefree p, the real cast of Hex.ZPoly.sturmChain p satisfies all the Sturm.IsSturmChain sign axioms for toPolyℝ (primitivePart p).

Stated at the primitive part: the executable chain's head is primitivePart p (the content is stripped), so an IsSturmChain (toPolyℝ p) … conclusion would have the wrong head; p and its primitive part have the same real roots (roots_toPolyℝ_eq_primitivePart), so the counting consequences are unaffected.

The elaborator runs compiled search only to choose certificate data. It emits the integer polynomial, Sturm chain, and intervals as literals, then applies the replay constructor whose obligations are ordinary Lean propositions.

🔗def
Hex.IsolatedRealRoots.ofCert {p : Hex.ZPoly} {chain : Array Hex.ZPoly}
  {n : ℕ} (iso : Vector (Hex.RealRootIsolation p) n)
  (hsize : Hex.DensePoly.size p ≠ 0)
  (hsf : p.hasSquarefreeSturmChain = true)
  (hcert : Hex.SturmChainCert p chain)
  (hordered : Hex.orderedAdjacent iso.toArray = true)
  (hcomplete :
    Hex.sturmVarNegInf chain - Hex.sturmVarPosInf chain = n) :
  Hex.IsolatedRealRoots (HexPolyZMathlib.toPolynomial p) n
Hex.IsolatedRealRoots.ofCert
  {p : Hex.ZPoly}
  {chain : Array Hex.ZPoly} {n : ℕ}
  (iso :
    Vector (Hex.RealRootIsolation p) n)
  (hsize : Hex.DensePoly.size p ≠ 0)
  (hsf : p.hasSquarefreeSturmChain = true)
  (hcert : Hex.SturmChainCert p chain)
  (hordered :
    Hex.orderedAdjacent iso.toArray =
      true)
  (hcomplete :
    Hex.sturmVarNegInf chain -
        Hex.sturmVarPosInf chain =
      n) :
  Hex.IsolatedRealRoots
    (HexPolyZMathlib.toPolynomial p) n

The replay constructor IsolatedRealRoots.ofCert. The production certificate shape: from the reified polynomial p, a reified Sturm chain chain, and n certified isolations iso (each carrying its interval and a cheap count_one_of_cert witness), assemble the isolation with every remaining obligation a single decide on literals:

  • hsize : p.size ≠ 0 — nonzeroness by a Nat decide;

  • hsf : hasSquarefreeSturmChain p — the squarefree side;

  • hcert : SturmChainCert p chain — the reified chain is p's Sturm chain, validated by coefficient-level checks that kernel-reduce (never a structural Array equality), used for complete;

  • hordered : orderedAdjacent iso.toArray — the O(n) adjacent-pair order check, walked to the all-pairs ordered field by ordered_of_adjacent;

  • hcomplete : sturmVarNegInf chain − sturmVarPosInf chain = n — the −∞/+∞ sign-variation gap, giving complete via rootCount_eq_of_cert.

The kernel replays only the exposed count-check closure against the literal chain; it never rebuilds sturmChain p inside a field.

The emitted top-level term uses Hex.IsolatedRealRoots.ofCertPretty, which changes only the presentation of dyadic endpoints. The kernel checks the chain, each interval count, the total count, and interval ordering; it does not trust the compiled search or the Descartes dispatch. Inputs written as Polynomial ℤ, Polynomial ℚ, or Polynomial ℝ are connected to HexPolyZMathlib.toPolynomial by a checked evaluation equivalence. Repeated-root inputs are isolated through a squarefree core and transported back with the following root-equivalence operation.

🔗def
Hex.IsolatedRealRoots.congrRoots.{u_1, u_2} {R : Type u_1}
  {S : Type u_2} [CommRing R] [Algebra R ℝ] [CommRing S] [Algebra S ℝ]
  {P : R[X]} {Q : S[X]} {n : ℕ}
  (h :
    ∀ (x : ℝ),
      (Polynomial.aeval x) P = 0 ↔ (Polynomial.aeval x) Q = 0) :
  Hex.IsolatedRealRoots P n → Hex.IsolatedRealRoots Q n
Hex.IsolatedRealRoots.congrRoots.{u_1,
    u_2}
  {R : Type u_1} {S : Type u_2}
  [CommRing R] [Algebra R ℝ] [CommRing S]
  [Algebra S ℝ] {P : R[X]} {Q : S[X]}
  {n : ℕ}
  (h :
    ∀ (x : ℝ),
      (Polynomial.aeval x) P = 0 ↔
        (Polynomial.aeval x) Q = 0) :
  Hex.IsolatedRealRoots P n →
    Hex.IsolatedRealRoots Q n

Transport an isolation along a pointwise root equivalence. One lemma, used twice by the elaborator: the squarefree-core step and the user-polynomial step. Heterogeneous in the coefficient ring, since the structure only sees P through aeval x P = 0.

The interval endpoints are presented as reduced rational literals, and the identification of the emitted literals with the isolator's dyadic endpoints is stated over ℝ. This keeps rational normalization, and its Nat.gcd, away from the kernel, which is what makes endpoint extraction a plain rfl even for the refined fractional endpoints above.