24.6. The extended chain🔗

Gcd consumers need more than the chain entries: to build a Bezout certificate they need the transformation that produced each entry. The extended chain runs the same Brown recurrence and additionally carries a cofactor pair through every pseudo-scaling and every exact scalar division, so each stored triple is a Bezout identity for the caller's two inputs.

def

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

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

def

Hex.DensePoly.subresultantChainExt.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) :
  Array (Hex.DensePoly R × Hex.DensePoly R × Hex.DensePoly R)
Hex.DensePoly.subresultantChainExt.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) :
  Array
    (Hex.DensePoly R ×
      Hex.DensePoly R × Hex.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.

The third components are the plain chain, unchanged. The extension adds information; it does not alter the resultant or discriminant contracts.

theorem

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

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

Correctness is packaged as one law with two halves. The Bezout half applies to every stored entry. The exactness half is what makes the executable divisions legitimate: at each divided step, both transformation numerators are the Brown scalar times the stored quotients, so the division the executable performs is exact rather than truncating.

def

Hex.DensePoly.SubresultantExt.Law.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R)
  (chain : Array (Hex.DensePoly.SubresultantExt.Entry R)) : Prop
Hex.DensePoly.SubresultantExt.Law.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R)
  (chain :
    Array
      (Hex.DensePoly.SubresultantExt.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.

theorem

Hex.DensePoly.subresultantChainExt_law.{u} {S : Type u}
  [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [Hex.ExactDivLaws S]
  (f g : Hex.DensePoly S) :
  Hex.DensePoly.SubresultantExt.Law f g (f.subresultantChainExt g)
Hex.DensePoly.subresultantChainExt_law.{u}
  {S : Type u} [Lean.Grind.CommRing S]
  [DecidableEq S] [Div S]
  [Hex.ExactDivLaws S]
  (f g : Hex.DensePoly S) :
  Hex.DensePoly.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.

The two halves are also available separately:

theorem

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

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

theorem

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

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

Both gcd libraries read the terminal entry for a deterministic fallback that needs a Bezout pair with no modulus, and so cannot go through the modular route. HexPolyZGcd turns it into a CoprimeWitness.constant; HexMvGcd turns it into a splitBezout certificate.