theorem
HexRealRootsTheory.Tarski.integer_check_sound
{Ctx : Type u_1}
[DecidableEq Ctx]
(context : Ctx)
(p q : Hex.ZPoly)
(a b : Hex.Endpoint Dyadic)
(value : ℤ)
(certificate : Hex.TarskiCertificate ℤ Dyadic Ctx)
(checked : Hex.TarskiCertificate.check Int.sign Hex.EndpointSigns.intDyadic context p q a b value certificate = true)
:
value = rootSum (toPolyℝ p) (toPolyℝ q) (Hex.Endpoint.map Dyadic.toReal a) (Hex.Endpoint.map Dyadic.toReal b)
The integer/dyadic replay has root-sum semantics for arbitrary accepted evidence.
theorem
Hex.IntTarskiCertificate.check_sound
(p q : ZPoly)
(I : DyadicInterval)
(value : ℤ)
(certificate : IntTarskiCertificate)
(checked : check p q I value certificate = true)
:
Every accepted integer certificate proves its stated signed root sum.
theorem
Hex.ZPoly.tarskiQuery_eq
(p q : ZPoly)
(I : DyadicInterval)
(value : ℤ)
(result : p.tarskiQuery q I = some value)
:
The integer/dyadic query computes the signed sum over the distinct interval roots.
theorem
Hex.ZPoly.tarskiQuery_isSome
(p q : ZPoly)
(I : 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_sign
(p q : ZPoly)
(I : DyadicInterval)
(value : ℤ)
(x : ℝ)
(result : p.tarskiQuery q I = some value)
(single :
HexRealRootsTheory.Tarski.rootsIn (HexRealRootsTheory.toPolyℝ p)
(Endpoint.finite (HexRealRootsTheory.Dyadic.toReal I.lower))
(Endpoint.finite (HexRealRootsTheory.Dyadic.toReal I.upper)) = {x})
:
A query on an interval with one root returns the query polynomial's sign there.