theorem HexRealRootsTheory.Tarski.rootsIn_card (p : Polynomial ℝ) (I : Hex.DyadicInterval) (hsf : Squarefree p) (hb : Polynomial.eval (Dyadic.toReal I.upper) p ≠ 0) : (rootsIn p (Hex.Endpoint.finite (Dyadic.toReal I.lower)) (Hex.Endpoint.finite (Dyadic.toReal I.upper))).card = (Literal.rootsIn p I).card

The open distinct-root set agrees with the legacy half-open multiset count when roots are simple and the upper endpoint is not a root.

theorem HexRealRootsTheory.Tarski.integer_sturmChain (p : Hex.ZPoly) (cert : Hex.SignedRemainderChain ℤ) (h : Hex.SignedRemainderChain.check Int.sign p 1 cert = true) (hlast : cert.lastIsConstant = true) (hn : cert.chain.size ≠ 1) : Sturm.IsSturmChain (toPolyℝ p) (List.map toPolyℝ cert.chain.toList)

A checked derivative chain over the integers satisfies the existing real Sturm-chain axioms. The initial quotient disappears by strict derivative degree.

theorem HexRealRootsTheory.Tarski.integer_check_count {Ctx : Type u} [DecidableEq Ctx] (context : Ctx) (p : Hex.ZPoly) (I : Hex.DyadicInterval) (value : ℤ) (cert : Hex.TarskiCertificate ℤ Dyadic Ctx) (h : Hex.TarskiCertificate.check Int.sign Hex.EndpointSigns.intDyadic context p 1 (Hex.Endpoint.finite I.lower) (Hex.Endpoint.finite I.upper) value cert = true) : value = ↑(Literal.rootsIn (toPolyℝ p) I).card

Accepted integer certificates for query 1 count the roots in the real half-open interval, using the existing derivative Sturm theorem. Endpoint guards also exclude the upper root, so this is the specified open count.

theorem HexRealRootsTheory.Tarski.integer_check_rootSum {Ctx : Type u} [DecidableEq Ctx] (context : Ctx) (p : Hex.ZPoly) (I : Hex.DyadicInterval) (value : ℤ) (cert : Hex.TarskiCertificate ℤ Dyadic Ctx) (h : Hex.TarskiCertificate.check Int.sign Hex.EndpointSigns.intDyadic context p 1 (Hex.Endpoint.finite I.lower) (Hex.Endpoint.finite I.upper) value cert = true) : value = rootSum (toPolyℝ p) 1 (Hex.Endpoint.finite (Dyadic.toReal I.lower)) (Hex.Endpoint.finite (Dyadic.toReal I.upper))

Accepted query-one certificates realize the open-interval root sum.

theorem HexRealRootsTheory.Tarski.integer_query_count (p : Hex.ZPoly) (I : Hex.DyadicInterval) (value : ℤ) (h : p.tarskiQuery 1 I = some value) : value = ↑(Literal.rootsIn (toPolyℝ p) I).card

The effective integer/dyadic query of 1 has the existing real root-count semantics.

theorem HexRealRootsTheory.Tarski.integer_query_rootSum (p : Hex.ZPoly) (I : Hex.DyadicInterval) (value : ℤ) (h : p.tarskiQuery 1 I = some value) : value = rootSum (toPolyℝ p) 1 (Hex.Endpoint.finite (Dyadic.toReal I.lower)) (Hex.Endpoint.finite (Dyadic.toReal I.upper))

The supported query-one result uses the same open finite-root sum as the abstract Sturm–Tarski interface.

theorem HexRealRootsTheory.Tarski.integer_query_nonneg (p : Hex.ZPoly) (I : Hex.DyadicInterval) (value : ℤ) (h : p.tarskiQuery 1 I = some value) : 0 ≤ value

The effective integer/dyadic query of 1 is nonnegative.

theorem HexRealRootsTheory.Tarski.integer_check_total {Ctx : Type u} [DecidableEq Ctx] (context : Ctx) (p : Hex.ZPoly) (value : ℤ) (cert : Hex.TarskiCertificate ℤ Dyadic Ctx) (h : Hex.TarskiCertificate.check Int.sign Hex.EndpointSigns.intDyadic context p 1 Hex.Endpoint.negInf Hex.Endpoint.posInf value cert = true) : value = ↑(toPolyℝ p).roots.card

A checked integer derivative certificate on the whole line counts all real roots, using the existing real derivative-Sturm theorem.