39.7.1. Sturm–Tarski queries🔗

HexSturm computes a signed sum over the distinct roots of a polynomial in an open interval. For a head polynomial P and query polynomial F, each root of P contributes the sign of F there: -1, 0 or 1. Querying 1 therefore counts the roots. A general query can return zero even when the interval contains roots, because opposite signs cancel.

The computational import is HexSturm. It is Mathlib-free and uses the shared signed-remainder and certificate-checking kernel from HexRealRoots. Import HexSturmTheory for the proofs relating those computations to mathematical root sets. Mathlib and Tau Ceti belong to the companion; neither is a computational dependency. Both Sturm libraries are development libraries in hex-dev and have not yet been published as split packages.

This frontend counts and queries roots without enumerating them. Complete sign tables and Thom encodings belong to sign determination; root isolation and adjoining a selected root belong to the real-closure library. The integer isolator documented in HexRealRoots remains a separate entry point.

39.7.2. Coefficients, endpoints and the success domain🔗

Polynomials use Hex.DensePoly, with coefficients stored in ascending degree order. Hex.Endpoint represents a finite coefficient value, negative infinity or positive infinity. Intervals are open: a finite endpoint does not belong to the queried interval.

The query accepts an explicit total sign function on coefficients. Canonical ordered coefficients can use the following function:

Hex.Sturm.orderSign.{u} {E : Type u} [Zero E] [DecidableEq E] [LT E]
  [DecidableLT E] (a : E) : ℤ
Hex.Sturm.orderSign.{u} {E : Type u}
  [Zero E] [DecidableEq E] [LT E]
  [DecidableLT E] (a : E) : ℤ

For the mathematical interpretation, a valid domain requires a nonzero, squarefree head, strictly ordered endpoints, and no head root at either finite endpoint. Nonzero constants are valid heads and give zero roots. The query polynomial does not affect domain validity: it can be zero, share roots with the head, or have higher degree than the head.

Hex.Sturm.query.{u} {E : Type u} [Zero E] [DecidableEq E] [One E]
  [Add E] [Sub E] [Mul E] [NatCast E] [Neg E] [Inv E] (sign : E → ℤ)
  (p f : Hex.DensePoly E) (a b : Hex.Endpoint E) : Option ℤ
Hex.Sturm.query.{u} {E : Type u} [Zero E]
  [DecidableEq E] [One E] [Add E] [Sub E]
  [Mul E] [NatCast E] [Neg E] [Inv E]
  (sign : E → ℤ) (p f : Hex.DensePoly E)
  (a b : Hex.Endpoint E) : Option ℤ

Here P = X²-1 has roots -1 and 1. The queries of X and X-1 illustrate cancellation and a zero contribution at a shared root:

none means that the head or interval is invalid. It is not a refinement timeout or an inconclusive sign. In particular, a zero query does not make an invalid head acceptable:

The sign callback and coefficient arithmetic must be total and lawful. A bounded approximation attempt from HexOrderedFn does not by itself supply this interface. Registered real extensions justify total sign search using their additional containment, width and relative-transcendence laws.

39.7.3. Prepare a head once🔗

Hex.Sturm.PreparedDomain stores the sign function, head, endpoints and the head's validated squarefree chain. Its constructor is private. Preparation validates the domain; subsequent prepared queries reuse the squarefree chain while computing the chain for their own query polynomial.

Hex.Sturm.PreparedDomain.{u} (E : Type u) [Zero E] [DecidableEq E]
  [One E] [Add E] [Sub E] [Mul E] [NatCast E] [Neg E] [Inv E] : Type u
Hex.Sturm.PreparedDomain.{u} (E : Type u)
  [Zero E] [DecidableEq E] [One E] [Add E]
  [Sub E] [Mul E] [NatCast E] [Neg E]
  [Inv E] : Type u

The stored data are the Hex.Sturm.PreparedDomain.sign, Hex.Sturm.PreparedDomain.head, Hex.Sturm.PreparedDomain.lower, Hex.Sturm.PreparedDomain.upper and Hex.Sturm.PreparedDomain.squarefree fields. The Hex.Sturm.PreparedDomain.endpoints_valid and Hex.Sturm.PreparedDomain.last_constant proofs retain the original endpoint guards and nonzero constant terminal. The Hex.Sturm.PreparedDomain.produced proof binds the stored chain to the actual producer. The public restoration operation requires these guarantees as inputs; transport preserves them.

Hex.Sturm.prepare.{u} {E : Type u} [Zero E] [DecidableEq E] [One E]
  [Add E] [Sub E] [Mul E] [NatCast E] [Neg E] [Inv E] (sign : E → ℤ)
  (p : Hex.DensePoly E) (a b : Hex.Endpoint E) :
  Option (Hex.Sturm.PreparedDomain E)
Hex.Sturm.prepare.{u} {E : Type u}
  [Zero E] [DecidableEq E] [One E] [Add E]
  [Sub E] [Mul E] [NatCast E] [Neg E]
  [Inv E] (sign : E → ℤ)
  (p : Hex.DensePoly E)
  (a b : Hex.Endpoint E) :
  Option (Hex.Sturm.PreparedDomain E)

Hex.Sturm.queryPrepared.{u} {E : Type u} [Zero E] [DecidableEq E]
  [One E] [Add E] [Sub E] [Mul E] [NatCast E] [Neg E] [Inv E]
  (domain : Hex.Sturm.PreparedDomain E) (f : Hex.DensePoly E) : ℤ
Hex.Sturm.queryPrepared.{u} {E : Type u}
  [Zero E] [DecidableEq E] [One E] [Add E]
  [Sub E] [Mul E] [NatCast E] [Neg E]
  [Inv E]
  (domain : Hex.Sturm.PreparedDomain E)
  (f : Hex.DensePoly E) : ℤ

Querying 1 has a further specialization: the stored squarefree chain serves in both certificate positions, avoiding a second chain construction. The result remains an integer; its nonnegativity is a semantic theorem.

Hex.Sturm.countPrepared.{u} {E : Type u} [Zero E] [DecidableEq E]
  [One E] [Add E] [Sub E] [Mul E] [NatCast E] [Neg E] [Inv E]
  (domain : Hex.Sturm.PreparedDomain E) : ℤ
Hex.Sturm.countPrepared.{u} {E : Type u}
  [Zero E] [DecidableEq E] [One E] [Add E]
  [Sub E] [Mul E] [NatCast E] [Neg E]
  [Inv E]
  (domain : Hex.Sturm.PreparedDomain E) :
  ℤ

The prepared count belongs to its current interval. To reuse the same head on another interval, retarget the endpoints and check their guards again:

Hex.Sturm.PreparedDomain.withEndpoints?.{u} {E : Type u} [Zero E]
  [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [NatCast E] [Neg E]
  [Inv E] (domain : Hex.Sturm.PreparedDomain E)
  (lower upper : Hex.Endpoint E) : Option (Hex.Sturm.PreparedDomain E)
Hex.Sturm.PreparedDomain.withEndpoints?.{u}
  {E : Type u} [Zero E] [DecidableEq E]
  [One E] [Add E] [Sub E] [Mul E]
  [NatCast E] [Neg E] [Inv E]
  (domain : Hex.Sturm.PreparedDomain E)
  (lower upper : Hex.Endpoint E) :
  Option (Hex.Sturm.PreparedDomain E)

Hex.Sturm.PreparedDomain.withEndpoints_eq proves that retargeting returns the same whole result as fresh preparation. The binding theorem preserves the literal head, sign and squarefree chain and records the new endpoints. Old endpoint signs, counts and certificates are not proofs about the retargeted interval.

For already proved chain data, Hex.Sturm.PreparedDomain.ofChecked restores a domain using endpoint validity, a constant-terminal proof and equality with the actual producer's chain. Serialized chain data alone do not meet those requirements. Hex.Sturm.prepare_ofChecked characterizes the restored value. Equal-operation transport through Hex.Sturm.PreparedDomain.changeOps preserves those proofs and the stored data without repeating preparation.

39.7.4. Produce and check literal certificates🔗

certify returns a finite Hex.TarskiCertificate containing the head and query, endpoints, remainder identities, signs and claimed value. It also records a caller-supplied context. check takes all these expected bindings separately, including the claimed integer. It checks the proposed certificate rather than regenerating the producer's chains.

Hex.Sturm.certify.{u, v} {E : Type u} [Zero E] [DecidableEq E] [One E]
  [Add E] [Sub E] [Mul E] [NatCast E] [Neg E] [Inv E] {Ctx : Type v}
  (sign : E → ℤ) (context : Ctx) (p f : Hex.DensePoly E)
  (a b : Hex.Endpoint E) : Option (Hex.TarskiCertificate E E Ctx)
Hex.Sturm.certify.{u, v} {E : Type u}
  [Zero E] [DecidableEq E] [One E] [Add E]
  [Sub E] [Mul E] [NatCast E] [Neg E]
  [Inv E] {Ctx : Type v} (sign : E → ℤ)
  (context : Ctx) (p f : Hex.DensePoly E)
  (a b : Hex.Endpoint E) :
  Option (Hex.TarskiCertificate E E Ctx)

Hex.Sturm.check.{u, v} {E : Type u} [Zero E] [DecidableEq E] [One E]
  [Add E] [Sub E] [Mul E] [NatCast E] {Ctx : Type v} [DecidableEq Ctx]
  (sign : E → ℤ) (context : Ctx) (p f : Hex.DensePoly E)
  (a b : Hex.Endpoint E) (value : ℤ)
  (cert : Hex.TarskiCertificate E E Ctx) : Bool
Hex.Sturm.check.{u, v} {E : Type u}
  [Zero E] [DecidableEq E] [One E] [Add E]
  [Sub E] [Mul E] [NatCast E]
  {Ctx : Type v} [DecidableEq Ctx]
  (sign : E → ℤ) (context : Ctx)
  (p f : Hex.DensePoly E)
  (a b : Hex.Endpoint E) (value : ℤ)
  (cert : Hex.TarskiCertificate E E Ctx) :
  Bool

The second check rejects the foreign context even though the mathematical polynomial and interval are unchanged. Accepted replay retains every literal binding through Hex.Sturm.check_bindings. This is separate from the theorem assigning the accepted value its mathematical meaning.

certifyPrepared adds a context to a prepared query; certifyCountPrepared specializes it to query 1 and the stored chain. Their equality and value lemmas expose agreement with ordinary certification and querying. Hex.Sturm.checkCached_eq proves that optional reuse of checked domain evidence preserves the complete checker result, including rejection and cache misses.

Certificate rejection only rejects that proposed evidence. It does not prove that the mathematical query is undefined. Conversely, a successful example from the producer is not the general soundness proof for arbitrary supplied certificates.

39.7.5. Reduce a large query before computing its value🔗

At a root of P, the value of F equals the value of its remainder modulo P. queryReduced uses the existing remainder-only division worker before the shared query producer, avoiding a retained high-degree quotient.

Hex.Sturm.queryReduced.{u} {E : Type u} [Zero E] [DecidableEq E] [One E]
  [Add E] [Sub E] [Mul E] [NatCast E] [Neg E] [Inv E] [Div E]
  (sign : E → ℤ) (p f : Hex.DensePoly E) (a b : Hex.Endpoint E) :
  Option ℤ
Hex.Sturm.queryReduced.{u} {E : Type u}
  [Zero E] [DecidableEq E] [One E] [Add E]
  [Sub E] [Mul E] [NatCast E] [Neg E]
  [Inv E] [Div E] (sign : E → ℤ)
  (p f : Hex.DensePoly E)
  (a b : Hex.Endpoint E) : Option ℤ

The companion's HexSturmTheory.queryReduced_eq proves equality with the ordinary query's entire Option, including failure. Its hypotheses include lawful interpretation of coefficient division. The prepared version has the corresponding value equality.

These are value APIs. When evidence must bind the original unreduced query, use the ordinary certificate APIs. Reduction does not provide a certificate with different inputs that can be replayed as the original one.

For the earlier head X²-1, the eighth power has value 1 at each root:

39.7.6. The Mathlib correspondence🔗

Polynomial interpretation is explained in the polynomial correspondence. The shared signed root sum comes from the Sturm–Tarski foundation.

The semantic field is an ordered real closed field. It can be non-Archimedean; an ordinary real embedding is not required. Coefficient storage itself need not have a field or order instance: an interpretation into that semantic field must preserve the supplied operations and signs and reflect zero. Zero reflection does not require injectivity on all stored representatives.

Producer theorems also require lawful negation and inversion because they justify the field normalization. The arbitrary-certificate theorem needs the operations used to check the supplied identities and signs; it does not assume that the producer made the certificate.

HexSturmTheory.Domain states the head and endpoint conditions; HexSturmTheory.domain_iff exposes them without unfolding the predicate. The endpoint order and nonvanishing predicates simplify at finite and infinite endpoints. The complete query theorem gives both producer success on that domain and the meaning of every returned integer:

HexSturmTheory.query_iff.{u, v} {E : Type u} {R : Type v} [Zero E]
  [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [NatCast E] [Field R]
  [DecidableEq R] [LinearOrder R] [IsStrictOrderedRing R]
  [IsRealClosed R] (f : E → R) (hz : ∀ (a : E), f a = 0 ↔ a = 0)
  (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b)
  (hs : ∀ (a b : E), f (a - b) = f a - f b)
  (hm : ∀ (a b : E), f (a * b) = f a * f b)
  (hnat : ∀ (n : ℕ), f ↑n = ↑n) (sign : E → ℤ)
  (hsign : ∀ (a : E), sign a = ↑(SignType.sign (f a))) [Neg E] [Inv E]
  (hn : ∀ (a : E), f (-a) = -f a) (hi : ∀ (a : E), f a⁻¹ = (f a)⁻¹)
  (p q : Hex.DensePoly E) (a b : Hex.Endpoint E) (value : ℤ) :
  Hex.Sturm.query sign p q a b = some value ↔
    HexSturmTheory.Domain f hz p a b ∧
      value =
        HexRealRootsTheory.Tarski.rootSum
          (HexPolyTheory.Interpret.interpret f hz p)
          (HexPolyTheory.Interpret.interpret f hz q)
          (Hex.Endpoint.map f a) (Hex.Endpoint.map f b)
HexSturmTheory.query_iff.{u, v}
  {E : Type u} {R : Type v} [Zero E]
  [DecidableEq E] [One E] [Add E] [Sub E]
  [Mul E] [NatCast E] [Field R]
  [DecidableEq R] [LinearOrder R]
  [IsStrictOrderedRing R] [IsRealClosed R]
  (f : E → R)
  (hz : ∀ (a : E), f a = 0 ↔ a = 0)
  (h1 : f 1 = 1)
  (ha :
    ∀ (a b : E), f (a + b) = f a + f b)
  (hs :
    ∀ (a b : E), f (a - b) = f a - f b)
  (hm :
    ∀ (a b : E), f (a * b) = f a * f b)
  (hnat : ∀ (n : ℕ), f ↑n = ↑n)
  (sign : E → ℤ)
  (hsign :
    ∀ (a : E),
      sign a = ↑(SignType.sign (f a)))
  [Neg E] [Inv E]
  (hn : ∀ (a : E), f (-a) = -f a)
  (hi : ∀ (a : E), f a⁻¹ = (f a)⁻¹)
  (p q : Hex.DensePoly E)
  (a b : Hex.Endpoint E) (value : ℤ) :
  Hex.Sturm.query sign p q a b =
      some value ↔
    HexSturmTheory.Domain f hz p a b ∧
      value =
        HexRealRootsTheory.Tarski.rootSum
          (HexPolyTheory.Interpret.interpret
            f hz p)
          (HexPolyTheory.Interpret.interpret
            f hz q)
          (Hex.Endpoint.map f a)
          (Hex.Endpoint.map f b)

For example, specialize the public theorem to the ordinary real field. This uses HexSturmTheory together with HexRealRootsTheory, whose umbrella supplies the real-closed-field instance for ℝ. Both are ordinary public imports:

HexSturmTheory.check_sound.{u, v, w} {E : Type u} {R : Type v} [Zero E]
  [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [NatCast E] [Field R]
  [DecidableEq R] [LinearOrder R] [IsStrictOrderedRing R]
  [IsRealClosed R] (f : E → R) (hz : ∀ (a : E), f a = 0 ↔ a = 0)
  (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b)
  (hs : ∀ (a b : E), f (a - b) = f a - f b)
  (hm : ∀ (a b : E), f (a * b) = f a * f b)
  (hnat : ∀ (n : ℕ), f ↑n = ↑n) (sign : E → ℤ)
  (hsign : ∀ (a : E), sign a = ↑(SignType.sign (f a))) {Ctx : Type w}
  [DecidableEq Ctx] (context : Ctx) (p q : Hex.DensePoly E)
  (a b : Hex.Endpoint E) (value : ℤ)
  (certificate : Hex.TarskiCertificate E E Ctx)
  (checked :
    Hex.Sturm.check sign context p q a b value certificate = true) :
  HexSturmTheory.Domain f hz p a b ∧
    value =
      HexRealRootsTheory.Tarski.rootSum
        (HexPolyTheory.Interpret.interpret f hz p)
        (HexPolyTheory.Interpret.interpret f hz q)
        (Hex.Endpoint.map f a) (Hex.Endpoint.map f b)
HexSturmTheory.check_sound.{u, v, w}
  {E : Type u} {R : Type v} [Zero E]
  [DecidableEq E] [One E] [Add E] [Sub E]
  [Mul E] [NatCast E] [Field R]
  [DecidableEq R] [LinearOrder R]
  [IsStrictOrderedRing R] [IsRealClosed R]
  (f : E → R)
  (hz : ∀ (a : E), f a = 0 ↔ a = 0)
  (h1 : f 1 = 1)
  (ha :
    ∀ (a b : E), f (a + b) = f a + f b)
  (hs :
    ∀ (a b : E), f (a - b) = f a - f b)
  (hm :
    ∀ (a b : E), f (a * b) = f a * f b)
  (hnat : ∀ (n : ℕ), f ↑n = ↑n)
  (sign : E → ℤ)
  (hsign :
    ∀ (a : E),
      sign a = ↑(SignType.sign (f a)))
  {Ctx : Type w} [DecidableEq Ctx]
  (context : Ctx) (p q : Hex.DensePoly E)
  (a b : Hex.Endpoint E) (value : ℤ)
  (certificate :
    Hex.TarskiCertificate E E Ctx)
  (checked :
    Hex.Sturm.check sign context p q a b
        value certificate =
      true) :
  HexSturmTheory.Domain f hz p a b ∧
    value =
      HexRealRootsTheory.Tarski.rootSum
        (HexPolyTheory.Interpret.interpret
          f hz p)
        (HexPolyTheory.Interpret.interpret
          f hz q)
        (Hex.Endpoint.map f a)
        (Hex.Endpoint.map f b)

That theorem proves domain validity and the signed sum for any accepted certificate. The independent HexSturmTheory.certify_checks theorem proves acceptance of produced certificates. HexSturmTheory.check_sound gives any accepted certificate its meaning, while HexSturmTheory.query_iff proves that the producer succeeds exactly on valid domains. A few successful outputs cannot establish those general statements.

HexSturmTheory.queryPrepared_sound gives prepared-query semantics; HexSturmTheory.countPrepared_sound identifies the actual prepared integer count with the cardinality of the current interval's root set. HexSturmTheory.countPrepared_nonneg justifies its nonnegativity before natural-number conversion.

HexSturmTheory.rootCount_eq.{u, v} {E : Type u} {R : Type v} [Zero E]
  [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [NatCast E] [Field R]
  [DecidableEq R] [LinearOrder R] [IsStrictOrderedRing R]
  [IsRealClosed R] (f : E → R) (hz : ∀ (a : E), f a = 0 ↔ a = 0)
  (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b)
  (hs : ∀ (a b : E), f (a - b) = f a - f b)
  (hm : ∀ (a b : E), f (a * b) = f a * f b)
  (hnat : ∀ (n : ℕ), f ↑n = ↑n) (sign : E → ℤ)
  (hsign : ∀ (a : E), sign a = ↑(SignType.sign (f a))) [Neg E] [Inv E]
  (hn : ∀ (a : E), f (-a) = -f a) (hi : ∀ (a : E), f a⁻¹ = (f a)⁻¹)
  (p : Hex.DensePoly E) (a b : Hex.Endpoint E) (n : ℕ)
  (result : Hex.Sturm.rootCount sign p a b = some n) :
  n =
    (HexRealRootsTheory.Tarski.rootsIn
        (HexPolyTheory.Interpret.interpret f hz p)
        (Hex.Endpoint.map f a) (Hex.Endpoint.map f b)).card
HexSturmTheory.rootCount_eq.{u, v}
  {E : Type u} {R : Type v} [Zero E]
  [DecidableEq E] [One E] [Add E] [Sub E]
  [Mul E] [NatCast E] [Field R]
  [DecidableEq R] [LinearOrder R]
  [IsStrictOrderedRing R] [IsRealClosed R]
  (f : E → R)
  (hz : ∀ (a : E), f a = 0 ↔ a = 0)
  (h1 : f 1 = 1)
  (ha :
    ∀ (a b : E), f (a + b) = f a + f b)
  (hs :
    ∀ (a b : E), f (a - b) = f a - f b)
  (hm :
    ∀ (a b : E), f (a * b) = f a * f b)
  (hnat : ∀ (n : ℕ), f ↑n = ↑n)
  (sign : E → ℤ)
  (hsign :
    ∀ (a : E),
      sign a = ↑(SignType.sign (f a)))
  [Neg E] [Inv E]
  (hn : ∀ (a : E), f (-a) = -f a)
  (hi : ∀ (a : E), f a⁻¹ = (f a)⁻¹)
  (p : Hex.DensePoly E)
  (a b : Hex.Endpoint E) (n : ℕ)
  (result :
    Hex.Sturm.rootCount sign p a b =
      some n) :
  n =
    (HexRealRootsTheory.Tarski.rootsIn
        (HexPolyTheory.Interpret.interpret
          f hz p)
        (Hex.Endpoint.map f a)
        (Hex.Endpoint.map f b)).card

HexSturmTheory.rootCount_isSome preserves the same domain as querying. Although the executable operation uses Int.toNat, HexSturmTheory.query_nonneg and HexSturmTheory.rootCount_query prove that no lawful count is clamped. HexSturmTheory.rootCount_map identifies the whole result after casting back to integers. These counts concern distinct roots of a squarefree head, not multiplicities of an arbitrary polynomial.

HexSturmTheory.query_bound bounds the absolute signed sum by the root count and the head degree. HexSturmTheory.query_sign identifies the answer with the sign at a selected root when the interval's semantic root set is exactly that singleton; the query does not itself select or isolate such a root.

39.7.7. Representation changes and the integer frontend🔗

HexSturmTheory.EndpointLt.map and HexSturmTheory.Nonvanishing.map compose endpoint interpretations. HexSturmTheory.domain_eq transfers a domain between equal interpreted heads and endpoints; HexSturmTheory.domain_congr also permits a nonzero constant factor in the head.

HexSturmTheory.query_congr compares representations interpreted in a common ordered field. It preserves the entire query result at corresponding finite or infinite endpoints, allowing positive scaling of both input polynomials. It does not construct a common field or an ordinary real realization of an arbitrary ordered extension.

For rational coefficients and a finite ordered dyadic interval, HexSturmTheory.query_rat_eq identifies the result with ZPoly.tarskiQuery after positive denominator clearing. The equality includes invalid none cases; differently normalized certificates need not be identical. Integer queries retain their finite-interval API.

The executable translations are Hex.TarskiCertificate.clearDenominators and Hex.TarskiCertificate.toRat, supplied by HexSturm.Transport. HexSturmTheory.DenominatorClearing.certificate_checks and HexSturmTheory.IntCast.certificate_checks prove that translations of accepted certificates are accepted, preserving the literal context and claimed value without rerunning the producer.

Finally, HexSturmTheory.rootCount_sturm connects successful finite-dyadic counts to the existing integer half-open Sturm count. Success includes both root-free endpoint guards; this theorem does not change the older API's behavior when its upper endpoint is a root.