@[reducible, inline]

abbrev Hex.DensePoly.SubresultantExt.Entry (R : Type u) [Zero R] [DecidableEq R] : Type u

One extended Brown-chain entry (u, v, s), representing u*f + v*g = s.

Equations

• Hex.DensePoly.SubresultantExt.Entry R = (Hex.DensePoly R × Hex.DensePoly R × Hex.DensePoly R)

@[inline]

def Hex.DensePoly.SubresultantExt.value {R : Type u} [Zero R] [DecidableEq R] (e : Entry R) : DensePoly R

The polynomial component of an extended Brown-chain entry.

Equations

• Hex.DensePoly.SubresultantExt.value e = e.snd.snd

@[inline]

def Hex.DensePoly.SubresultantExt.numerator {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] [Sub R] (a : R) (q prev curr : DensePoly R) : DensePoly R

The numerator update for one transformation cofactor in a pseudo-division step: lc(curr)^d * prevCofactor - quotient * currCofactor.

Equations

• Hex.DensePoly.SubresultantExt.numerator a q prev curr = Hex.DensePoly.scaleImpl a prev - q * curr

def Hex.DensePoly.subresultantAuxExt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (prev curr : DensePoly R) (hPrev : R) (prevU prevV currU currV : DensePoly R) (chain : Array (SubresultantExt.Entry R)) : Nat → Array (SubresultantExt.Entry R)

Fuel-bounded extended Brown recurrence after the initial pseudo-division.

The polynomial branch decisions and polynomial successor are byte-for-byte the same expressions used by subresultantAux; the additional divisions update only the two transformation cofactors.

Equations

• One or more equations did not get rendered due to their size.
• prev.subresultantAuxExt curr hPrev prevU prevV currU currV chain 0 = chain

def Hex.DensePoly.subresultantOrderedExt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (f g fU fV gU gV : DensePoly R) : Array (SubresultantExt.Entry R)

Extended Brown recurrence for two nonzero, degree-ordered inputs, supplied with their transformation cofactors relative to the caller's inputs.

Equations

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

def Hex.DensePoly.subresultantChainExt {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (f g : DensePoly R) : Array (DensePoly R × DensePoly R × DensePoly R)

Brown's nonzero subresultant chain together with a caller-order-sensitive Bezout representation for every stored entry.

Zero inputs follow subresultantChain: they are omitted, and the one remaining input receives its evident unit cofactor. Two nonzero inputs are ordered by decreasing dense degree; equal-degree inputs retain caller order.

Equations

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

theorem Hex.DensePoly.subresultantChainExt_values {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (f g : DensePoly R) : Array.map SubresultantExt.value (f.subresultantChainExt g) = f.subresultantChain g

Forgetting the two cofactors recovers subresultantChain, including its input ordering and all zero-input conventions.

def Hex.DensePoly.SubresultantExt.brownScale {R : Type u} [Zero R] [DecidableEq R] [One R] [Mul R] [Div R] (chain : Array (Entry R)) : Nat → R

Brown's accumulated principal-subresultant scale associated to a stored chain entry. The value at index 1 is the ordered worker's initial h₂; later values apply the unchanged divExp recurrence.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.SubresultantExt.brownScale chain 0 = 1

def Hex.DensePoly.SubresultantExt.CofactorStep {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (chain : Array (Entry R)) (i : Nat) : Prop

Exact coefficientwise divisibility at a noninitial Brown step.

Index 2 is the signed first pseudo-remainder and involves no exact scalar division. Every entry at index at least 3 is obtained from the two preceding entries by the scalar division recorded here.

Equations

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

def Hex.DensePoly.SubresultantExt.Law {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (f g : DensePoly R) (chain : Array (Entry R)) : Prop

Algebraic contract of an extended Brown chain: every stored triple is a Bezout identity for the caller's inputs, and every post-initial transformation row is coefficientwise divisible by the exact Brown scalar before division.

Equations

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

theorem Hex.DensePoly.subresultantChainExt_law {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g : DensePoly S) : SubresultantExt.Law f g (f.subresultantChainExt g)

The extended Brown recurrence has exact transformation rows and every stored entry satisfies its caller-order-sensitive Bezout identity.

theorem Hex.DensePoly.subresultantChainExt_bezout {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g : DensePoly S) (e : SubresultantExt.Entry S) (he : e ∈ f.subresultantChainExt g) : e.fst * f + e.snd.fst * g = e.snd.snd

Every extended-chain entry reconstructs from the two caller inputs.

theorem Hex.DensePoly.subresultantChainExt_exact {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g : DensePoly S) (i : Nat) (hi : 3 ≤ i) (hbound : i < (f.subresultantChainExt g).size) : SubresultantExt.CofactorStep (f.subresultantChainExt g) i

At every divided Brown step, both transformation numerators reconstruct as the Brown scalar times the stored executable quotients.