theorem HexRealRootsTheory.Tarski.step_iff {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [Add D] [Sub D] [Mul D] (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) [LinearOrder K] [IsStrictOrderedRing K] (sign : D → ℤ) (hsign : ∀ (a : D), sign a = 1 ↔ 0 < f a) (a b c : Hex.DensePoly D) (s : Hex.RemainderStep D) : Hex.SignedRemainderChain.checkStep sign a b c s = true ↔ 0 < f s.leftScale ∧ 0 < f s.rightScale ∧ Polynomial.C (f s.leftScale) * HexPolyTheory.Interpret.interpret f hz a = HexPolyTheory.Interpret.interpret f hz s.quotient * HexPolyTheory.Interpret.interpret f hz b - Polynomial.C (f s.rightScale) * HexPolyTheory.Interpret.interpret f hz c

The actual replay step tests positive scales and a semantic zero difference.

theorem HexRealRootsTheory.Tarski.normalize_bounds {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [Sub D] (hs : ∀ (a b : D), f (a - b) = f a - f b) (normalize : Hex.DensePoly D → D × Hex.DensePoly D) (hnormalize : ∀ (r : Hex.DensePoly D), r ≠ 0 → f (normalize r).1 ≠ 0 ∧ Polynomial.C (f (normalize r).1) * HexPolyTheory.Interpret.interpret f hz (normalize r).2 = HexPolyTheory.Interpret.interpret f hz r) (r : Hex.DensePoly D) (hr : r ≠ 0) : (normalize r).2 ≠ 0 ∧ (normalize r).2.size = r.size ∧ -(normalize r).2 ≠ 0 ∧ (-(normalize r).2).size = r.size

A nonzero scalar normalization preserves stored size, also after the negative sign required by the signed-remainder recurrence.

theorem HexRealRootsTheory.Tarski.check_initial {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [Add D] [Sub D] [Mul D] (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) [NatCast D] [LinearOrder K] [IsStrictOrderedRing K] (hn : ∀ (n : ℕ), f ↑n = ↑n) (sign : D → ℤ) (hsign : ∀ (a : D), sign a = 1 ↔ 0 < f a) (p g : Hex.DensePoly D) (cert : Hex.SignedRemainderChain D) (h : Hex.SignedRemainderChain.check sign p g cert = true) : 0 < f cert.initial.leftScale ∧ 0 < f cert.initial.rightScale ∧ Polynomial.C (f cert.initial.leftScale) * (HexPolyTheory.Interpret.interpret f hz g * Polynomial.derivative (HexPolyTheory.Interpret.interpret f hz p)) = HexPolyTheory.Interpret.interpret f hz cert.initial.quotient * HexPolyTheory.Interpret.interpret f hz p + Polynomial.C (f cert.initial.rightScale) * HexPolyTheory.Interpret.interpret f hz (cert.chain.getD 1 0)

Accepted replay supplies the positive initial product reduction. This is an algebraic identity, not yet the Sturm–Tarski root-sum theorem.

theorem HexRealRootsTheory.Tarski.check_step {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [Add D] [Sub D] [Mul D] (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) [NatCast D] [LinearOrder K] [IsStrictOrderedRing K] (sign : D → ℤ) (hsign : ∀ (a : D), sign a = 1 ↔ 0 < f a) (p g : Hex.DensePoly D) (cert : Hex.SignedRemainderChain D) (h : Hex.SignedRemainderChain.check sign p g cert = true) (hn : cert.chain.size ≠ 1) (i : ℕ) (hi : i < cert.steps.size) : 0 < f (cert.steps.getD i { leftScale := 0, quotient := 0, rightScale := 0 }).leftScale ∧ 0 < f (cert.steps.getD i { leftScale := 0, quotient := 0, rightScale := 0 }).rightScale ∧ Polynomial.C (f (cert.steps.getD i { leftScale := 0, quotient := 0, rightScale := 0 }).leftScale) * HexPolyTheory.Interpret.interpret f hz (cert.chain.getD i 0) = HexPolyTheory.Interpret.interpret f hz (cert.steps.getD i { leftScale := 0, quotient := 0, rightScale := 0 }).quotient * HexPolyTheory.Interpret.interpret f hz (cert.chain.getD (i + 1) 0) - Polynomial.C (f (cert.steps.getD i { leftScale := 0, quotient := 0, rightScale := 0 }).rightScale) * HexPolyTheory.Interpret.interpret f hz (cert.chain.getD (i + 2) 0)

Every accepted finite triple has the positive signed recurrence under interpretation. The checker reads the supplied quotient; it does not divide.

theorem HexRealRootsTheory.Tarski.check_terminal {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [Add D] [Sub D] [Mul D] (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) [NatCast D] [LinearOrder K] [IsStrictOrderedRing K] (sign : D → ℤ) (hsign : ∀ (a : D), sign a = 1 ↔ 0 < f a) (p g : Hex.DensePoly D) (cert : Hex.SignedRemainderChain D) (h : Hex.SignedRemainderChain.check sign p g cert = true) (hn : cert.chain.size ≠ 1) (u : D) (q : Hex.DensePoly D) (ht : cert.terminal = some (u, q)) : 0 < f u ∧ Polynomial.C (f u) * HexPolyTheory.Interpret.interpret f hz (cert.chain.getD (cert.chain.size - 2) 0) = HexPolyTheory.Interpret.interpret f hz q * HexPolyTheory.Interpret.interpret f hz (cert.chain.getD (cert.chain.size - 1) 0)

Terminal replay is an exact zero-remainder identity with positive scale; the last polynomial is allowed to be nonconstant.

theorem HexRealRootsTheory.Tarski.check_bound {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [Add D] [Sub D] [Mul D] [NatCast D] (sign : D → ℤ) (p g : Hex.DensePoly D) (cert : Hex.SignedRemainderChain D) (h : Hex.SignedRemainderChain.check sign p g cert = true) : 0 < cert.chain.size ∧ cert.chain.size ≤ (HexPolyTheory.Interpret.interpret f hz p).natDegree + 1

Replay's literal size guard supplies the mathematical chain bound.

theorem HexRealRootsTheory.Tarski.check_nonzero {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [Add D] [Sub D] [Mul D] [NatCast D] (sign : D → ℤ) (p g : Hex.DensePoly D) (cert : Hex.SignedRemainderChain D) (h : Hex.SignedRemainderChain.check sign p g cert = true) (r : Hex.DensePoly D) (hr : r ∈ cert.chain) : HexPolyTheory.Interpret.interpret f hz r ≠ 0

Every supplied entry of an accepted replay is semantically nonzero.

theorem HexRealRootsTheory.Tarski.build_complete {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [One D] [Add D] [Sub D] [Mul D] (hs : ∀ (a b : D), f (a - b) = f a - f b) [Neg D] [NatCast D] (sign : D → ℤ) (normalize : Hex.DensePoly D → D × Hex.DensePoly D) (hnormalize : ∀ (r : Hex.DensePoly D), r ≠ 0 → f (normalize r).1 ≠ 0 ∧ Polynomial.C (f (normalize r).1) * HexPolyTheory.Interpret.interpret f hz (normalize r).2 = HexPolyTheory.Interpret.interpret f hz r) (p g : Hex.DensePoly D) (hp : p ≠ 0) (hr : (Hex.DensePoly.positivePseudoDiv sign (g * p.derivative) p).remainder.isZero = false) : (Hex.SignedRemainderChain.build sign normalize p g).terminal.isSome = true

The actual producer reaches its terminal identity after every nonzero initial remainder. The only normalization premise is a nonzero scalar identity.

theorem HexRealRootsTheory.Tarski.build_bound {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [One D] [Add D] [Sub D] [Mul D] (hs : ∀ (a b : D), f (a - b) = f a - f b) [Neg D] [NatCast D] (sign : D → ℤ) (normalize : Hex.DensePoly D → D × Hex.DensePoly D) (hnormalize : ∀ (r : Hex.DensePoly D), r ≠ 0 → f (normalize r).1 ≠ 0 ∧ Polynomial.C (f (normalize r).1) * HexPolyTheory.Interpret.interpret f hz (normalize r).2 = HexPolyTheory.Interpret.interpret f hz r) (p g : Hex.DensePoly D) (hp : p ≠ 0) : (Hex.SignedRemainderChain.build sign normalize p g).chain.size ≤ p.size

The producer's array satisfies the replay length bound under interpretation.

theorem HexRealRootsTheory.Tarski.step_produced {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [One D] [Add D] [Sub D] [Mul D] (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) [Neg D] [LinearOrder K] [IsStrictOrderedRing K] (h1 : f 1 = 1) (hn : ∀ (a : D), f (-a) = -f a) (sign : D → ℤ) (hpos : ∀ (a : D), sign a = 1 ↔ 0 < f a) (hneg : ∀ (a : D), sign a < 0 ↔ f a < 0) (normalize : Hex.DensePoly D → D × Hex.DensePoly D) (hnormalize : ∀ (r : Hex.DensePoly D), r ≠ 0 → 0 < f (normalize r).1 ∧ Polynomial.C (f (normalize r).1) * HexPolyTheory.Interpret.interpret f hz (normalize r).2 = HexPolyTheory.Interpret.interpret f hz r) (a b : Hex.DensePoly D) (hb : b ≠ 0) (hr : (Hex.DensePoly.positivePseudoDiv sign a b).remainder.isZero = false) : Hex.SignedRemainderChain.checkStep sign a b (-(normalize (Hex.DensePoly.positivePseudoDiv sign a b).remainder).2) { leftScale := (Hex.DensePoly.positivePseudoDiv sign a b).multiplier, quotient := (Hex.DensePoly.positivePseudoDiv sign a b).quotient, rightScale := (normalize (Hex.DensePoly.positivePseudoDiv sign a b).remainder).1 } = true

The producer's actual sign-corrected remainder and normalization satisfy the positive three-term replay check.

theorem HexRealRootsTheory.Tarski.terminal_produced {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [One D] [Add D] [Sub D] [Mul D] (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) [Neg D] [LinearOrder K] [IsStrictOrderedRing K] (h1 : f 1 = 1) (hn : ∀ (a : D), f (-a) = -f a) (sign : D → ℤ) (hpos : ∀ (a : D), sign a = 1 ↔ 0 < f a) (hneg : ∀ (a : D), sign a < 0 ↔ f a < 0) (a b : Hex.DensePoly D) (hb : b ≠ 0) (hr : (Hex.DensePoly.positivePseudoDiv sign a b).remainder.isZero = true) : sign (Hex.DensePoly.positivePseudoDiv sign a b).multiplier = 1 ∧ Hex.SignedRemainderChain.subIsZero (Hex.DensePoly.scale (Hex.DensePoly.positivePseudoDiv sign a b).multiplier a) ((Hex.DensePoly.positivePseudoDiv sign a b).quotient * b) = true

A zero final remainder produces the positive terminal identity checked by replay, independently of whether the last nonzero polynomial is constant.

theorem HexRealRootsTheory.Tarski.build_checks {D : Type u} {K : Type v} [Zero D] [DecidableEq D] [Field K] [DecidableEq K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) [One D] [Add D] [Sub D] [Mul D] (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) [Neg D] [LinearOrder K] [IsStrictOrderedRing K] (h1 : f 1 = 1) (hn : ∀ (a : D), f (-a) = -f a) (sign : D → ℤ) (hpos : ∀ (a : D), sign a = 1 ↔ 0 < f a) (hneg : ∀ (a : D), sign a < 0 ↔ f a < 0) (normalize : Hex.DensePoly D → D × Hex.DensePoly D) (hnormalize : ∀ (r : Hex.DensePoly D), r ≠ 0 → 0 < f (normalize r).1 ∧ Polynomial.C (f (normalize r).1) * HexPolyTheory.Interpret.interpret f hz (normalize r).2 = HexPolyTheory.Interpret.interpret f hz r) [NatCast D] (p g : Hex.DensePoly D) (hp : p ≠ 0) : Hex.SignedRemainderChain.check sign p g (Hex.SignedRemainderChain.build sign normalize p g) = true

Every chain produced from a nonzero head passes literal replay. The proof follows the array loop and discharges its backend laws through interpretation; no field structure is imposed on stored representatives.