theorem HexRealRootsTheory.Tarski.remainder_scale {K : Type u} [Field K] (a b : K) (hb : b ≠ 0) (p q : Polynomial K) : Polynomial.C a * p % (Polynomial.C b * q) = Polynomial.C a * (p % q)

Rescaling the dividend and rescaling the divisor by a nonzero scalar rescales the remainder by the dividend's scalar.

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

The zero-padded view of an accepted chain is zero precisely beyond its stored entries. This uses zero reflection, not injectivity of interpretation.

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

Successive interpreted entries have strictly smaller degree, with the implicit zero after the last entry handled separately.

theorem HexRealRootsTheory.Tarski.check_initial_rem {K : Type u} [Field K] {D : Type v} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] [DecidableEq K] [LinearOrder K] [IsStrictOrderedRing K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) (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) (hn : ∀ (n : ℕ), f ↑n = ↑n) (sign : D → ℤ) (hpos : ∀ (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) : ∃ (c : K), 0 < c ∧ HexPolyTheory.Interpret.interpret f hz (cert.chain.getD 1 0) = Polynomial.C c * (HexPolyTheory.Interpret.interpret f hz g * Polynomial.derivative (HexPolyTheory.Interpret.interpret f hz p) % HexPolyTheory.Interpret.interpret f hz p)

An accepted initial reduction determines the second entry up to its recorded positive scalar, including the singleton/zero-remainder case.

theorem HexRealRootsTheory.Tarski.check_next_rem {K : Type u} [Field K] {D : Type v} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] [DecidableEq K] [LinearOrder K] [IsStrictOrderedRing K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) (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) (sign : D → ℤ) (hpos : ∀ (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) (i : ℕ) (hi : i + 1 < cert.chain.size) : ∃ (c : K), 0 < c ∧ HexPolyTheory.Interpret.interpret f hz (cert.chain.getD (i + 2) 0) = Polynomial.C c * -(HexPolyTheory.Interpret.interpret f hz (cert.chain.getD i 0) % HexPolyTheory.Interpret.interpret f hz (cert.chain.getD (i + 1) 0))

Each checked step determines the following entry up to a positive scalar. The terminal identity supplies the same equation with zero as the next entry; no constant-tail or coprimality hypothesis is needed.

theorem HexRealRootsTheory.Tarski.check_compare {K : Type u} [Field K] {D : Type v} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] [DecidableEq K] [LinearOrder K] [IsStrictOrderedRing K] (f : D → K) (hz : ∀ (a : D), f a = 0 ↔ a = 0) (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) (hn : ∀ (n : ℕ), f ↑n = ↑n) (sign : D → ℤ) (hpos : ∀ (a : D), sign a = 1 ↔ 0 < f a) {E : Type w} [Zero E] [DecidableEq E] [Add E] [Sub E] [Mul E] [NatCast E] (j : E → K) (jz : ∀ (a : E), j a = 0 ↔ a = 0) (ja : ∀ (a b : E), j (a + b) = j a + j b) (js : ∀ (a b : E), j (a - b) = j a - j b) (jm : ∀ (a b : E), j (a * b) = j a * j b) (jn : ∀ (n : ℕ), j ↑n = ↑n) (sign' : E → ℤ) (jpos : ∀ (a : E), sign' a = 1 ↔ 0 < j a) (p g : Hex.DensePoly D) (cert : Hex.SignedRemainderChain D) (h : Hex.SignedRemainderChain.check sign p g cert = true) (p' g' : Hex.DensePoly E) (cert' : Hex.SignedRemainderChain E) (h' : Hex.SignedRemainderChain.check sign' p' g' cert' = true) (a b : K) (ha' : 0 < a) (hb' : 0 < b) (hp : HexPolyTheory.Interpret.interpret j jz p' = Polynomial.C a * HexPolyTheory.Interpret.interpret f hz p) (hg : HexPolyTheory.Interpret.interpret j jz g' = Polynomial.C b * HexPolyTheory.Interpret.interpret f hz g) : cert.chain.size = cert'.chain.size ∧ ∀ (i : ℕ), ∃ (c : K), 0 < c ∧ HexPolyTheory.Interpret.interpret j jz (cert'.chain.getD i 0) = Polynomial.C c * HexPolyTheory.Interpret.interpret f hz (cert.chain.getD i 0)

Accepted chains for positively scaled inputs have the same length and correspond entry by entry by positive scalars. Both coefficient interpretations may be noninjective; no producer provenance or root theorem is assumed.