theorem HexRealRootsTheory.Tarski.check_value {D : Type v} {A : Type w} {Ctx : Type u} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] [DecidableEq A] [DecidableEq Ctx] (sign : D → ℤ) (endpointSigns : Hex.EndpointSigns D A) (context : Ctx) (p g : Hex.DensePoly D) (a b : Hex.Endpoint A) (value : ℤ) (cert : Hex.TarskiCertificate D A Ctx) (h : Hex.TarskiCertificate.check sign endpointSigns context p g a b value cert = true) : Hex.SignedRemainderChain.check sign p g cert.remainders = true ∧ value = ↑(Hex.signVar (Hex.TarskiCertificate.signs sign endpointSigns cert.remainders.chain a).toList) - ↑(Hex.signVar (Hex.TarskiCertificate.signs sign endpointSigns cert.remainders.chain b).toList)

Accepted literal replay fixes its value to the endpoint variations of its supplied remainder chain. This does not invoke a producer or root semantics.

theorem HexRealRootsTheory.Tarski.check_singleton {D : Type v} {A : Type w} {Ctx : Type u} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] [DecidableEq A] [DecidableEq Ctx] (sign : D → ℤ) (endpointSigns : Hex.EndpointSigns D A) (context : Ctx) (p g : Hex.DensePoly D) (a b : Hex.Endpoint A) (value : ℤ) (cert : Hex.TarskiCertificate D A Ctx) (h : Hex.TarskiCertificate.check sign endpointSigns context p g a b value cert = true) (hs : cert.remainders.chain.size = 1) : value = 0

A checked singleton chain has zero variation at both endpoints.

theorem HexRealRootsTheory.Tarski.check_constant {D : Type v} {A : Type w} {Ctx : Type u} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] [DecidableEq A] [DecidableEq Ctx] (sign : D → ℤ) (endpointSigns : Hex.EndpointSigns D A) (context : Ctx) (p g : Hex.DensePoly D) (a b : Hex.Endpoint A) (value : ℤ) (cert : Hex.TarskiCertificate D A Ctx) (h : Hex.TarskiCertificate.check sign endpointSigns context p g a b value cert = true) (hp : p.size = 1) : value = 0

Constant heads force a singleton checked chain, hence a zero answer. This supported count specialization needs no signed-index theorem.

theorem HexRealRootsTheory.Tarski.signs_scale {K : Type u} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (s t : ℤ) (x y c : K) (hc : 0 < c) (he : y = c * x) (hs : -1 ≤ s ∧ s ≤ 1) (ht : -1 ≤ t ∧ t ≤ 1) (hsn : s < 0 ↔ x < 0) (htn : t < 0 ↔ y < 0) (hsz : s = 0 ↔ x = 0) (htz : t = 0 ↔ y = 0) : s = t

Exact three-valued signs agree when their arguments differ by a positive factor. Zero evaluations are included.

theorem HexRealRootsTheory.Tarski.finite_signs_eq {K : Type u} [Field K] [DecidableEq K] [LinearOrder K] [IsStrictOrderedRing K] {D : Type v} {E : Type w} {A : Type u₁} {B : Type u₂} [Zero D] [DecidableEq D] [Zero E] [DecidableEq E] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) (j : E → K) (jz : ∀ (a : E), j a = 0 ↔ a = 0) (sign : D → ℤ) (sign' : E → ℤ) (endpointSigns : Hex.EndpointSigns D A) (endpointSigns' : Hex.EndpointSigns E B) (a : A) (b : B) (x : K) (hbound : ∀ (p : Hex.DensePoly D), -1 ≤ endpointSigns.evalSign p a ∧ endpointSigns.evalSign p a ≤ 1) (hbound' : ∀ (p : Hex.DensePoly E), -1 ≤ endpointSigns'.evalSign p b ∧ endpointSigns'.evalSign p b ≤ 1) (hneg : ∀ (p : Hex.DensePoly D), endpointSigns.evalSign p a < 0 ↔ Polynomial.eval x (HexPolyTheory.Interpret.interpret f hz p) < 0) (hneg' : ∀ (p : Hex.DensePoly E), endpointSigns'.evalSign p b < 0 ↔ Polynomial.eval x (HexPolyTheory.Interpret.interpret j jz p) < 0) (hzero : ∀ (p : Hex.DensePoly D), endpointSigns.evalSign p a = 0 ↔ Polynomial.eval x (HexPolyTheory.Interpret.interpret f hz p) = 0) (hzero' : ∀ (p : Hex.DensePoly E), endpointSigns'.evalSign p b = 0 ↔ Polynomial.eval x (HexPolyTheory.Interpret.interpret j jz p) = 0) (chain : Array (Hex.DensePoly D)) (chain' : Array (Hex.DensePoly E)) (hsize : chain.size = chain'.size) (hscale : ∀ (i : ℕ), ∃ (c : K), 0 < c ∧ HexPolyTheory.Interpret.interpret j jz (chain'.getD i 0) = Polynomial.C c * HexPolyTheory.Interpret.interpret f hz (chain.getD i 0)) : Hex.TarskiCertificate.signs sign endpointSigns chain (Hex.Endpoint.finite a) = Hex.TarskiCertificate.signs sign' endpointSigns' chain' (Hex.Endpoint.finite b)

Positive entrywise scaling preserves the actual finite endpoint sign arrays, and hence their zero-skipping variation counts. Endpoint carriers and coefficient representations may differ on the two sides.

theorem HexRealRootsTheory.Tarski.infinite_signs_eq {K : Type u} [Field K] [DecidableEq K] [LinearOrder K] [IsStrictOrderedRing K] {D : Type v} {E : Type w} {A : Type u₁} {B : Type u₂} [Zero D] [DecidableEq D] [Zero E] [DecidableEq E] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) (j : E → K) (jz : ∀ (a : E), j a = 0 ↔ a = 0) (sign : D → ℤ) (sign' : E → ℤ) (endpointSigns : Hex.EndpointSigns D A) (endpointSigns' : Hex.EndpointSigns E B) (hbound : ∀ (a : D), -1 ≤ sign a ∧ sign a ≤ 1) (hbound' : ∀ (a : E), -1 ≤ sign' a ∧ sign' a ≤ 1) (hneg : ∀ (a : D), sign a < 0 ↔ f a < 0) (hneg' : ∀ (a : E), sign' a < 0 ↔ j a < 0) (hzero : ∀ (a : D), sign a = 0 ↔ f a = 0) (hzero' : ∀ (a : E), sign' a = 0 ↔ j a = 0) (chain : Array (Hex.DensePoly D)) (chain' : Array (Hex.DensePoly E)) (hsize : chain.size = chain'.size) (hscale : ∀ (i : ℕ), ∃ (c : K), 0 < c ∧ HexPolyTheory.Interpret.interpret j jz (chain'.getD i 0) = Polynomial.C c * HexPolyTheory.Interpret.interpret f hz (chain.getD i 0)) : Hex.TarskiCertificate.signs sign endpointSigns chain Hex.Endpoint.negInf = Hex.TarskiCertificate.signs sign' endpointSigns' chain' Hex.Endpoint.negInf ∧ Hex.TarskiCertificate.signs sign endpointSigns chain Hex.Endpoint.posInf = Hex.TarskiCertificate.signs sign' endpointSigns' chain' Hex.Endpoint.posInf

Positive entrywise scaling preserves signs at both infinities: leading coefficient signs and degree parity agree, including zero entries.