hex

17.8. Signed sums over roots🔗

A Tarski query sums the sign of a query polynomial at each distinct root of another polynomial in an open interval. Querying the constant polynomial 1 counts roots; a negative value is possible for other queries. The computational operation Hex.ZPoly.tarskiQuery uses integer coefficients and exact dyadic endpoints. Its head must be nonzero and squarefree, and neither endpoint may be a root. A failed domain returns none.

The ordinary HexRealRootsTheory import exposes both the exact success-domain theorem and the interpretation of a successful answer in the real numbers:

🔗theorem
Hex.ZPoly.tarskiQuery_isSome (p q : Hex.ZPoly)
  (I : Hex.DyadicInterval) :
  (p.tarskiQuery q I).isSome = true ↔
    p ≠ 0 ∧
      Squarefree (HexRealRootsTheory.toPolyℝ p) ∧
        Polynomial.eval (HexRealRootsTheory.Dyadic.toReal I.lower)
              (HexRealRootsTheory.toPolyℝ p) ≠
            0 ∧
          Polynomial.eval (HexRealRootsTheory.Dyadic.toReal I.upper)
              (HexRealRootsTheory.toPolyℝ p) ≠
            0
Hex.ZPoly.tarskiQuery_isSome
  (p q : Hex.ZPoly)
  (I : Hex.DyadicInterval) :
  (p.tarskiQuery q I).isSome = true ↔
    p ≠ 0 ∧
      Squarefree
          (HexRealRootsTheory.toPolyℝ p) ∧
        Polynomial.eval
              (HexRealRootsTheory.Dyadic.toReal
                I.lower)
              (HexRealRootsTheory.toPolyℝ
                p) ≠
            0 ∧
          Polynomial.eval
              (HexRealRootsTheory.Dyadic.toReal
                I.upper)
              (HexRealRootsTheory.toPolyℝ
                p) ≠
            0

Integer querying succeeds exactly for a nonzero squarefree head with root-free endpoints.

🔗theorem
Hex.ZPoly.tarskiQuery_eq (p q : Hex.ZPoly) (I : Hex.DyadicInterval)
  (value : ℤ) (result : p.tarskiQuery q I = some value) :
  value =
    HexRealRootsTheory.Tarski.rootSum (HexRealRootsTheory.toPolyℝ p)
      (HexRealRootsTheory.toPolyℝ q)
      (Hex.Endpoint.finite (HexRealRootsTheory.Dyadic.toReal I.lower))
      (Hex.Endpoint.finite (HexRealRootsTheory.Dyadic.toReal I.upper))
Hex.ZPoly.tarskiQuery_eq (p q : Hex.ZPoly)
  (I : Hex.DyadicInterval) (value : ℤ)
  (result :
    p.tarskiQuery q I = some value) :
  value =
    HexRealRootsTheory.Tarski.rootSum
      (HexRealRootsTheory.toPolyℝ p)
      (HexRealRootsTheory.toPolyℝ q)
      (Hex.Endpoint.finite
        (HexRealRootsTheory.Dyadic.toReal
          I.lower))
      (Hex.Endpoint.finite
        (HexRealRootsTheory.Dyadic.toReal
          I.upper))

The integer/dyadic query computes the signed sum over the distinct interval roots.

The checker theorem also applies to arbitrary supplied certificate data. The following example uses that theorem directly; it does not assume that the certificate was produced by the search algorithm.

open Hex HexRealRootsTheory example (p q : ZPoly) (interval : DyadicInterval) (value : Int) (certificate : IntTarskiCertificate) (accepted : IntTarskiCertificate.check p q interval value certificate = true) : value = Tarski.rootSum (toPolyℝ p) (toPolyℝ q) (.finite (Dyadic.toReal interval.lower)) (.finite (Dyadic.toReal interval.upper)) := p:ZPolyq:ZPolyinterval:DyadicIntervalvalue:ℤcertificate:IntTarskiCertificateaccepted:IntTarskiCertificate.check p q interval value certificate = true⊢ value = Tarski.rootSum (toPolyℝ p) (toPolyℝ q) (Endpoint.finite interval.lower.toReal) (Endpoint.finite interval.upper.toReal) All goals completed! 🐙

The shared theorem HexRealRootsTheory.Tarski.check_rootSum works over any ordered real closed field, including non-Archimedean fields. Its coefficient interpretation and sign laws are explicit hypotheses. HexSturmTheory applies that theorem to the field frontend, prepared queries and root counts. Tau Ceti supplies the abstract Sturm–Tarski foundation in the theory companion; the computational package does not depend on it.