structure Hex.SignedRemainderChain.Prefix {D : Type u} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] (sign : D → Int) (p f : DensePoly D) (initial : RemainderStep D) (chain : Array (DensePoly D)) (steps : Array (RemainderStep D)) : Prop

The part of a literal replay already established before its terminal zero identity. The array stores every actual quotient and positive scale.

• two_le : 2 ≤ chain.size
• head : chain[0]? = some p
• nonzero (r : DensePoly D) : r ∈ chain → r ≠ 0
• descent (i : Nat) : i + 1 < chain.size → (chain.getD (i + 1) 0).size < (chain.getD i 0).size
• left_pos : sign initial.leftScale = 1
• right_pos : sign initial.rightScale = 1
• initial_eq : subIsZero (DensePoly.scale initial.leftScale (f * p.derivative)) (initial.quotient * p + DensePoly.scale initial.rightScale (chain.getD 1 0)) = true
• size_steps : steps.size + 2 = chain.size
• recurrences (i : Nat) : i < steps.size → checkStep sign (chain.getD i 0) (chain.getD (i + 1) 0) (chain.getD (i + 2) 0) (steps.getD i { leftScale := 0, quotient := 0, rightScale := 0 }) = true

theorem Hex.SignedRemainderChain.Prefix.pair {D : Type u} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] (sign : D → Int) (p f second : DensePoly D) (initial : RemainderStep D) (hp : p ≠ 0) (hs : second ≠ 0) (hd : second.size < p.size) (hl : sign initial.leftScale = 1) (hr : sign initial.rightScale = 1) (hi : subIsZero (DensePoly.scale initial.leftScale (f * p.derivative)) (initial.quotient * p + DensePoly.scale initial.rightScale second) = true) : Prefix sign p f initial #[p, second] #[]

A correctly reduced initial pair starts a replay prefix.

theorem Hex.SignedRemainderChain.Prefix.push {D : Type u} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] {sign : D → Int} {p f : DensePoly D} {initial : RemainderStep D} {chain : Array (DensePoly D)} {steps : Array (RemainderStep D)} (h : Prefix sign p f initial chain steps) (next : DensePoly D) (step : RemainderStep D) (hn : next ≠ 0) (hd : next.size < (chain.getD (chain.size - 1) 0).size) (hs : checkStep sign (chain.getD (chain.size - 2) 0) (chain.getD (chain.size - 1) 0) next step = true) : Prefix sign p f initial (chain.push next) (steps.push step)

Appending an actual signed-remainder step preserves all prior literal identities and adds precisely the new final recurrence.

theorem Hex.SignedRemainderChain.Prefix.finish {D : Type u} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] {sign : D → Int} {p f : DensePoly D} {initial : RemainderStep D} {chain : Array (DensePoly D)} {steps : Array (RemainderStep D)} (h : Prefix sign p f initial chain steps) (hp : p ≠ 0) (bound : chain.size ≤ p.size) (u : D) (q : DensePoly D) (hu : sign u = 1) (ht : subIsZero (DensePoly.scale u (chain.getD (chain.size - 2) 0)) (q * chain.getD (chain.size - 1) 0) = true) : check sign p f { chain := chain, degrees := Array.map' DensePoly.natDegree chain, initial := initial, steps := steps, terminal := some (u, q) } = true

Finishing an established prefix with a positive terminal zero identity passes the actual finite checker, with the computed degree evidence.

theorem Hex.SignedRemainderChain.singleton_checks {D : Type u} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] (sign : D → Int) (p f : DensePoly D) (initial : RemainderStep D) (hp : p ≠ 0) (hl : sign initial.leftScale = 1) (hr : sign initial.rightScale = 1) (hi : subIsZero (DensePoly.scale initial.leftScale (f * p.derivative)) (initial.quotient * p + DensePoly.scale initial.rightScale 0) = true) : check sign p f { chain := #[p], degrees := #[p.natDegree], initial := initial, steps := #[], terminal := none } = true

A zero initial remainder has a singleton replay, with no fictitious second entry or terminal pair.

theorem Hex.SignedRemainderChain.buildAux_checks {D : Type u} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] [One D] [Neg D] (sign : D → Int) (normalize : DensePoly D → D × DensePoly D) (hnext : ∀ (r : DensePoly D), r ≠ 0 → -(normalize r).snd ≠ 0 ∧ (-(normalize r).snd).size ≤ r.size) (hstep : ∀ (a b : DensePoly D), b ≠ 0 → (DensePoly.positivePseudoDiv sign a b).remainder.isZero = false → checkStep sign a b (-(normalize (DensePoly.positivePseudoDiv sign a b).remainder).snd) { leftScale := (DensePoly.positivePseudoDiv sign a b).multiplier, quotient := (DensePoly.positivePseudoDiv sign a b).quotient, rightScale := (normalize (DensePoly.positivePseudoDiv sign a b).remainder).fst } = true) (hterminal : ∀ (a b : DensePoly D), b ≠ 0 → (DensePoly.positivePseudoDiv sign a b).remainder.isZero = true → sign (DensePoly.positivePseudoDiv sign a b).multiplier = 1 ∧ subIsZero (DensePoly.scale (DensePoly.positivePseudoDiv sign a b).multiplier a) ((DensePoly.positivePseudoDiv sign a b).quotient * b) = true) (p f : DensePoly D) (initial : RemainderStep D) (hp : p ≠ 0) (fuel : Nat) (prev cur : DensePoly D) (chain : Array (DensePoly D)) (steps : Array (RemainderStep D)) (h : Prefix sign p f initial chain steps) (hprev : chain.getD (chain.size - 2) 0 = prev) (hcur : chain.getD (chain.size - 1) 0 = cur) (hc : cur ≠ 0) (hfuel : cur.size ≤ fuel) (hcapacity : chain.size + cur.size - 1 ≤ p.size) : have result := buildAux sign normalize fuel prev cur chain steps; check sign p f { chain := result.fst, degrees := Array.map' DensePoly.natDegree result.fst, initial := initial, steps := result.snd.fst, terminal := result.snd.snd } = true

The actual array loop preserves its established prefix and finishes with accepted terminal evidence. The hypotheses are mathematical laws of the backend, not arguments to the executable producer or arithmetic operations.

theorem Hex.Endpoint.signAt_bounds {D : Type u} {E : Type v} [Zero D] [DecidableEq D] (sign : D → Int) (endpointSigns : EndpointSigns D E) (hsign : ∀ (c : D), -1 ≤ sign c ∧ sign c ≤ 1) (heval : ∀ (p : DensePoly D) (x : E), -1 ≤ endpointSigns.evalSign p x ∧ endpointSigns.evalSign p x ≤ 1) (p : DensePoly D) (endpoint : Endpoint E) : -1 ≤ signAt sign endpointSigns p endpoint ∧ signAt sign endpointSigns p endpoint ≤ 1

Finite endpoint evaluation signs and coefficient signs in [-1,1] also give bounded infinity signs, including the negative-infinity degree-parity correction.

theorem Hex.TarskiCertificate.signs_bounded {D : Type u} {E : Type v} [Zero D] [DecidableEq D] (sign : D → Int) (endpointSigns : EndpointSigns D E) (hvalues : ∀ (p : DensePoly D) (e : Endpoint E), -1 ≤ Endpoint.signAt sign endpointSigns p e ∧ Endpoint.signAt sign endpointSigns p e ≤ 1) (chain : Array (DensePoly D)) (endpoint : Endpoint E) : ((signs sign endpointSigns chain endpoint).all fun (s : Int) => decide (-1 ≤ s) && decide (s ≤ 1)) = true

Endpoint operations with three-valued signs produce bounded sign arrays.

theorem Hex.TarskiCertificate.certify_checks {D : Type u} {E : Type v} {Ctx : Type w} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [NatCast D] [Neg D] [DecidableEq E] [DecidableEq Ctx] (sign : D → Int) (endpointSigns : EndpointSigns D E) (normalize : DensePoly D → D × DensePoly D) (hchains : ∀ (p g : DensePoly D), p ≠ 0 → SignedRemainderChain.check sign p g (SignedRemainderChain.build sign normalize p g) = true) (hvalues : ∀ (p : DensePoly D) (e : Endpoint E), -1 ≤ Endpoint.signAt sign endpointSigns p e ∧ Endpoint.signAt sign endpointSigns p e ≤ 1) (context : Ctx) (p g : DensePoly D) (a b : Endpoint E) (cert : TarskiCertificate D E Ctx) (hcert : certify sign endpointSigns normalize context p g a b = some cert) : check sign endpointSigns context p g a b cert.value cert = true

The shared producer's complete certificate passes replay whenever its chain backend and endpoint sign operations satisfy their established laws. Literal inputs, context, endpoints, signs and variations are checked without alteration.