theorem HexRealRootsTheory.Tarski.int_zero (z : ℤ) : ↑z = 0 ↔ z = 0

@[reducible, inline]

noncomputable abbrev HexRealRootsTheory.Tarski.integerPoly (p : Hex.DensePoly ℤ) : Polynomial ℚ

Interpret the actual integer coefficient array in the fraction field.

Equations

• HexRealRootsTheory.Tarski.integerPoly = HexPolyTheory.Interpret.interpret (fun (z : ℤ) => ↑z) HexRealRootsTheory.Tarski.int_zero

theorem HexRealRootsTheory.Tarski.content_pos (p : Hex.ZPoly) (hp : p ≠ 0) : 0 < Hex.DensePoly.content p

Nonzero integer polynomials have positive content, regardless of the sign of their leading coefficient.

theorem HexRealRootsTheory.Tarski.integer_normalize (p : Hex.ZPoly) (hp : p ≠ 0) : 0 < ↑p.normalizeContent.1 ∧ Polynomial.C ↑p.normalizeContent.1 * integerPoly p.normalizeContent.2 = integerPoly p

The integer backend's exact content division has the shared positive normalization law in the semantic fraction field.

theorem HexRealRootsTheory.Tarski.integer_chain_checks (p g : Hex.ZPoly) (hp : p ≠ 0) : Hex.SignedRemainderChain.check Int.sign p g (Hex.SignedRemainderChain.build Int.sign Hex.ZPoly.normalizeContent p g) = true

Every produced integer signed chain passes literal replay, including singleton chains and chains with a nonconstant terminal gcd.

theorem HexRealRootsTheory.Tarski.integer_signs (p : Hex.ZPoly) (e : Hex.Endpoint Dyadic) : -1 ≤ Hex.Endpoint.signAt Int.sign Hex.EndpointSigns.intDyadic p e ∧ Hex.Endpoint.signAt Int.sign Hex.EndpointSigns.intDyadic p e ≤ 1

Exact dyadic evaluation and leading terms at infinity give three-valued signs.

theorem HexRealRootsTheory.Tarski.integer_certify_checks (p g : Hex.ZPoly) (I : Hex.DyadicInterval) (cert : Hex.IntTarskiCertificate) (hcert : Hex.IntTarskiCertificate.certify p g I = some cert) : Hex.IntTarskiCertificate.check p g I cert.value cert = true ∧ p.tarskiQuery g I = some cert.value

Every produced integer/dyadic certificate is accepted with its literal input bindings and the same value returned by the query frontend.

theorem HexRealRootsTheory.Tarski.integer_query_isSome (p g : Hex.ZPoly) (I : Hex.DyadicInterval) : (p.tarskiQuery g I).isSome = true ↔ Hex.TarskiCertificate.checkEndpoints Hex.EndpointSigns.intDyadic p (Hex.Endpoint.finite I.lower) (Hex.Endpoint.finite I.upper) = true ∧ Squarefree (integerPoly p)

The integer frontend has no resource-exhaustion failure: its Option records exactly the endpoint guards and squarefreeness over the fraction field.