theorem HexRealRootsTheory.Tarski.dyadicSign_neg (d : Dyadic) : Hex.dyadicSign d < 0 ↔ Dyadic.toReal d < 0

The actual dyadic sign reflects strict negativity of its real value.

theorem HexRealRootsTheory.Tarski.integer_checkEndpoints (p : Hex.ZPoly) (I : Hex.DyadicInterval) : Hex.TarskiCertificate.checkEndpoints Hex.EndpointSigns.intDyadic p (Hex.Endpoint.finite I.lower) (Hex.Endpoint.finite I.upper) = true ↔ p ≠ 0 ∧ Polynomial.eval (Dyadic.toReal I.lower) (toPolyℝ p) ≠ 0 ∧ Polynomial.eval (Dyadic.toReal I.upper) (toPolyℝ p) ≠ 0

The integer frontend's executable endpoint guards are exactly head and endpoint nonvanishing. Its interval already certifies strict endpoint order.

theorem HexRealRootsTheory.Tarski.interpret_int_real (p : Hex.ZPoly) : HexPolyTheory.Interpret.interpret (fun (z : ℤ) => ↑z) ⋯ p = toPolyℝ p

The generic integer interpretation agrees with the existing real-polynomial correspondence, rather than defining a second semantic polynomial.

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

Integer/dyadic Tarski production succeeds exactly on its mathematical open-interval domain. No root-sum theorem or resource bound is assumed.

theorem HexRealRootsTheory.Tarski.integer_check_domain (p g : Hex.ZPoly) (I : Hex.DyadicInterval) (value : ℤ) (cert : Hex.IntTarskiCertificate) (hc : Hex.IntTarskiCertificate.check p g I value cert = true) : p ≠ 0 ∧ Squarefree (toPolyℝ p) ∧ Polynomial.eval (Dyadic.toReal I.lower) (toPolyℝ p) ≠ 0 ∧ Polynomial.eval (Dyadic.toReal I.upper) (toPolyℝ p) ≠ 0

An accepted integer certificate proves the same mathematical domain using only its supplied squarefree chain and exact dyadic endpoint checks.