theorem HexRealRootsTheory.Tarski.check_rootSum {D : Type u} {E : Type v} {Ctx : Type w} {R : Type u₁} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] [DecidableEq E] [DecidableEq Ctx] [Field R] [DecidableEq R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (f : D → R) (hz : ∀ (a : D), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : D), f (a + b) = f a + f b) (hs : ∀ (a b : D), f (a - b) = f a - f b) (hm : ∀ (a b : D), f (a * b) = f a * f b) (hnat : ∀ (n : ℕ), f ↑n = ↑n) (sign : D → ℤ) (hsign : ∀ (a : D), sign a = ↑(SignType.sign (f a))) (point : E → R) (ends : Hex.EndpointSigns D E) (hcompare : ∀ (a b : E), ends.compare a b = ↑(SignType.sign (point a - point b))) (heval : ∀ (p : Hex.DensePoly D) (a : E), ends.evalSign p a = ↑(SignType.sign (Polynomial.eval (point a) (HexPolyTheory.Interpret.interpret f hz p)))) (context : Ctx) (p q : Hex.DensePoly D) (a b : Hex.Endpoint E) (value : ℤ) (certificate : Hex.TarskiCertificate D E Ctx) (checked : Hex.TarskiCertificate.check sign ends context p q a b value certificate = true) : value = rootSum (HexPolyTheory.Interpret.interpret f hz p) (HexPolyTheory.Interpret.interpret f hz q) (Hex.Endpoint.map point a) (Hex.Endpoint.map point b)

Every accepted shared query certificate gives the sum of signs at the distinct roots in its open interval. Coefficient representations need only reflect zero and preserve the actual operations; endpoint representations may differ from coefficients. This includes infinite endpoints, constant heads, zero queries and common factors, with no producer-success premise.