Add balanced polynomial product trees

.github/workflows/ci.yml

@@ -162,8 +162,8 @@ jobs:
       # fresh against the restored libs, which is cheap.
       - name: Define the hex-dev cache + build target sets
         run: |
-          echo "HEX_LIB_TARGETS=HexBasic HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV"
-          echo "HEX_EXE_TARGETS=hextruncatedseries_bench hexarith_bench hexpoly_bench hexpolysmith_bench hexmvpoly_bench hexmvgcd_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexmodular_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexprimality_bench hexintfactor_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexminpoly_bench hexgramschmidt_bench hexhermite_bench hexsmith_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_bench hexinterval_decision_bench hexroots_demo hex_interval_representation_spike hex_interval_center_spike hex_interval_scale_spike hex_interval_scheduler_spike hex_interval_policy_frontier_spike hex_arith_floor hexlll_bench hexlll_gram_bench hexlll_external_reduction hexbz_factor_service" >> "$GITHUB_ENV"
+          echo "HEX_LIB_TARGETS=HexBasic HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexPolyFast HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV"
+          echo "HEX_EXE_TARGETS=hextruncatedseries_bench hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench hexmvpoly_bench hexmvgcd_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexmodular_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexprimality_bench hexintfactor_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexminpoly_bench hexgramschmidt_bench hexhermite_bench hexsmith_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_bench hexinterval_decision_bench hexroots_demo hex_interval_representation_spike hex_interval_center_spike hex_interval_scale_spike hex_interval_scheduler_spike hex_interval_policy_frontier_spike hex_arith_floor hexlll_bench hexlll_gram_bench hexlll_external_reduction hexbz_factor_service" >> "$GITHUB_ENV"
       # Shared build. The libraries, bench exes, conformance #guard drivers, and
       # emit-fixture exes are all elaborated here so the two verification tails
       # below only *run* things, never rebuild them -- which is what lets the
@@ -222,7 +222,7 @@ jobs:
         run: |
           bash scripts/ci/check_bench_verify_budget.sh \
             hextruncatedseries_bench \
-            hexarith_bench hexpoly_bench hexpolysmith_bench \
+            hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench \
             hexmvpoly_bench hexmvgcd_bench \
             hexpolyz_bench \
             hexpolyzgcd_bench hexsparsepoly_bench hexpolyfp_bench \

HexPolyFast.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import HexPolyFast.Plan
+public import HexPolyFast.Karatsuba
+public import HexPolyFast.Cyclic
+public import HexPolyFast.Reverse
+public import HexPolyFast.Reciprocal
+public import HexPolyFast.Division
+public import HexPolyFast.Tree
+
+public section
+
+/-! Fast proof-carrying dense-polynomial algorithms. -/

HexPolyFast/Cyclic.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import HexPolyFast.Plan
+
+public section
+
+/-!
+# Cyclic and negacyclic products
+
+The reference kernels fold an ordinary planned product by congruence classes
+of exponents. They allocate exactly the requested `n` coefficient slots and
+therefore also serve as independent comparators for transform-based plans.
+-/
+
+namespace Hex.DensePoly
+
+universe u
+
+attribute [local instance 1000] Lean.Grind.Semiring.ofNat
+
+variable {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R]
+
+/-- Sum coefficients of `p` whose exponents are congruent to `k` modulo `n`. -/
+def cyclicCoeff (n k : Nat) (p : DensePoly R) : R :=
+  (List.range ((p.size + n - 1) / n)).foldl
+    (fun acc t => acc + p.coeff (k + t * n)) 0
+
+/-- Alternating sum of coefficients in one congruence class, implementing
+reduction by `x^n = -1`. -/
+def negacyclicCoeff (n k : Nat) (p : DensePoly R) : R :=
+  (List.range ((p.size + n - 1) / n)).foldl
+    (fun acc t =>
+      if t % 2 = 0 then acc + p.coeff (k + t * n)
+      else acc - p.coeff (k + t * n)) 0
+
+/-- Cyclic convolution of positive length `n`. -/
+def mulCyclic (plan : MulPlan R) (n : Nat) (_hn : 0 < n)
+    (a b : DensePoly R) : DensePoly R :=
+  let p := mulWith plan a b
+  ofList ((List.range n).map fun k => cyclicCoeff n k p)
+
+/-- Negacyclic convolution of positive length `n`. -/
+def mulNegacyclic (plan : MulPlan R) (n : Nat) (_hn : 0 < n)
+    (a b : DensePoly R) : DensePoly R :=
+  let p := mulWith plan a b
+  ofList ((List.range n).map fun k => negacyclicCoeff n k p)
+
+/-- Checked cyclic convolution; length zero has no quotient-ring meaning. -/
+def mulCyclic? (plan : MulPlan R) (n : Nat) (a b : DensePoly R) :
+    Option (DensePoly R) :=
+  if hn : 0 < n then some (mulCyclic plan n hn a b) else none
+
+/-- Checked negacyclic convolution; length zero has no quotient-ring meaning. -/
+def mulNegacyclic? (plan : MulPlan R) (n : Nat) (a b : DensePoly R) :
+    Option (DensePoly R) :=
+  if hn : 0 < n then some (mulNegacyclic plan n hn a b) else none
+
+/-- Cyclic products contain at most `n` stored coefficients. -/
+theorem size_mulCyclic_le (plan : MulPlan R) (n : Nat) (hn : 0 < n)
+    (a b : DensePoly R) : (mulCyclic plan n hn a b).size ≤ n := by
+  unfold mulCyclic
+  exact Nat.le_trans (size_ofList_le _) (by simp)
+
+/-- Negacyclic products contain at most `n` stored coefficients. -/
+theorem size_mulNegacyclic_le (plan : MulPlan R) (n : Nat) (hn : 0 < n)
+    (a b : DensePoly R) : (mulNegacyclic plan n hn a b).size ≤ n := by
+  unfold mulNegacyclic
+  exact Nat.le_trans (size_ofList_le _) (by simp)
+
+/-- Coefficient description of cyclic folding. -/
+theorem coeff_mulCyclic (plan : MulPlan R) (n : Nat) (hn : 0 < n)
+    (a b : DensePoly R) (i : Nat) :
+    (mulCyclic plan n hn a b).coeff i =
+      if i < n then cyclicCoeff n i (a * b) else 0 := by
+  unfold mulCyclic
+  rw [coeff_ofList]
+  by_cases hi : i < n
+  · rw [_root_.ite_eq_left hi]
+    simp [List.getD, hi, mulWith_eq]
+  · rw [_root_.ite_eq_right hi, List.getD_eq_getElem?_getD]
+    simp [hi]
+    rfl
+
+/-- Coefficient description of negacyclic folding. -/
+theorem coeff_mulNegacyclic (plan : MulPlan R) (n : Nat) (hn : 0 < n)
+    (a b : DensePoly R) (i : Nat) :
+    (mulNegacyclic plan n hn a b).coeff i =
+      if i < n then negacyclicCoeff n i (a * b) else 0 := by
+  unfold mulNegacyclic
+  rw [coeff_ofList]
+  by_cases hi : i < n
+  · rw [_root_.ite_eq_left hi]
+    simp [List.getD, hi, mulWith_eq]
+  · rw [_root_.ite_eq_right hi, List.getD_eq_getElem?_getD]
+    simp [hi]
+    rfl
+
+end Hex.DensePoly