structure Hex.PRSResult (R : Type u) [Zero R] [DecidableEq R] : Type u

Executable result of a degree-ordered Brown PRS run.

scale belongs to the ordered chain. In particular, subresultantRun does not record whether it swapped its arguments, so this structure alone is not a caller-order-sensitive resultant; use resultant for that value.

• chain : Array (DensePoly R)

  Brown's nonzero G₁, …, Gₖ, excluding the generated terminal zero.

• scale : R

  Corrected terminal principal-subresultant scalar hₖ.

def Hex.DensePoly.negOnePow {R : Type u} [Zero R] [One R] [Sub R] (n : Nat) : R

The ring element (-1)^n, expressed using only Zero, One, and Sub.

Equations

• Hex.DensePoly.negOnePow n = if n % 2 = 0 then 1 else 0 - 1

theorem Hex.DensePoly.negOnePow_eq_sign {S : Type u} [Zero S] [One S] [Sub S] (n : Nat) : negOnePow n = SubresultantMinor.sign n

The executable Brown sign is the local determinant's alternating sign.

theorem Hex.DensePoly.negOnePow_ne_zero {S : Type u} [Lean.Grind.CommRing S] (h1 : 1 ≠ 0) (n : Nat) : negOnePow n ≠ 0

Brown signs are nonzero in every nontrivial commutative ring.

def Hex.DensePoly.BrownLaw {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (prev curr : DensePoly R) (hPrev : R) : Nat → Prop

The exactness and nonzero obligations for every reachable Brown worker state. A valid state must terminate naturally before its fuel reaches zero; the adjacent polynomials have strictly decreasing size, the current and successor scales are nonzero, both scalar divisions reconstruct their numerators, the Brown divisor and quotient are nonzero, and the successor is valid.

Equations

• One or more equations did not get rendered due to their size.
• prev.BrownLaw curr hPrev 0 = False

def Hex.DensePoly.BrownInv {R : Type u} [Zero R] [Lean.Grind.CommRing R] [DecidableEq R] (f g prev curr : DensePoly R) (hPrev : R) : Prop

Integral subresultant-family invariant for one recursive Brown state. It keeps all accumulated factors cross-multiplied in the coefficient ring.

Equations

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

theorem Hex.DensePoly.BrownInv.nextScale {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g prev curr : DensePoly S) (hPrev : S) (hinv : f.BrownInv g prev curr hPrev) : have delta := prev.size - curr.size; have hCurr := divExp curr.leadingCoeff hPrev delta; hCurr = (Subresultant.poly (curr.size - 1) f g).coeff (curr.size - 1) ∧ hCurr ≠ 0 ∧ powNat curr.leadingCoeff delta = powNat hPrev (delta - 1) * hCurr

The invariant identifies the next Brown scale with the leading principal coefficient of the original-pair subresultant and proves its exact quotient law inside the base ring.

theorem Hex.DensePoly.brownInv_init {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g : DensePoly S) (hg : g ≠ 0) (hgf : g.size ≤ f.size) (hp : (f.pseudoDivMod g).snd ≠ 0) : have delta := f.size - g.size; have h₂ := powNat g.leadingCoeff delta; have g₃ := scale (negOnePow (delta + 1)) (f.pseudoDivMod g).snd; f.BrownInv g g g₃ h₂

The signed first pseudo-remainder establishes the integral invariant for the first recursive Brown state.

theorem Hex.DensePoly.BrownInv.factor {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g prev curr : DensePoly S) (hPrev : S) (hinv : f.BrownInv g prev curr hPrev) (hp : (prev.pseudoDivMod curr).snd ≠ 0) : have delta := prev.size - curr.size; have p := (prev.pseudoDivMod curr).snd; have divisor := negOnePow (delta + 1) * prev.leadingCoeff * powNat hPrev delta; have next := p.divScalar divisor; divisor ≠ 0 ∧ p = scale divisor next ∧ next ≠ 0 ∧ next = Subresultant.poly (curr.size - 2) f g

At a nonterminal invariant state, the pseudo-remainder has the exact Brown factor and its quotient is the adjacent original-pair subresultant.

theorem Hex.DensePoly.BrownInv.step {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g prev curr : DensePoly S) (hPrev : S) (hinv : f.BrownInv g prev curr hPrev) (hp : (prev.pseudoDivMod curr).snd ≠ 0) : have delta := prev.size - curr.size; have hCurr := divExp curr.leadingCoeff hPrev delta; have p := (prev.pseudoDivMod curr).snd; have divisor := negOnePow (delta + 1) * prev.leadingCoeff * powNat hPrev delta; have next := p.divScalar divisor; f.BrownInv g curr next hCurr

One nonterminal Brown step preserves the integral original-pair subresultant invariant.

def Hex.DensePoly.subresultantAux {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (prev curr : DensePoly R) (hPrev : R) (chain : Array (DensePoly R)) : Nat → PRSResult R

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

prev, curr, and hPrev are Gᵢ₋₁, Gᵢ, and hᵢ₋₁. A valid state has nonzero adjacent polynomials of strictly decreasing degree and a nonzero scale. The zero checks preserve the public nonzero-only chain convention even on junk coefficient structures.

Equations

• One or more equations did not get rendered due to their size.
• prev.subresultantAux curr hPrev chain 0 = { chain := chain, scale := hPrev }

def Hex.DensePoly.subresultantOrderedFuel {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (f g : DensePoly R) (fuel : Nat) : PRSResult R

Brown's recurrence for two nonzero inputs already ordered by decreasing dense degree, with an explicit proof-audit fuel parameter.

Equations

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

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

Brown's recurrence for two nonzero inputs already ordered by decreasing dense degree. One fuel unit per possible degree, plus the terminal step, is sufficient on a lawful exact-division domain.

Equations

• f.subresultantOrdered g = f.subresultantOrderedFuel g (g.size + 1)

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

Total Brown run. Zero inputs are omitted; two nonzero inputs are ordered by decreasing dense degree before entering subresultantOrdered.

Equations

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

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

Brown's nonzero subresultant pseudo-remainder sequence.

Equations

• f.subresultantChain g = (f.subresultantRun g).chain

theorem Hex.DensePoly.subresultantOrdered_brownLaw {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g : DensePoly S) (hg : g ≠ 0) (hgf : g.size ≤ f.size) : have delta := f.size - g.size; have h₂ := powNat g.leadingCoeff delta; have p := (f.pseudoDivMod g).snd; if p.isZero = true then h₂ ≠ 0 else have g₃ := scaleImpl (negOnePow (delta + 1)) p; g₃ ≠ 0 ∧ g.BrownLaw g₃ h₂ (g.size + 1)

Ordered nonzero inputs establish every nonzero-denominator and exactness obligation recorded by BrownLaw, including the unreachability of the junk zero-quotient branch.

theorem Hex.DensePoly.subresultantOrderedFuel_eq {S : Type u} [Zero S] [DecidableEq S] [One S] [Add S] [Sub S] [Mul S] [Div S] (f g : DensePoly S) (hg : g ≠ 0) (extra : Nat) : f.subresultantOrderedFuel g (g.size + 1 + extra) = f.subresultantOrdered g

Adding fuel beyond the public ordered-run budget leaves the result unchanged. This is a structural consequence of strict remainder-size descent and needs no divisibility laws.

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

Extract the resultant value from an ordered nonzero Brown run. The corrected terminal scale is returned exactly when the last stored term is a nonzero constant.

Equations

• f.resultantOrdered g = if ((f.subresultantOrdered g).chain.getD ((f.subresultantOrdered g).chain.size - 1) 0).size = 1 then (f.subresultantOrdered g).scale else 0

theorem Hex.DensePoly.resultantOrdered_eq_coeffMinor {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g : DensePoly S) (hf : f ≠ 0) (hg : g ≠ 0) (hgf : g.size ≤ f.size) : f.resultantOrdered g = Subresultant.coeffMinor 0 0 f g

For ordered nonzero inputs, Brown's corrected terminal value is the zeroth generalized subresultant coefficient.

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

Executable polynomial resultant with default formal-degree conventions.

Zero polynomials are treated as degree zero, so two constants (including two zeros) have resultant one. Reversed nonzero inputs are ordered for the Brown run and receive the standard degree-product sign.

Equations

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

@[simp]

theorem Hex.DensePoly.subresultantChain_zero_zero {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] : subresultantChain 0 0 = #[]

Both zero inputs produce the empty nonzero chain.

theorem Hex.DensePoly.subresultantChain_zero_right {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (f : DensePoly R) (hf : f ≠ 0) : f.subresultantChain 0 = #[f]

A nonzero left input paired with zero is the singleton chain.

theorem Hex.DensePoly.subresultantChain_zero_left {R : Type u} [Zero R] [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R] (g : DensePoly R) (hg : g ≠ 0) : subresultantChain 0 g = #[g]

A nonzero right input paired with zero is the singleton chain.

theorem Hex.DensePoly.subresultantChain_ne_zero {S : Type u} [Zero S] [DecidableEq S] [One S] [Add S] [Sub S] [Mul S] [Div S] (f g p : DensePoly S) (hp : p ∈ f.subresultantChain g) : p ≠ 0

Every stored term is nonzero. This follows from the worker's explicit zero guards and needs no divisibility laws.

theorem Hex.DensePoly.subresultantChain_size_strict {S : Type u} [Zero S] [DecidableEq S] [One S] [Add S] [Sub S] [Mul S] [Div S] (f g : DensePoly S) (i : Nat) (hi : 1 ≤ i) (hnext : i + 1 < (f.subresultantChain g).size) : ((f.subresultantChain g).getD (i + 1) 0).size < ((f.subresultantChain g).getD i 0).size

After the possibly equal-degree ordered inputs, stored degrees strictly decrease.

theorem Hex.DensePoly.subresultantChain_size_le {S : Type u} [Zero S] [DecidableEq S] [One S] [Add S] [Sub S] [Mul S] [Div S] (f g : DensePoly S) (hf : f ≠ 0) (hg : g ≠ 0) : (f.subresultantChain g).size ≤ min f.natDegree g.natDegree + 2

The nonzero Brown chain stores at most two inputs plus one term for every possible degree at or below the smaller input degree.