From 01ec377a325cc63b622459a3cc9741d93ad5bbef Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 31 Aug 2026 06:18:57 +0000 Subject: [PATCH] fix(poly-fast): prove remainder capacities --- HexManual/Chapters/HexPolyFast.lean | 4 + HexPolyFast/Multipoint.lean | 165 ++++++++++++++++++------- HexPolyFast/RemainderTree.lean | 180 ++++++++++++++++++++++++++-- HexPolyFast/SPEC/hex-poly-fast.md | 6 +- 4 files changed, 300 insertions(+), 55 deletions(-) diff --git a/HexManual/Chapters/HexPolyFast.lean b/HexManual/Chapters/HexPolyFast.lean index 9ec1117fa..182b888d8 100644 --- a/HexManual/Chapters/HexPolyFast.lean +++ b/HexManual/Chapters/HexPolyFast.lean @@ -233,8 +233,12 @@ their sibling subtree. {docstring Hex.DensePoly.RemainderTree.build} +{docstring Hex.DensePoly.RemainderTree.rootDegree} + {docstring Hex.DensePoly.RemainderTree.remainders?} +{docstring Hex.DensePoly.RemainderTree.remainders?_isSome_of_capacity} + {docstring Hex.DensePoly.RemainderTree.remainders?_sound} {name}`Hex.DensePoly.EvalPlan` specializes the leaves to `x - a` and caches diff --git a/HexPolyFast/Multipoint.lean b/HexPolyFast/Multipoint.lean index d04b6a065..861d33bb7 100644 --- a/HexPolyFast/Multipoint.lean +++ b/HexPolyFast/Multipoint.lean @@ -97,13 +97,28 @@ inductive PointNode (R : Type u) [DecidableEq R] PointNode R mul (leftPoints ++ rightPoints) (mulWith mul leftPoly rightPoly) +/-- The cached child plans have the exact divisor sizes and sibling capacities +needed by a bounded remainder-tree traversal. -/ +def PointNode.CapacitySafe {mul : MulPlan R} : + {points : List R} → {poly : DensePoly R} → PointNode R mul points poly → Prop + | _, _, .leaf _ => True + | _, _, @PointNode.branch _ _ _ _ leftPoints rightPoints _ _ + left right leftPlan rightPlan _ _ => + left.CapacitySafe ∧ right.CapacitySafe ∧ + leftPlan.divisor.size = leftPoints.length + 1 ∧ + rightPlan.divisor.size = rightPoints.length + 1 ∧ + leftPlan.capacity = rightPoints.length ∧ + rightPlan.capacity = leftPoints.length + /-- A constructed node together with its monic product polynomial. -/ private structure BuiltNode (mul : MulPlan R) (points : List R) where poly : DensePoly R node : PointNode R mul points poly monic : poly.Monic ne : poly ≠ 0 + size_eq : poly.size = points.length + 1 evalZero : ∀ a, a ∈ points → poly.eval a = 0 + capacitySafe : node.CapacitySafe private def leafNode (mul : MulPlan R) (hone : (1 : R) ≠ 0) (a : R) : BuiltNode mul [a] := @@ -111,11 +126,13 @@ private def leafNode (mul : MulPlan R) (hone : (1 : R) ≠ 0) (a : R) : node := .leaf a monic := pointFactor_monic a ne := (pointFactor_monic a).neOfOneNe hone + size_eq := pointFactor_size a hone evalZero := by intro x hx simp only [List.mem_singleton] at hx subst x - exact pointFactor_eval a } + exact pointFactor_eval a + capacitySafe := True.intro } private def branchNode (mul : MulPlan R) (hone : (1 : R) ≠ 0) {leftPoints rightPoints : List R} @@ -124,6 +141,14 @@ private def branchNode (mul : MulPlan R) (hone : (1 : R) ≠ 0) let leftPlan := DivPlan.ofMonic mul left.poly left.monic left.ne rightPoints.length let rightPlan := DivPlan.ofMonic mul right.poly right.monic right.ne leftPoints.length let poly := mulWith mul left.poly right.poly + have hleftPos : 0 < left.poly.size := by rw [left.size_eq]; omega + have hrightPos : 0 < right.poly.size := by rw [right.size_eq]; omega + have hproduct := size_mul_of_top_ne left.poly right.poly hleftPos hrightPos (by + rw [leadingCoeff_eq_one_of_monic left.monic, + leadingCoeff_eq_one_of_monic right.monic] + have hzero : (Zero.zero : R) = 0 := rfl + rw [hzero, Lean.Grind.Semiring.one_mul] + exact hone) { poly node := .branch left.node right.node leftPlan rightPlan (by intro a ha; simpa [leftPlan] using left.evalZero a ha) @@ -138,6 +163,10 @@ private def branchNode (mul : MulPlan R) (hone : (1 : R) ≠ 0) rw [mulWith_eq] exact left.monic.mul right.monic · exact hone + size_eq := by + dsimp [poly] + rw [mulWith_eq, hproduct, left.size_eq, right.size_eq, List.length_append] + omega evalZero := by intro a ha dsimp [poly] @@ -145,7 +174,18 @@ private def branchNode (mul : MulPlan R) (hone : (1 : R) ≠ 0) rw [List.mem_append] at ha cases ha with | inl hleft => rw [left.evalZero a hleft]; grind - | inr hright => rw [right.evalZero a hright]; grind } + | inr hright => rw [right.evalZero a hright]; grind + capacitySafe := by + change left.node.CapacitySafe ∧ right.node.CapacitySafe ∧ + leftPlan.divisor.size = leftPoints.length + 1 ∧ + rightPlan.divisor.size = rightPoints.length + 1 ∧ + leftPlan.capacity = rightPoints.length ∧ + rightPlan.capacity = leftPoints.length + exact ⟨left.capacitySafe, right.capacitySafe, + (by simp [leftPlan, left.size_eq]), + (by simp [rightPlan, right.size_eq]), + (by simp [leftPlan]), + (by simp [rightPlan])⟩ } /-- Recursively build a count-balanced cached remainder tree. -/ private def buildNode (mul : MulPlan R) (hone : (1 : R) ≠ 0) : @@ -194,7 +234,8 @@ structure EvalPlan (R : Type u) [DecidableEq R] [Lean.Grind.CommRing R] where /-- Empty and trivial-ring plans use `none`; otherwise the type index ties every cached divisor to the exact public point sequence. -/ private nodeData : Option - (Sigma fun poly => PointNode R mulData pointsData.toList poly) + (Sigma fun poly => { node : PointNode R mulData pointsData.toList poly // + node.CapacitySafe }) namespace EvalPlan @@ -206,7 +247,7 @@ def build (mul : MulPlan R) (points : Array R) : EvalPlan R := else if hempty : points.toList = [] then none else let built := buildNode mul hone points.toList hempty - some ⟨built.poly, built.node⟩ } + some ⟨built.poly, ⟨built.node, built.capacitySafe⟩⟩ } /-- The planned point sequence. -/ def points (plan : EvalPlan R) : Array R := plan.pointsData @@ -226,14 +267,13 @@ def mulPlan (plan : EvalPlan R) : MulPlan R := plan.mulData nondegenerate. -/ def cachedNode (plan : EvalPlan R) : Option (Sigma fun poly => PointNode R plan.mulPlan plan.points.toList poly) := - plan.nodeData + plan.nodeData.map fun built => ⟨built.1, built.2.1⟩ /-- A nonempty point sequence over a nontrivial ring has a cached node. -/ theorem cachedNode_build_isSome (mul : MulPlan R) (points : Array R) (hone : (1 : R) ≠ 0) (hne : points.toList ≠ []) : (build mul points).cachedNode.isSome := by simp [cachedNode, mulPlan, build, hone, hne] - rfl /-- Rebuild the observational product-tree view. Constructing an evaluation plan does not eagerly build this redundant level representation. -/ @@ -260,64 +300,99 @@ theorem eval_eq_map (plan : EvalPlan R) (f : DensePoly R) : plan.eval f = plan.points.map (f.eval ·) := by rfl -/-- Reduce one parent remainder into a cached child node. The capacity guard -is executable defensive checking; plans built by `build` satisfy it throughout -the bounded traversal. -/ -private def reduceNode (parent : DensePoly R) (node : DivPlan R) : DensePoly R := - if hcap : quotientLength parent node.divisor ≤ node.capacity then - node.mod parent hcap - else - parent +/-- A divisor of size `degree + 1` needs at most `capacity` quotient +coefficients when the parent has size at most `degree + capacity`. -/ +private theorem quotientLength_le_capacity (parent : DensePoly R) + (node : DivPlan R) {degree capacity : Nat} + (hdivisor : node.divisor.size = degree + 1) + (hparent : parent.size ≤ degree + capacity) : + quotientLength parent node.divisor ≤ capacity := by + have hne : node.divisor.size ≠ 0 := by rw [hdivisor]; omega + by_cases hlt : parent.size < node.divisor.size + · simp [quotientLength_eq, hlt] + · rw [quotientLength_eq] + simp [hne, hlt] + rw [hdivisor] at hlt + omega /-- Reduction by a divisor vanishing at `a` preserves evaluation at `a`. -/ -private theorem eval_reduceNode (parent : DensePoly R) (node : DivPlan R) (a : R) +private theorem eval_mod (parent : DensePoly R) (node : DivPlan R) + (hcap : quotientLength parent node.divisor ≤ node.capacity) (a : R) (hzero : node.divisor.eval a = 0) : - (reduceNode parent node).eval a = parent.eval a := by - unfold reduceNode - split - · rename_i hcap - rw [node.mod_eq parent hcap] - simp only [eval_sub_ring, mulWith_eq, eval_mul_commring, hzero, - Lean.Grind.Semiring.mul_zero] - grind - · rfl + (node.mod parent hcap).eval a = parent.eval a := by + rw [node.mod_eq parent hcap] + simp only [eval_sub_ring, mulWith_eq, eval_mul_commring, hzero, + Lean.Grind.Semiring.mul_zero] + grind + +private theorem map_eval_mod (parent : DensePoly R) (node : DivPlan R) + (hcap : quotientLength parent node.divisor ≤ node.capacity) + (points : List R) (hzero : ∀ a, a ∈ points → node.divisor.eval a = 0) : + points.map ((node.mod parent hcap).eval ·) = + points.map (parent.eval ·) := by + apply List.map_congr_left + intro a ha + exact eval_mod parent node hcap a (hzero a ha) /-- Execute the balanced remainder tree, preserving left-to-right point order. -/ private def evalNode {points : List R} {poly : DensePoly R} : - PointNode R plan points poly → DensePoly R → List R - | .leaf a, f => [f.eval a] - | .branch left right leftPlan rightPlan _ _, f => - evalNode left (reduceNode f leftPlan) ++ - evalNode right (reduceNode f rightPlan) + (node : PointNode R plan points poly) → + node.CapacitySafe → (f : DensePoly R) → f.size ≤ points.length → List R + | .leaf a, _, f, _ => [f.eval a] + | @PointNode.branch _ _ _ _ leftPoints rightPoints _ _ + left right leftPlan rightPlan leftZero rightZero, safe, f, hsize => + have leftSafe := safe.1 + have rightSafe := safe.2.1 + have leftSize := safe.2.2.1 + have rightSize := safe.2.2.2.1 + have leftCapacity := safe.2.2.2.2.1 + have rightCapacity := safe.2.2.2.2.2 + have hleftCap : quotientLength f leftPlan.divisor ≤ leftPlan.capacity := by + rw [leftCapacity] + exact quotientLength_le_capacity f leftPlan leftSize (by + simp [List.length_append] at hsize ⊢ + omega) + have hrightCap : quotientLength f rightPlan.divisor ≤ rightPlan.capacity := by + rw [rightCapacity] + exact quotientLength_le_capacity f rightPlan rightSize (by + simp [List.length_append] at hsize ⊢ + omega) + let leftRemainder := leftPlan.mod f hleftCap + let rightRemainder := rightPlan.mod f hrightCap + have hleftSize : leftRemainder.size ≤ leftPoints.length := by + have h := leftPlan.size_mod_le f hleftCap + rw [leftSize] at h + simp [leftRemainder] at h ⊢ + omega + have hrightSize : rightRemainder.size ≤ rightPoints.length := by + have h := rightPlan.size_mod_le f hrightCap + rw [rightSize] at h + simp [rightRemainder] at h ⊢ + omega + evalNode left leftSafe leftRemainder hleftSize ++ + evalNode right rightSafe rightRemainder hrightSize private theorem evalNode_eq {points : List R} {poly : DensePoly R} - (node : PointNode R plan points poly) - (f : DensePoly R) : evalNode node f = points.map (f.eval ·) := by + {node : PointNode R plan points poly} (safe : node.CapacitySafe) + (f : DensePoly R) (hsize : f.size ≤ points.length) : + evalNode node safe f hsize = points.map (f.eval ·) := by induction node generalizing f with | leaf a => rfl | @branch leftPoints rightPoints leftPoly rightPoly left right leftPlan rightPlan leftZero rightZero leftIH rightIH => simp only [evalNode, List.map_append] rw [leftIH, rightIH] - have hleft : leftPoints.map ((reduceNode f leftPlan).eval ·) = - leftPoints.map (f.eval ·) := by - apply List.map_congr_left - intro a ha - exact eval_reduceNode f leftPlan a (leftZero a ha) - have hright : rightPoints.map ((reduceNode f rightPlan).eval ·) = - rightPoints.map (f.eval ·) := by - apply List.map_congr_left - intro a ha - exact eval_reduceNode f rightPlan a (rightZero a ha) - rw [hleft, hright] + rw [map_eval_mod (hzero := leftZero), map_eval_mod (hzero := rightZero)] /-- Executable cached remainder-tree evaluation. Oversized inputs and the degenerate ring use direct Horner evaluation, exactly as specified. -/ def evalImpl (plan : EvalPlan R) (f : DensePoly R) : Array R := - if f.size ≤ plan.size then + if hsize : f.size ≤ plan.size then match plan.nodeData with | none => plan.points.map (f.eval ·) - | some built => (evalNode built.2 f).toArray + | some built => + (evalNode built.2.1 built.2.2 f (by + simpa [size, points] using hsize)).toArray else plan.points.map (f.eval ·) @@ -331,7 +406,7 @@ theorem eval_eq_impl (plan : EvalPlan R) (f : DensePoly R) : | none => rfl | some built => simp only - rw [evalNode_eq built.2 f] + rw [evalNode_eq built.2.2 f] unfold points rw [← Array.toList_map, Array.toArray_toList] · rfl diff --git a/HexPolyFast/RemainderTree.lean b/HexPolyFast/RemainderTree.lean index d6a9e8630..88da35a9d 100644 --- a/HexPolyFast/RemainderTree.lean +++ b/HexPolyFast/RemainderTree.lean @@ -89,29 +89,56 @@ private inductive WellFormed : RemainderNode R → Prop where (left right : RemainderNode R) (hleft : left.WellFormed) (hright : right.WellFormed) (leftDvd : left.root.poly ∣ root.poly) - (rightDvd : right.root.poly ∣ root.poly) : + (rightDvd : right.root.poly ∣ root.poly) + (rootDegree : root.poly.size - 1 = + (left.root.poly.size - 1) + (right.root.poly.size - 1)) + (leftCapacity : left.plan.capacity = right.root.poly.size - 1) + (rightCapacity : right.plan.capacity = left.root.poly.size - 1) : WellFormed (.branch root plan hplan left right) end RemainderNode -private structure BuiltRemainderNode (leaves : List (MonicLeaf R)) where - node : RemainderNode R - leaves_eq : node.leaves = leaves - wellFormed : node.WellFormed +private theorem foldlDegree_add (leaves : List (MonicLeaf R)) (a b : Nat) : + leaves.foldl (fun degree leaf => degree + (leaf.poly.size - 1)) (a + b) = + a + leaves.foldl (fun degree leaf => degree + (leaf.poly.size - 1)) b := by + induction leaves generalizing b with + | nil => simp + | cons leaf leaves ih => + simp only [List.foldl_cons, Nat.add_assoc] + exact ih (b + (leaf.poly.size - 1)) /-- Sum of leaf degrees, hence the degree of their monic product. -/ private def leafDegreeSum (leaves : List (MonicLeaf R)) : Nat := leaves.foldl (fun degree leaf => degree + (leaf.poly.size - 1)) 0 +private theorem leafDegreeSum_append (left right : List (MonicLeaf R)) : + leafDegreeSum (left ++ right) = + leafDegreeSum left + leafDegreeSum right := by + simp only [leafDegreeSum, List.foldl_append] + simpa using foldlDegree_add right + (left.foldl (fun degree leaf => degree + (leaf.poly.size - 1)) 0) 0 + +private structure BuiltRemainderNode (capacity : Nat) + (leaves : List (MonicLeaf R)) where + node : RemainderNode R + leaves_eq : node.leaves = leaves + capacity_eq : node.plan.capacity = capacity + degree_eq : node.root.poly.size - 1 = leafDegreeSum leaves + wellFormed : node.WellFormed + private def buildRemainderNode (mul : MulPlan R) (capacity : Nat) (hone : (1 : R) ≠ 0) : (leaves : List (MonicLeaf R)) → leaves ≠ [] → - BuiltRemainderNode leaves + BuiltRemainderNode capacity leaves | [], hne => False.elim (hne rfl) | [entry], _ => let plan := DivPlan.ofMonic mul entry.poly entry.monic entry.ne capacity { node := .leaf entry plan (by simp [plan]) leaves_eq := rfl + capacity_eq := by + change plan.capacity = capacity + simp [plan] + degree_eq := by simp [RemainderNode.root, leafDegreeSum] wellFormed := .leaf entry plan _ } | a :: b :: rest, _ => let leaves := a :: b :: rest @@ -151,16 +178,52 @@ private def buildRemainderNode (mul : MulPlan R) (capacity : Nat) have hrightDvd : right.node.root.poly ∣ root.poly := by refine ⟨left.node.root.poly, ?_⟩ rw [hroot, mul_comm_poly] + have hleftCapacity : + left.node.plan.capacity = right.node.root.poly.size - 1 := by + rw [left.capacity_eq, right.degree_eq] + have hrightCapacity : + right.node.plan.capacity = left.node.root.poly.size - 1 := by + rw [right.capacity_eq, left.degree_eq] let node : RemainderNode R := .branch root plan (by simp [plan, root]) left.node right.node have hsplit : leftLeaves ++ rightLeaves = leaves := List.take_append_drop split leaves + have hdegree : root.poly.size - 1 = leafDegreeSum leaves := by + have hleftPos : 0 < left.node.root.poly.size := by + apply Nat.pos_of_ne_zero + intro hz + exact left.node.root.ne ((size_eq_zero_iff _).mp hz) + have hrightPos : 0 < right.node.root.poly.size := by + apply Nat.pos_of_ne_zero + intro hz + exact right.node.root.ne ((size_eq_zero_iff _).mp hz) + have hproduct := size_mul_of_top_ne left.node.root.poly + right.node.root.poly hleftPos hrightPos (by + rw [leadingCoeff_eq_one_of_monic left.node.root.monic, + leadingCoeff_eq_one_of_monic right.node.root.monic] + have hzero : (Zero.zero : R) = 0 := rfl + rw [hzero, Lean.Grind.Semiring.one_mul] + exact hone) + rw [hroot, hproduct] + rw [← hsplit, leafDegreeSum_append] + rw [← left.degree_eq, ← right.degree_eq] + omega + have hrootDegree : root.poly.size - 1 = + (left.node.root.poly.size - 1) + + (right.node.root.poly.size - 1) := by + rw [hdegree, ← hsplit, leafDegreeSum_append, + ← left.degree_eq, ← right.degree_eq] { node leaves_eq := by dsimp [node, RemainderNode.leaves] rw [left.leaves_eq, right.leaves_eq, hsplit] + capacity_eq := by + change plan.capacity = capacity + simp [plan] + degree_eq := hdegree wellFormed := .branch root plan _ left.node right.node - left.wellFormed right.wellFormed hleftDvd hrightDvd } + left.wellFormed right.wellFormed hleftDvd hrightDvd + hrootDegree hleftCapacity hrightCapacity } termination_by leaves => leaves.length decreasing_by all_goals @@ -180,6 +243,10 @@ structure RemainderTree (R : Type u) [DecidableEq R] private nodeLeaves : ∀ node, nodeData = some node → node.leaves = leavesData.toList private nodeWellFormed : ∀ node, nodeData = some node → node.WellFormed + private nodeCapacity : ∀ node, nodeData = some node → + node.plan.capacity = capacityData + private nodeDegree : ∀ node, nodeData = some node → + node.root.poly.size - 1 = leafDegreeSum leavesData.toList private noNodeLeaves : nodeData = none → leavesData.toList = [] namespace RemainderTree @@ -197,6 +264,8 @@ def build (mul : MulPlan R) (capacity : Nat) (leaves : Array (MonicLeaf R)) nodeData := none nodeLeaves := by intro node h; contradiction nodeWellFormed := by intro node h; contradiction + nodeCapacity := by intro node h; contradiction + nodeDegree := by intro node h; contradiction noNodeLeaves := by intro; exact hempty } else let built := buildRemainderNode mul capacity hone leaves.toList hempty @@ -206,6 +275,8 @@ def build (mul : MulPlan R) (capacity : Nat) (leaves : Array (MonicLeaf R)) nodeData := some built.node nodeLeaves := by intro node h; cases h; exact built.leaves_eq nodeWellFormed := by intro node h; cases h; exact built.wellFormed + nodeCapacity := by intro node h; cases h; exact built.capacity_eq + nodeDegree := by intro node h; cases h; exact built.degree_eq noNodeLeaves := by intro h; contradiction } /-- Leaf divisors in their original order. -/ @@ -222,6 +293,10 @@ def size (tree : RemainderTree R) : Nat := tree.leavesData.size /-- Reciprocal capacity cached at the root. -/ def capacity (tree : RemainderTree R) : Nat := tree.capacityData +/-- Degree of the root product, computed as the sum of the leaf degrees. -/ +def rootDegree (tree : RemainderTree R) : Nat := + leafDegreeSum tree.leavesData.toList + private def reduceNode? (node : RemainderNode R) (p : DensePoly R) : Option (DensePoly R) := if hcap : quotientLength p node.plan.divisor ≤ node.plan.capacity then @@ -278,6 +353,71 @@ private def runNode? : RemainderNode R → let rs ← runNode? right r pure (ls ++ rs) +private theorem quotientLength_le_capacity (p q : DensePoly R) (hq : q ≠ 0) + {degree capacity : Nat} (hdegree : q.size - 1 = degree) + (hsize : p.size ≤ degree + capacity) : + quotientLength p q ≤ capacity := by + have hqsize : q.size ≠ 0 := by + intro hz + exact hq ((size_eq_zero_iff q).mp hz) + by_cases hp : p.size < q.size + · simp [quotientLength_eq, hp] + · rw [quotientLength_eq] + simp [hqsize, hp] + omega + +private theorem runNode?_exists {node : RemainderNode R} + (hwf : node.WellFormed) (p : DensePoly R) + (hcap : quotientLength p node.plan.divisor ≤ node.plan.capacity) : + ∃ results, runNode? node p = some results := by + induction hwf generalizing p with + | leaf entry plan hplan => + let current : RemainderNode R := .leaf entry plan hplan + refine ⟨[current.plan.mod p hcap], ?_⟩ + have hred : reduceNode? current p = some (current.plan.mod p hcap) := by + unfold reduceNode? + rw [_root_.dite_eq_left hcap] + simp [current, runNode?, hred] + | branch root plan hplan left right hleft hright leftDvd rightDvd + rootDegree leftCapacity rightCapacity leftIH rightIH => + let current : RemainderNode R := .branch root plan hplan left right + let r := current.plan.mod p hcap + have hrsize : r.size ≤ root.poly.size - 1 := by + have hsize := current.plan.size_mod_le p hcap + simpa [r, current, hplan, RemainderNode.plan] using hsize + rw [rootDegree] at hrsize + have hleftPos : 0 < left.root.poly.size := by + apply Nat.pos_of_ne_zero + intro hz + exact left.root.ne ((size_eq_zero_iff _).mp hz) + have hrightPos : 0 < right.root.poly.size := by + apply Nat.pos_of_ne_zero + intro hz + exact right.root.ne ((size_eq_zero_iff _).mp hz) + have hleftCap : + quotientLength r left.plan.divisor ≤ left.plan.capacity := by + rw [left.plan_divisor, leftCapacity] + by_cases hr : r.size < left.root.poly.size + · simp [quotientLength_eq, hr] + · rw [quotientLength_eq] + simp [Nat.ne_of_gt hleftPos, hr] + omega + have hrightCap : + quotientLength r right.plan.divisor ≤ right.plan.capacity := by + rw [right.plan_divisor, rightCapacity] + by_cases hr : r.size < right.root.poly.size + · simp [quotientLength_eq, hr] + · rw [quotientLength_eq] + simp [Nat.ne_of_gt hrightPos, hr] + omega + rcases leftIH r hleftCap with ⟨ls, hls⟩ + rcases rightIH r hrightCap with ⟨rs, hrs⟩ + refine ⟨ls ++ rs, ?_⟩ + have hred : reduceNode? current p = some r := by + unfold reduceNode? + rw [_root_.dite_eq_left hcap] + simp [current, runNode?, hred, hls, hrs] + private theorem runNode?_sound {node : RemainderNode R} (hwf : node.WellFormed) (origin parent : DensePoly R) (hparent : node.root.poly ∣ origin - parent) @@ -294,7 +434,8 @@ private theorem runNode?_sound {node : RemainderNode R} subst results have hs := reduceNode?_sound (.leaf entry plan hplan) parent r hred exact .cons ⟨dvd_sub_chain hparent hs.1, hs.2⟩ .nil - | branch root plan hplan left right hleft hright leftDvd rightDvd leftIH rightIH => + | branch root plan hplan left right hleft hright leftDvd rightDvd + rootDegree leftCapacity rightCapacity leftIH rightIH => cases hred : reduceNode? (.branch root plan hplan left right) parent with | none => simp [runNode?, hred] at hrun | some r => @@ -327,6 +468,29 @@ def remainders? (tree : RemainderTree R) (p : DensePoly R) : | none => some #[] | some node => runNode? node p |>.map List.toArray +/-- 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 remainders?_isSome_of_capacity (tree : RemainderTree R) + (p : DensePoly R) (hcap : p.size ≤ tree.rootDegree + tree.capacity) : + (tree.remainders? p).isSome := by + unfold remainders? + cases hnode : tree.nodeData with + | none => simp + | some node => + have hrootCap : + quotientLength p node.plan.divisor ≤ node.plan.capacity := by + rw [tree.nodeCapacity node hnode] + exact quotientLength_le_capacity p node.plan.divisor + (degree := tree.rootDegree) (capacity := tree.capacity) (by + rw [node.plan_divisor] + exact node.root.ne) (by + rw [node.plan_divisor] + simpa [rootDegree] using tree.nodeDegree node hnode) hcap + rcases runNode?_exists (tree.nodeWellFormed node hnode) p hrootCap with + ⟨results, hresults⟩ + simp [hresults] + /-- Every successful traversal returns, in leaf order, the canonical-size remainder of the input modulo each leaf polynomial. -/ theorem remainders?_sound (tree : RemainderTree R) (p : DensePoly R) diff --git a/HexPolyFast/SPEC/hex-poly-fast.md b/HexPolyFast/SPEC/hex-poly-fast.md index d227b563c..9ae637bad 100644 --- a/HexPolyFast/SPEC/hex-poly-fast.md +++ b/HexPolyFast/SPEC/hex-poly-fast.md @@ -405,8 +405,10 @@ uses leaves `x - C point`. leaves. Its root caches the caller-supplied reciprocal capacity; each proper node caches exactly the sibling-subtree degree, the largest quotient length that can reach it after its parent reduction. `remainders?` returns `none` -when the input exceeds the root capacity. On success, `remainders?_sound` -supplies a `RemainderSpec`: the output +exactly when the root quotient length exceeds the caller-supplied capacity; +`remainders?_isSome_of_capacity` proves that a capacity covering the input +size above `rootDegree` makes every proper-node reduction succeed. +On success, `remainders?_sound` supplies a `RemainderSpec`: the output has one entry per leaf in the original order, each leaf divides the difference between the input and its result, and every result has size strictly below its leaf divisor. The empty tree succeeds with an empty result.