From 534ca4eb149b8f4ca44c3b1156f02028774bf58c Mon Sep 17 00:00:00 2001 From: Elias Judin Date: Fri, 27 Feb 2026 13:53:15 +0200 Subject: [PATCH 1/3] feat(toMathlib): add finSucc degree and coefficient helpers Add first-variable degree and finSucc leading-coefficient helper API in MvPolynomial equivalence utilities. Co-authored-by: Aristotle (Harmonic) --- CompPoly/ToMathlib/MvPolynomial/Equiv.lean | 37 +++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/CompPoly/ToMathlib/MvPolynomial/Equiv.lean b/CompPoly/ToMathlib/MvPolynomial/Equiv.lean index f3f1e99..4beea42 100644 --- a/CompPoly/ToMathlib/MvPolynomial/Equiv.lean +++ b/CompPoly/ToMathlib/MvPolynomial/Equiv.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Chung Thai Nguyen, Quang Dao +Authors: Chung Thai Nguyen, Quang Dao, Elias Judin -/ import Mathlib.Algebra.MvPolynomial.Equiv @@ -224,6 +224,41 @@ theorem degreeOf_coeff_finSuccEquivNth (f : MvPolynomial (Fin (n + 1)) R) (j : F exact Finset.le_sup (f := fun (g : Fin n.succ →₀ ℕ) => g (Fin.succAbove p j)) (support_coeff_finSuccEquivNth.1 hm) +/-- Maximal degree contributed by the first `n` variables of a polynomial on `Fin (n + 1)`. + +This is the support supremum of the sum of coordinates on `Fin.castSucc`. -/ +noncomputable def firstVarsDegree (P : MvPolynomial (Fin (n + 1)) R) : ℕ := + P.support.sup (fun α => ∑ i : Fin n, α (Fin.castSucc i)) + +/-- A support element bounds `firstVarsDegree` from below. -/ +lemma le_firstVarsDegree_of_mem_support {P : MvPolynomial (Fin (n + 1)) R} + {α : Fin (n + 1) →₀ ℕ} (hα : α ∈ P.support) : + (∑ i : Fin n, α (Fin.castSucc i)) ≤ firstVarsDegree (R := R) P := by + classical + simpa using Finset.le_sup (s := P.support) + (f := fun β : Fin (n + 1) →₀ ℕ => ∑ i : Fin n, β (Fin.castSucc i)) hα + +/-- `firstVarsDegree` of a monomial with nonzero coefficient. -/ +lemma firstVarsDegree_monomial (α : Fin (n + 1) →₀ ℕ) (c : R) (hc : c ≠ 0) : + firstVarsDegree (R := R) (MvPolynomial.monomial α c) = + (∑ i : Fin n, α (Fin.castSucc i)) := by + classical + have hsupp : (MvPolynomial.monomial α c).support = {α} := by + rw [MvPolynomial.support_monomial, if_neg hc] + simp [firstVarsDegree, hsupp] + +/-- Coefficient in the last variable after `finSuccEquiv`. -/ +noncomputable def leadingCoeffFinSucc (P : MvPolynomial (Fin (n + 1)) R) + (d : ℕ) : MvPolynomial (Fin n) R := + (MvPolynomial.finSuccEquiv R n P).coeff d + +/-- Coefficients of `leadingCoeffFinSucc` are the corresponding coefficients of `P`. -/ +@[simp] lemma coeff_leadingCoeffFinSucc (P : MvPolynomial (Fin (n + 1)) R) + (d : ℕ) (i : Fin n →₀ ℕ) : + (leadingCoeffFinSucc (R := R) P d).coeff i = P.coeff (i.cons d) := by + simpa [leadingCoeffFinSucc] using + (MvPolynomial.finSuccEquiv_coeff_coeff (f := P) (m := i) (i := d)) + /-- Consider a multivariate polynomial `φ` whose variables are indexed by `Option σ`, and suppose that `σ ≃ Fin n`. Then one may view `φ` as a polynomial over `MvPolynomial (Fin n) R`, by From 341b198dc65ac2b9b36d7175dad0890fef7b2e17 Mon Sep 17 00:00:00 2001 From: Elias Judin Date: Fri, 27 Feb 2026 14:03:41 +0200 Subject: [PATCH 2/3] chore(imports): regenerate CompPoly.lean import order Regenerate the root import list with scripts/update-lib.sh so import checks are deterministic. --- CompPoly.lean | 67 ++++++++++++++++++++++++++------------------------- 1 file changed, 34 insertions(+), 33 deletions(-) diff --git a/CompPoly.lean b/CompPoly.lean index 95805bd..ba204b7 100644 --- a/CompPoly.lean +++ b/CompPoly.lean @@ -1,55 +1,56 @@ +import CompPoly.Bivariate.Basic +import CompPoly.Bivariate.ToPoly import CompPoly.Data.Array.Lemmas import CompPoly.Data.Classes.DCast import CompPoly.Data.Fin.BigOperators import CompPoly.Data.List.Lemmas +import CompPoly.Data.MvPolynomial.Notation import CompPoly.Data.Nat.Bitwise import CompPoly.Data.Polynomial.Frobenius -import CompPoly.Data.MvPolynomial.Notation +import CompPoly.Data.Polynomial.MonomialBasis import CompPoly.Data.RingTheory.AlgebraTower import CompPoly.Data.RingTheory.CanonicalEuclideanDomain import CompPoly.Data.Vector.Basic +import CompPoly.Fields.BLS12_377 +import CompPoly.Fields.BLS12_381 +import CompPoly.Fields.BN254 +import CompPoly.Fields.BabyBear +import CompPoly.Fields.Basic +import CompPoly.Fields.Binary.AdditiveNTT.AdditiveNTT +import CompPoly.Fields.Binary.AdditiveNTT.Impl +import CompPoly.Fields.Binary.AdditiveNTT.NovelPolynomialBasis +import CompPoly.Fields.Binary.BF128Ghash.Basic +import CompPoly.Fields.Binary.BF128Ghash.Impl +import CompPoly.Fields.Binary.BF128Ghash.Prelude +import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowGcdCertificate +import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowModCertificate +import CompPoly.Fields.Binary.Common +import CompPoly.Fields.Binary.Tower.Basic +import CompPoly.Fields.Binary.Tower.Impl +import CompPoly.Fields.Binary.Tower.Prelude +import CompPoly.Fields.Binary.Tower.TensorAlgebra +import CompPoly.Fields.Goldilocks +import CompPoly.Fields.KoalaBear +import CompPoly.Fields.Mersenne +import CompPoly.Fields.PrattCertificate +import CompPoly.Fields.Secp256k1 import CompPoly.Multilinear.Basic import CompPoly.Multilinear.Equiv import CompPoly.Multivariate.CMvMonomial import CompPoly.Multivariate.CMvPolynomial import CompPoly.Multivariate.CMvPolynomialEvalLemmas -import CompPoly.Multivariate.Restrict -import CompPoly.Multivariate.VarsDegrees import CompPoly.Multivariate.Lawful import CompPoly.Multivariate.MvPolyEquiv import CompPoly.Multivariate.Rename +import CompPoly.Multivariate.Restrict import CompPoly.Multivariate.Unlawful +import CompPoly.Multivariate.VarsDegrees import CompPoly.Multivariate.Wheels -import CompPoly.Univariate.Raw +import CompPoly.ToMathlib.Finsupp.Fin +import CompPoly.ToMathlib.MvPolynomial.Equiv import CompPoly.Univariate.Basic +import CompPoly.Univariate.Lagrange import CompPoly.Univariate.Quotient -import CompPoly.Univariate.ToPoly import CompPoly.Univariate.QuotientEquiv -import CompPoly.Univariate.Lagrange -import CompPoly.Bivariate.Basic -import CompPoly.Bivariate.ToPoly -import CompPoly.ToMathlib.Finsupp.Fin -import CompPoly.ToMathlib.MvPolynomial.Equiv -import CompPoly.Fields.Basic -import CompPoly.Fields.BabyBear -import CompPoly.Fields.Binary.AdditiveNTT.NovelPolynomialBasis -import CompPoly.Fields.Binary.AdditiveNTT.AdditiveNTT -import CompPoly.Fields.Binary.AdditiveNTT.Impl -import CompPoly.Fields.Binary.Common -import CompPoly.Fields.Binary.Tower.Prelude -import CompPoly.Fields.Binary.Tower.Basic -import CompPoly.Fields.Binary.Tower.Impl -import CompPoly.Fields.Binary.Tower.TensorAlgebra -import CompPoly.Fields.Binary.BF128Ghash.Prelude -import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowModCertificate -import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowGcdCertificate -import CompPoly.Fields.Binary.BF128Ghash.Basic -import CompPoly.Fields.Binary.BF128Ghash.Impl -import CompPoly.Fields.BLS12_377 -import CompPoly.Fields.BLS12_381 -import CompPoly.Fields.BN254 -import CompPoly.Fields.Goldilocks -import CompPoly.Fields.KoalaBear -import CompPoly.Fields.Mersenne -import CompPoly.Fields.Secp256k1 -import CompPoly.Fields.PrattCertificate +import CompPoly.Univariate.Raw +import CompPoly.Univariate.ToPoly From 1059857a4defdaed8faa8ee6b1cfe1592124a45e Mon Sep 17 00:00:00 2001 From: Elias Judin Date: Fri, 27 Feb 2026 14:03:41 +0200 Subject: [PATCH 3/3] refactor(multivariate): move first-vars degree helpers into core module Move firstVarsDegree and related support/monomial lemmas to CompPoly.Data.MvPolynomial so ToMathlib only carries equivalence bridge helpers. --- .../Data/MvPolynomial/FirstVarsDegree.lean | 50 +++++++++++++++++++ CompPoly/ToMathlib/MvPolynomial/Equiv.lean | 23 +-------- 2 files changed, 51 insertions(+), 22 deletions(-) create mode 100644 CompPoly/Data/MvPolynomial/FirstVarsDegree.lean diff --git a/CompPoly/Data/MvPolynomial/FirstVarsDegree.lean b/CompPoly/Data/MvPolynomial/FirstVarsDegree.lean new file mode 100644 index 0000000..45a17bd --- /dev/null +++ b/CompPoly/Data/MvPolynomial/FirstVarsDegree.lean @@ -0,0 +1,50 @@ +/- +Copyright (c) 2025 CompPoly. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Elias Judin +-/ + +import Mathlib.Algebra.MvPolynomial.Basic +import Mathlib.Data.Finsupp.Fin + +/-! +# First-variable degree helpers for `MvPolynomial (Fin (n + 1)) R` + +This file defines the maximal total degree contributed by the first `n` variables +(i.e., all variables except the last coordinate). +-/ + +namespace MvPolynomial + +open Finsupp + +section FirstVarsDegree + +variable {n : ℕ} {R : Type*} [CommSemiring R] + +/-- Maximal degree contributed by the first `n` variables of a polynomial on `Fin (n + 1)`. + +This is the support supremum of the sum of coordinates on `Fin.castSucc`. -/ +noncomputable def firstVarsDegree (P : MvPolynomial (Fin (n + 1)) R) : ℕ := + P.support.sup (fun α => ∑ i : Fin n, α (Fin.castSucc i)) + +/-- A support element bounds `firstVarsDegree` from below. -/ +lemma le_firstVarsDegree_of_mem_support {P : MvPolynomial (Fin (n + 1)) R} + {α : Fin (n + 1) →₀ ℕ} (hα : α ∈ P.support) : + (∑ i : Fin n, α (Fin.castSucc i)) ≤ firstVarsDegree (R := R) P := by + classical + simpa using Finset.le_sup (s := P.support) + (f := fun β : Fin (n + 1) →₀ ℕ => ∑ i : Fin n, β (Fin.castSucc i)) hα + +/-- `firstVarsDegree` of a monomial with nonzero coefficient. -/ +lemma firstVarsDegree_monomial (α : Fin (n + 1) →₀ ℕ) (c : R) (hc : c ≠ 0) : + firstVarsDegree (R := R) (MvPolynomial.monomial α c) = + (∑ i : Fin n, α (Fin.castSucc i)) := by + classical + have hsupp : (MvPolynomial.monomial α c).support = {α} := by + rw [MvPolynomial.support_monomial, if_neg hc] + simp [firstVarsDegree, hsupp] + +end FirstVarsDegree + +end MvPolynomial diff --git a/CompPoly/ToMathlib/MvPolynomial/Equiv.lean b/CompPoly/ToMathlib/MvPolynomial/Equiv.lean index 4beea42..3a33c69 100644 --- a/CompPoly/ToMathlib/MvPolynomial/Equiv.lean +++ b/CompPoly/ToMathlib/MvPolynomial/Equiv.lean @@ -5,6 +5,7 @@ Authors: Chung Thai Nguyen, Quang Dao, Elias Judin -/ import Mathlib.Algebra.MvPolynomial.Equiv +import CompPoly.Data.MvPolynomial.FirstVarsDegree import CompPoly.ToMathlib.Finsupp.Fin /-! @@ -224,28 +225,6 @@ theorem degreeOf_coeff_finSuccEquivNth (f : MvPolynomial (Fin (n + 1)) R) (j : F exact Finset.le_sup (f := fun (g : Fin n.succ →₀ ℕ) => g (Fin.succAbove p j)) (support_coeff_finSuccEquivNth.1 hm) -/-- Maximal degree contributed by the first `n` variables of a polynomial on `Fin (n + 1)`. - -This is the support supremum of the sum of coordinates on `Fin.castSucc`. -/ -noncomputable def firstVarsDegree (P : MvPolynomial (Fin (n + 1)) R) : ℕ := - P.support.sup (fun α => ∑ i : Fin n, α (Fin.castSucc i)) - -/-- A support element bounds `firstVarsDegree` from below. -/ -lemma le_firstVarsDegree_of_mem_support {P : MvPolynomial (Fin (n + 1)) R} - {α : Fin (n + 1) →₀ ℕ} (hα : α ∈ P.support) : - (∑ i : Fin n, α (Fin.castSucc i)) ≤ firstVarsDegree (R := R) P := by - classical - simpa using Finset.le_sup (s := P.support) - (f := fun β : Fin (n + 1) →₀ ℕ => ∑ i : Fin n, β (Fin.castSucc i)) hα - -/-- `firstVarsDegree` of a monomial with nonzero coefficient. -/ -lemma firstVarsDegree_monomial (α : Fin (n + 1) →₀ ℕ) (c : R) (hc : c ≠ 0) : - firstVarsDegree (R := R) (MvPolynomial.monomial α c) = - (∑ i : Fin n, α (Fin.castSucc i)) := by - classical - have hsupp : (MvPolynomial.monomial α c).support = {α} := by - rw [MvPolynomial.support_monomial, if_neg hc] - simp [firstVarsDegree, hsupp] /-- Coefficient in the last variable after `finSuccEquiv`. -/ noncomputable def leadingCoeffFinSucc (P : MvPolynomial (Fin (n + 1)) R)