def Hex.DensePoly.pointFactor {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a : R) : DensePoly R

The monic linear factor vanishing at a.

Equations

• Hex.DensePoly.pointFactor a = Hex.DensePoly.ofList [0 - a, 1]

theorem Hex.DensePoly.pointFactor_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a : R) : pointFactor a = monomial 1 1 - C a

The point factor is x - a.

theorem Hex.DensePoly.pointFactor_eval_at {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a x : R) : (pointFactor a).eval x = x - a

Evaluating the point factor at x gives x - a.

@[simp]

theorem Hex.DensePoly.pointFactor_eval {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a : R) : (pointFactor a).eval a = 0

The point factor vanishes at its defining point.

theorem Hex.DensePoly.pointFactor_size {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a : R) (hone : 1 ≠ 0) : (pointFactor a).size = 2

Over a nontrivial ring, a point factor has size two.

theorem Hex.DensePoly.pointFactor_monic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a : R) : (pointFactor a).Monic

Every point factor is monic, including over the trivial ring.

inductive Hex.DensePoly.PointNode (R : Type u) [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) : List R → DensePoly R → Type u

Internal balanced remainder-tree shape, indexed by its exact point sequence and product polynomial. Public clients use it only through opaque plans.

• leaf {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {mul : MulPlan R} (a : R) : PointNode R mul [a] (pointFactor a)
• branch {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {mul : MulPlan R} {leftPoints rightPoints : List R} {leftPoly rightPoly : DensePoly R} (left : PointNode R mul leftPoints leftPoly) (right : PointNode R mul rightPoints rightPoly) (leftPlan rightPlan : DivPlan R) (leftZero : ∀ (a : R), a ∈ leftPoints → leftPlan.divisor.eval a = 0) (rightZero : ∀ (a : R), a ∈ rightPoints → rightPlan.divisor.eval a = 0) : PointNode R mul (leftPoints ++ rightPoints) (mulWith mul leftPoly rightPoly)

def Hex.DensePoly.PointNode.CapacitySafe {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] {mul : MulPlan R} {points : List R} {poly : DensePoly R} : PointNode R mul points poly → Prop

The cached child plans have the exact divisor sizes and sibling capacities needed by a bounded remainder-tree traversal.

Equations

• One or more equations did not get rendered due to their size.
• (Hex.DensePoly.PointNode.leaf a).CapacitySafe = True

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

An opaque reusable multipoint-evaluation plan.

• mulData : Hex.DensePoly.MulPlan R
• pointsData : Array R
• nodeData : Option ((poly : Hex.DensePoly R) × { node : Hex.DensePoly.PointNode R (mulData self) (pointsData self).toList poly // node.CapacitySafe })

def Hex.DensePoly.EvalPlan.build {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) (points : Array R) : EvalPlan R

Build the point-product tree and all finite-capacity reciprocal plans.

Equations

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

def Hex.DensePoly.EvalPlan.points {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : EvalPlan R) : Array R

The planned point sequence.

Equations

• plan.points = Hex.DensePoly.EvalPlan.pointsData✝ plan

@[simp]

theorem Hex.DensePoly.EvalPlan.points_build {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) (points : Array R) : (build mul points).points = points

Building an evaluation plan preserves the supplied point sequence.

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

Number of planned points.

Equations

• plan.size = plan.points.size

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

Lawful multiplication plan used by the cached tree.

Equations

• plan.mulPlan = Hex.DensePoly.EvalPlan.mulData✝ plan

def Hex.DensePoly.EvalPlan.cachedNode {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : EvalPlan R) : Option ((poly : DensePoly R) × PointNode R plan.mulPlan plan.points.toList poly)

The cached indexed tree, when the point sequence and coefficient ring are nondegenerate.

Equations

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

theorem Hex.DensePoly.EvalPlan.cachedNode_build_isSome {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (mul : MulPlan R) (points : Array R) (hone : 1 ≠ 0) (hne : points.toList ≠ []) : (build mul points).cachedNode.isSome = true

A nonempty point sequence over a nontrivial ring has a cached node.

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

Rebuild the observational leaf-and-root product-tree view. Constructing an evaluation plan does not eagerly recompute this redundant product tree.

Equations

• plan.treeView = Hex.DensePoly.ProductTree.build plan.mulPlan (Array.map Hex.DensePoly.pointFactor plan.points)

noncomputable def Hex.DensePoly.EvalPlan.eval {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : EvalPlan R) (f : DensePoly R) : Array R

Specification of multipoint evaluation. The compiled implementation below replaces this direct map by the cached remainder tree.

Equations

• plan.eval f = Array.map (fun (x : R) => f.eval x) plan.points

@[simp]

theorem Hex.DensePoly.EvalPlan.size_eval {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : EvalPlan R) (f : DensePoly R) : (plan.eval f).size = plan.size

Evaluation preserves the planned point count.

@[simp]

theorem Hex.DensePoly.EvalPlan.size_points {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : EvalPlan R) : plan.points.size = plan.size

The points accessor has the advertised plan size.

theorem Hex.DensePoly.EvalPlan.eval_eq_map {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : EvalPlan R) (f : DensePoly R) : plan.eval f = Array.map (fun (x : R) => f.eval x) plan.points

Semantic expansion of the evaluation specification.

def Hex.DensePoly.EvalPlan.evalImpl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : EvalPlan R) (f : DensePoly R) : Array R

Executable cached remainder-tree evaluation. Oversized inputs and the degenerate ring use direct Horner evaluation, exactly as specified.

Equations

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

theorem Hex.DensePoly.EvalPlan.eval_eq_impl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : EvalPlan R) (f : DensePoly R) : plan.eval f = plan.evalImpl f

The cached implementation agrees exactly with direct evaluation.

@[csimp]

theorem Hex.DensePoly.EvalPlan.eval_csimp : @eval = @evalImpl

Compile multipoint evaluation through the cached remainder tree.

theorem Hex.DensePoly.EvalPlan.get_eval {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : EvalPlan R) (f : DensePoly R) (i : Nat) (hi : i < plan.size) : (plan.eval f)[i] = f.eval plan.points[i]

Every output entry is evaluation at the corresponding planned point.