structure Hex.DensePoly.MonicLeaf (R : Type u) [DecidableEq R] [Lean.Grind.CommRing R] : Type u

A nonzero monic polynomial suitable as a remainder-tree leaf.

• poly : DensePoly R

  Leaf divisor.

• monic : self.poly.Monic

  The divisor is monic.

• ne : self.poly ≠ 0

  The divisor is nonzero.

inductive Hex.DensePoly.RemainderSpec {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (origin : DensePoly R) : List (MonicLeaf R) → List (DensePoly R) → Prop

RemainderSpec origin leaves results states that results contains, in order, the canonical-size remainder of origin at every corresponding leaf. The divisibility and size conditions uniquely characterize a monic remainder.

• nil {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {origin : DensePoly R} : origin.RemainderSpec [] []
• cons {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {origin : DensePoly R} {leaf : MonicLeaf R} {r : DensePoly R} {leaves : List (MonicLeaf R)} {results : List (DensePoly R)} (head : leaf.poly ∣ origin - r ∧ r.size ≤ leaf.poly.size - 1) (tail : origin.RemainderSpec leaves results) : origin.RemainderSpec (leaf :: leaves) (r :: results)

structure Hex.DensePoly.RemainderTree (R : Type u) [DecidableEq R] [Lean.Grind.CommRing R] : Type u

An opaque balanced remainder tree whose root has fixed reciprocal capacity and whose proper nodes use the degree of their sibling subtree.

• mulData : Hex.DensePoly.MulPlan R
• capacityData : Nat
• leavesData : Array (Hex.DensePoly.MonicLeaf R)
• nodeData : Option (RemainderNode R)
• nodeLeaves (node : RemainderNode R) : nodeData self = some node → RemainderNode.leaves node = (leavesData self).toList
• nodeWellFormed (node : RemainderNode R) : nodeData self = some node → RemainderNode.WellFormed node
• nodeCapacity (node : RemainderNode R) : nodeData self = some node → (RemainderNode.plan node).capacity = capacityData self
• nodeDegree (node : RemainderNode R) : nodeData self = some node → (RemainderNode.root node).poly.size - 1 = leafDegreeSum (leavesData self).toList
• noNodeLeaves : nodeData self = none → (leavesData self).toList = []

def Hex.DensePoly.RemainderTree.build {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) (capacity : Nat) (leaves : Array (MonicLeaf R)) (hone : 1 ≠ 0) : RemainderTree R

Build a cached remainder tree. capacity is the reciprocal capacity of the root; every proper node derives the exact worst-case capacity it needs from its sibling subtree. The empty leaf sequence is represented without an internal root.

Equations

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

def Hex.DensePoly.RemainderTree.leaves {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : RemainderTree R) : Array (DensePoly R)

Leaf divisors in their original order.

Equations

• tree.leaves = Array.map (fun (x : Hex.DensePoly.MonicLeaf R) => x.poly) (Hex.DensePoly.RemainderTree.leavesData✝ tree)

def Hex.DensePoly.RemainderTree.entries {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : RemainderTree R) : Array (MonicLeaf R)

Proof-carrying leaf entries in their original order.

Equations

• tree.entries = Hex.DensePoly.RemainderTree.leavesData✝ tree

def Hex.DensePoly.RemainderTree.size {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : RemainderTree R) : Nat

Number of leaf divisors.

Equations

• tree.size = (Hex.DensePoly.RemainderTree.leavesData✝ tree).size

def Hex.DensePoly.RemainderTree.capacity {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : RemainderTree R) : Nat

Reciprocal capacity cached at the root.

Equations

• tree.capacity = Hex.DensePoly.RemainderTree.capacityData✝ tree

def Hex.DensePoly.RemainderTree.rootDegree {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : RemainderTree R) : Nat

Degree of the root product, computed as the sum of the leaf degrees.

Equations

• tree.rootDegree = Hex.DensePoly.leafDegreeSum✝ (Hex.DensePoly.RemainderTree.leavesData✝ tree).toList

def Hex.DensePoly.RemainderTree.remainders? {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : RemainderTree R) (p : DensePoly R) : Option (Array (DensePoly R))

Compute all leaf remainders with the cached reciprocal plans. Returns none exactly when the input needs more reciprocal precision than the root capacity. Proper-node capacities are sufficient by construction.

Equations

• tree.remainders? p = match Hex.DensePoly.RemainderTree.nodeData✝ tree with | none => some #[] | some node => Option.map List.toArray (Hex.DensePoly.RemainderTree.runNode?✝ node p)

theorem Hex.DensePoly.RemainderTree.remainders?_isSome_of_capacity {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : RemainderTree R) (p : DensePoly R) (hcap : p.size ≤ tree.rootDegree + tree.capacity) : (tree.remainders? p).isSome = true

A caller-supplied root capacity covering the input above the root degree makes the entire traversal succeed. Every proper-node guard follows from the sibling-degree capacities recorded by construction.

theorem Hex.DensePoly.RemainderTree.remainders?_sound {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : RemainderTree R) (p : DensePoly R) (results : Array (DensePoly R)) (h : tree.remainders? p = some results) : p.RemainderSpec tree.entries.toList results.toList

Every successful traversal returns, in leaf order, the canonical-size remainder of the input modulo each leaf polynomial.