theorem Hex.DensePoly.Monic.neOfOneNe {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {p : DensePoly R} (hp : p.Monic) (hone : 1 ≠ 0) : p ≠ 0

A monic polynomial over a nontrivial commutative ring is nonzero.

theorem Hex.DensePoly.Monic.mul {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {p q : DensePoly R} (hp : p.Monic) (hq : q.Monic) : (p * q).Monic

A product of monic polynomials over a commutative ring is monic.

def Hex.DensePoly.treeSplit (n : Nat) : Nat

Root split used by adjacent-pair product levels: the largest power of two strictly below n.

Equations

• Hex.DensePoly.treeSplit n = 2 ^ (n - 1).log2

theorem Hex.DensePoly.treeSplit_pos (n : Nat) : 0 < treeSplit n

The adjacent-pair tree split is positive.

theorem Hex.DensePoly.treeSplit_lt (n : Nat) (hn : 2 ≤ n) : treeSplit n < n

For at least two leaves, the tree split is strictly smaller than the leaf count.

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

An opaque balanced product tree with a cached root and on-demand levels.

• planData : Hex.DensePoly.MulPlan R
• leafData : Array (Hex.DensePoly R)
• rootData : Hex.DensePoly R

def Hex.DensePoly.ProductTree.build {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (leaves : Array (DensePoly R)) : ProductTree R

Build a balanced product tree without retaining intermediate levels. The empty tree has root 1 and one singleton level containing that root.

Equations

• Hex.DensePoly.ProductTree.build plan leaves = { planData := plan, leafData := leaves, rootData := Hex.DensePoly.buildRoot✝ plan leaves.size leaves.toList }

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

The leaf sequence in its original order.

Equations

• tree.leaves = Hex.DensePoly.ProductTree.leafData✝ tree

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

Number of nonempty balanced levels, including the leaf and root levels.

Equations

• tree.levelCount = if (Hex.DensePoly.ProductTree.leafData✝ tree).size ≤ 1 then 1 else ((Hex.DensePoly.ProductTree.leafData✝ tree).size - 1).log2 + 2

def Hex.DensePoly.ProductTree.plan {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : ProductTree R) : MulPlan R

Lawful multiplication plan used to build the tree.

Equations

• tree.plan = Hex.DensePoly.ProductTree.planData✝ tree

def Hex.DensePoly.ProductTree.level? {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : ProductTree R) (i : Nat) : Option (Array (DensePoly R))

A balanced level reconstructed from the leaves, from leaves upward. The empty tree has the singleton level [1].

Equations

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

def Hex.DensePoly.ProductTree.root {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : ProductTree R) : DensePoly R

The product represented by the root node.

Equations

• tree.root = Hex.DensePoly.ProductTree.rootData✝ tree

def Hex.DensePoly.ProductTree.nodeLeaves {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : ProductTree R) (level index : Nat) : Array (DensePoly R)

The ordered leaf block represented by a node. Invalid level/node pairs represent the empty block; use nodeProduct? when validity matters.

Equations

• tree.nodeLeaves level index = (Hex.DensePoly.ProductTree.leafData✝ tree).extract (index * 2 ^ level) (min (Hex.DensePoly.ProductTree.leafData✝ tree).size (index * 2 ^ level + 2 ^ level))

def Hex.DensePoly.ProductTree.nodeProduct? {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : ProductTree R) (level index : Nat) : Option (DensePoly R)

Product represented by a valid balanced node. The observation is semantic: it folds exactly that node's leaf block, independently of the internal level layout.

Equations

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

theorem Hex.DensePoly.ProductTree.nodeProduct?_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (tree : ProductTree R) (level index : Nat) (p : DensePoly R) (h : tree.nodeProduct? level index = some p) : p = Array.foldl (fun (acc q : DensePoly R) => mulWith tree.plan acc q) 1 (tree.nodeLeaves level index)

Every observed node product is the planned product of precisely its represented leaf block.

@[simp]

theorem Hex.DensePoly.ProductTree.leaves_build {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (leaves : Array (DensePoly R)) : (build plan leaves).leaves = leaves

Building preserves the supplied leaf sequence.

theorem Hex.DensePoly.ProductTree.root_build {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (leaves : Array (DensePoly R)) : (build plan leaves).root = List.foldl (fun (acc p : DensePoly R) => mulWith plan acc p) 1 leaves.toList

The root is the planned product of all leaves in order.

theorem Hex.DensePoly.ProductTree.root_build_eq_foldl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (leaves : Array (DensePoly R)) : (build plan leaves).root = Array.foldl (fun (acc p : DensePoly R) => acc * p) 1 leaves

The root is independent of the selected lawful multiplication kernel.