structure Hex.RemainderStep (D : Type u) [Zero D] [DecidableEq D] : Type u

Positive scales and a literal quotient for a three-term identity.

• leftScale : D
• quotient : DensePoly D
• rightScale : D

structure Hex.SignedRemainderChain (D : Type u) [Zero D] [DecidableEq D] : Type u

A signed remainder chain, its initial reduction, and a separate terminal zero identity. A singleton chain has no terminal pair.

• chain : Array (DensePoly D)
• degrees : Array Nat

  Literal degree data for serialized certificates; replay checks it against the stored entries as well as checking strict degree descent.

• initial : RemainderStep D
• steps : Array (RemainderStep D)
• terminal : Option (D × DensePoly D)

@[instance_reducible]

instance Hex.instDecidableEqRemainderStep {E : Type u} [Zero E] [DecidableEq E] : DecidableEq (RemainderStep E)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.instDecidableEqSignedRemainderChain {E : Type u} [Zero E] [DecidableEq E] : DecidableEq (SignedRemainderChain E)

Equations

• One or more equations did not get rendered due to their size.

def Hex.SignedRemainderChain.normalizeId {D : Type u} [Zero D] [DecidableEq D] [One D] (p : DensePoly D) : D × DensePoly D

No content removal; useful for small generic interpretation probes. Unnormalized pseudo-remainder sequences can have exponential coefficient growth. Production backends should supply a proved positive normalization.

Equations

• Hex.SignedRemainderChain.normalizeId p = (1, p)

def Hex.SignedRemainderChain.buildAux {D : Type u} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [Neg D] (sign : D → Int) (normalize : DensePoly D → D × DensePoly D) : Nat → DensePoly D → DensePoly D → Array (DensePoly D) → Array (RemainderStep D) → Array (DensePoly D) × Array (RemainderStep D) × Option (D × DensePoly D)

Extend the chain using only positive-scaled pseudo-division. The internal bound comes from the original head degree. Under the normalization laws, strict degree descent reaches the terminal zero branch within that bound. The zero-fuel value lacks terminal evidence and cannot pass replay for a pair.

Equations

• One or more equations did not get rendered due to their size.
• Hex.SignedRemainderChain.buildAux sign normalize 0 x✝³ x✝² x✝¹ x✝ = (x✝¹, x✝, none)

theorem Hex.SignedRemainderChain.buildAux_complete {D : Type u} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul 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) (fuel : Nat) (prev cur : DensePoly D) (chain : Array (DensePoly D)) (steps : Array (RemainderStep D)) (hcur : cur ≠ 0) (bound : cur.size ≤ fuel) : (buildAux sign normalize fuel prev cur chain steps).snd.snd.isSome = true

The input-derived bound reaches a terminal zero identity when normalized nonzero remainders stay nonzero and do not increase stored size. This is an adequacy theorem for the actual recursive loop, separate from query semantics.

theorem Hex.SignedRemainderChain.buildAux_size {D : Type u} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul 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) (fuel : Nat) (prev cur : DensePoly D) (chain : Array (DensePoly D)) (steps : Array (RemainderStep D)) (hcur : cur ≠ 0) : (buildAux sign normalize fuel prev cur chain steps).fst.size ≤ chain.size + cur.size - 1

Strict size descent bounds the number of appended entries, including when an internal call is viewed at an arbitrary finite recursion depth.

def Hex.SignedRemainderChain.build {D : Type u} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [Neg D] [NatCast D] (sign : D → Int) (normalize : DensePoly D → D × DensePoly D) (p f : DensePoly D) : SignedRemainderChain D

Produce the signed chain of (p, f*p') after the mandatory initial reduction. Normalization is a total polynomial backend operation: its laws require a positive factor and preservation of the polynomial up to that factor. It supplies no coefficient-operation certificates or arithmetic budgets.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.SignedRemainderChain.build_terminal {D : Type u} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [Neg D] [NatCast D] (sign : D → Int) (normalize : DensePoly D → D × DensePoly D) (hnormalize : ∀ (r : DensePoly D), r ≠ 0 → (normalize r).snd ≠ 0 ∧ (normalize r).snd.size ≤ r.size) (hnext : ∀ (r : DensePoly D), r ≠ 0 → -(normalize r).snd ≠ 0 ∧ (-(normalize r).snd).size ≤ r.size) (p f : DensePoly D) (hp : p ≠ 0) (hr : (DensePoly.positivePseudoDiv sign (f * p.derivative) p).remainder.isZero = false) : (build sign normalize p f).terminal.isSome = true

A nonzero initial remainder reaches terminal evidence using exactly the head's internally computed degree bound.

theorem Hex.SignedRemainderChain.build_size {D : Type u} [Zero D] [DecidableEq D] [One D] [Add D] [Sub D] [Mul D] [Neg D] [NatCast D] (sign : D → Int) (normalize : DensePoly D → D × DensePoly D) (hnormalize : ∀ (r : DensePoly D), r ≠ 0 → (normalize r).snd ≠ 0 ∧ (normalize r).snd.size ≤ r.size) (hnext : ∀ (r : DensePoly D), r ≠ 0 → -(normalize r).snd ≠ 0 ∧ (-(normalize r).snd).size ≤ r.size) (p f : DensePoly D) (hp : p ≠ 0) : (build sign normalize p f).chain.size ≤ p.size

A produced chain has at most degree p + 1 entries for nonzero p.

def Hex.SignedRemainderChain.subIsZero {D : Type u} [Zero D] [DecidableEq D] [Sub D] (p q : DensePoly D) : Bool

Arithmetic identities test a zero difference. This is intentionally separate from the literal equality used for the head and context bindings.

Equations

• Hex.SignedRemainderChain.subIsZero p q = (p - q).isZero

def Hex.SignedRemainderChain.checkStep {D : Type u} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] (sign : D → Int) (a b c : DensePoly D) (s : RemainderStep D) : Bool

Check a positive three-term recurrence without performing division.

Equations

• One or more equations did not get rendered due to their size.

def Hex.SignedRemainderChain.check {D : Type u} [Zero D] [DecidableEq D] [Add D] [Sub D] [Mul D] [NatCast D] (sign : D → Int) (p f : DensePoly D) (cert : SignedRemainderChain D) : Bool

Literal finite replay of the initial reduction, degree evidence, all recurrences and the terminal zero identity. No gcd or chain producer runs.

Equations

• One or more equations did not get rendered due to their size.