Parameterize CMvPolynomial by a [FinEnum σ] type instead of n : ℕ

[BoltonBailey]

Claude draft of PR not vetted yet.

Summary

Switch the computable multivariate polynomial stack from a variable count
n : ℕ to a variable type σ carrying a [FinEnum σ] instance, mirroring
Mathlib's MvPolynomial σ R, while staying computationally equivalent to the
current implementation (instantiating σ := Fin n recovers today's behavior).

FinEnum σ supplies FinEnum.card σ : ℕ and FinEnum.equiv : σ ≃ Fin (card σ),
which lets us keep the existing Vector-backed, ExtTreeMap-keyed representation:
CMvMonomial σ := Vector ℕ (FinEnum.card σ), indexed through FinEnum.equiv.

Design decisions

• Monomial representation: Vector ℕ (FinEnum.card σ) (keeps the current
  Ord/compare/ExtTreeMap layer essentially unchanged).
• Arity machinery → disjoint sum: the numeric-overlay machinery (extend,
  align, liftPoly, polyCoe, the Coe/mixed-arity HAdd/HSub/HMul,
  Lawful.X) has no analog for arbitrary types and is replaced with disjoint-sum
  analogs: … σ R → … τ R → … (σ ⊕ τ) R via rename Sum.inl/rename Sum.inr,
  plus a general embedDomain (f : σ ↪ τ).
• Downstream stays Fin-specialized: finSuccEquiv, isEmptyRingEquiv, and the
  Univariate/Bivariate bridges instantiate σ := Fin n.

Status

🚧 Draft / work in progress. The core data layer (CMvMonomial) is generalized
and building. Remaining layers (Unlawful, Lawful, CMvPolynomial, MvPolyEquiv/*,
Operations/Rename, and the Fin-specialized downstream) are still in flux and the
full project does not yet build.

Known follow-up

The main proof-engineering cost is that FinEnum.card (Fin n) is only
propositionally equal to n (FinEnum.card_fin), not definitionally, so the
Fin-specialized proofs need card_fin/equiv bridging where they previously relied
on defeq.

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Parameterize CMvPolynomial by a [FinEnum σ] type instead of n : ℕ

Core Logic Generalization

• Generalizes the CMvPolynomial stack to use an arbitrary type σ with a [FinEnum σ] instance instead of a fixed natural number n, aligning with Mathlib's MvPolynomial architecture.
• Maintains computational equivalence by backing CMvMonomial σ with Vector ℕ (FinEnum.card σ) and indexing through FinEnum.equiv.

API and Structural Changes

• Replaces legacy numeric arity-extension machinery (extend, align, liftPoly, polyCoe, Lawful.X) with embedDomain and disjoint-sum (σ ⊕ τ) analogs.
• Preserves existing Fin n functionality for univariate and bivariate bridges through explicit specialization.
• Addresses proof engineering costs resulting from the loss of definitional equality between FinEnum.card (Fin n) and n by implementing card_fin and equiv bridging.

Status and Discrepancies

• Build Status: This is a work-in-progress; the Lawful, Unlawful, and Operations layers are in flux and the full project does not currently build.
• Discrepancy: The draft summary claims no sorry or admit placeholders were introduced; however, the PR body's description of the project being "in flux" and failing to build suggests that proofs in several core layers remain incomplete.

---

Statistics

Metric	Count
📝 Files Changed	21
✅ Lines Added	755
❌ Lines Removed	781

---

Lean Declarations

✏️ **Removed:** 14 declaration(s)

• example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) : in tests/CompPolyTests/Multivariate/Restrict.lean
• example (p : CMvPolynomial 1 MinimalCoeff) (q : CMvPolynomial 2 MinimalCoeff) : in tests/CompPolyTests/Multivariate/TypeclassMinimization.lean
• def extend (n' : ℕ) (m : CMvMonomial n) : CMvMonomial (max n n') in CompPoly/Multivariate/CMvMonomial.lean
• example (p : CMvPolynomial 1 MinimalCoeff) (q : CMvPolynomial 2 MinimalCoeff) : in tests/CompPolyTests/Multivariate/TypeclassMinimization.lean
• def X (i : ℕ) : Lawful (i + 1) ℤ in CompPoly/Multivariate/Lawful.lean
• def liftPoly in CompPoly/Multivariate/Lawful.lean
• def align in CompPoly/Multivariate/Lawful.lean
• def polyCoe (p : Lawful n R) : Lawful (n + 1) R in CompPoly/Multivariate/Lawful.lean
• example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) : in tests/CompPolyTests/Multivariate/Restrict.lean
• example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) : in tests/CompPolyTests/Multivariate/Restrict.lean
• def extend (n' : ℕ) (p : Unlawful n R) : Unlawful (n ⊔ n') R in CompPoly/Multivariate/Unlawful.lean
• def extend (n' : ℕ) (p : Lawful n R) : Lawful (max n n') R in CompPoly/Multivariate/Lawful.lean
• example (d : ℕ) : restrictDegree (n in tests/CompPolyTests/Multivariate/Restrict.lean
• example (p : CMvPolynomial 1 MinimalCoeff) (q : CMvPolynomial 2 MinimalCoeff) : in tests/CompPolyTests/Multivariate/TypeclassMinimization.lean

✏️ **Added:** 7 declaration(s)

• example (d : ℕ) : restrictDegree (σ in tests/CompPolyTests/Multivariate/Restrict.lean
• example (d d' : ℕ) (p : CMvPolynomial (Fin 2) ℚ) : in tests/CompPolyTests/Multivariate/Restrict.lean
• theorem ofFinsupp_zero : ofFinsupp (0 : σ →₀ ℕ) = (zero : CMvMonomial σ) in CompPoly/Multivariate/CMvMonomial.lean
• example (d d' : ℕ) (p : CMvPolynomial (Fin 2) ℚ) : in tests/CompPolyTests/Multivariate/Restrict.lean
• example (d d' : ℕ) (p : CMvPolynomial (Fin 2) ℚ) : in tests/CompPolyTests/Multivariate/Restrict.lean
• example (p : CMvPolynomial (Fin 1) MinimalCoeff) : in tests/CompPolyTests/Multivariate/TypeclassMinimization.lean
• def embedDomain {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} in CompPoly/Multivariate/Operations.lean

✏️ **Affected:** 231 declaration(s) (line number changed)

• protected lemma grind_add_skip [Add R] {p₁ p₂ : Unlawful σ R} : in CompPoly/Multivariate/Unlawful.lean moved from L166 to L162
• example : in tests/CompPolyTests/Multivariate/CMvMonomial.lean moved from L31 to L31
• private lemma groupWeightedSpec_hornerGroups {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L245 to L245
• theorem evalHorner_eq_eval {R : Type*} {σ : Type*} [FinEnum σ] [CommSemiring R] in CompPoly/Multivariate/HornerLemmas.lean moved from L474 to L483
• lemma map_mul {m₁ m₂ : Multiplicative (σ →₀ ℕ)} : in CompPoly/Multivariate/CMvMonomial.lean moved from L159 to L159
• lemma C_zero : C (σ in CompPoly/Multivariate/Lawful.lean moved from L109 to L109
• lemma rename_mul (f : σ → τ) in CompPoly/Multivariate/Rename.lean moved from L261 to L264
• abbrev CMvPolynomial (σ : Type*) [FinEnum σ] (R : Type*) [Zero R] : Type _ in CompPoly/Multivariate/CMvPolynomial.lean moved from L44 to L44
• example (p : CMvPolynomial (Fin 2) MinimalCoeff) : CMvPolynomial (Fin 2) MinimalCoeff in tests/CompPolyTests/Multivariate/TypeclassMinimization.lean moved from L82 to L82
• lemma eval_equiv {p : CMvPolynomial σ R} {vals : σ → R} : in CompPoly/Multivariate/MvPolyEquiv/Eval.lean moved from L49 to L50
• def C {σ : Type*} [FinEnum σ] {R : Type*} [BEq R] [LawfulBEq R] [Zero R] (c : R) : in CompPoly/Multivariate/CMvPolynomial.lean moved from L51 to L51
• example : (0 : CMvPolynomial (Fin 3) ℚ).vars = ∅ in tests/CompPolyTests/Multivariate/VarsDegrees.lean moved from L26 to L26
• example {σ : Type*} [FinEnum σ] (m : CMvMonomial σ) : ofFinsupp m.toFinsupp = m in tests/CompPolyTests/Multivariate/CMvMonomial.lean moved from L19 to L19
• private lemma eval₂HornerTermSpec_eq_product {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] in CompPoly/Multivariate/HornerLemmas.lean moved from L381 to L381
• def eval₂HornerTerms {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] in CompPoly/Multivariate/CMvPolynomial.lean moved from L196 to L199
• def fromUnlawful (p : Unlawful σ R) : Lawful σ R in CompPoly/Multivariate/Lawful.lean moved from L88 to L88
• lemma degreeOf_equiv {S : Type*} {p : CMvPolynomial σ R} [CommSemiring S] : in CompPoly/Multivariate/MvPolyEquiv/Eval.lean moved from L60 to L61
• theorem npowBySq_eq_npow (p : Lawful σ R) : ∀ k : ℕ, npowBySq p k = npow k p in CompPoly/Multivariate/Operations.lean moved from L487 to L514
• def CMvMonomial (σ : Type*) [FinEnum σ] : Type in CompPoly/Multivariate/CMvMonomial.lean moved from L31 to L38
• def sortHornerGroups {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/CMvPolynomial.lean moved from L172 to L175
• lemma eval_zero : (0 : CMvPolynomial σ R).eval vals = 0 in CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean moved from L31 to L31
• private def groupWeightedSpec {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] in CompPoly/Multivariate/HornerLemmas.lean moved from L37 to L37
• lemma fromUnlawful_cast {p : Lawful σ R} : fromUnlawful p.1 = p in CompPoly/Multivariate/Lawful.lean moved from L210 to L206
• lemma rename_rename {υ : Type*} [FinEnum υ] (f : σ → τ) in CompPoly/Multivariate/Rename.lean moved from L281 to L284
• private lemma insertHornerGroupDesc_pairwise {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L88 to L88
• private lemma eval₂HornerTermSpec_eq_evalMonomial {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L407 to L407
• noncomputable def CRingHom : R →+* CMvPolynomial σ R where in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L408 to L393
• lemma restrictTotalDegree_restrictDegree_comm (d d' : ℕ) (p : CMvPolynomial σ R) : in CompPoly/Multivariate/Restrict.lean moved from L240 to L241
• def zero : CMvMonomial σ in CompPoly/Multivariate/CMvMonomial.lean moved from L95 to L92
• lemma degreeOf_le_of_mem_monomials_restrictDegree {d : ℕ} {m : CMvMonomial σ} in CompPoly/Multivariate/Restrict.lean moved from L109 to L109
• private lemma hornerGroups_descending {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L139 to L139
• def hornerGroups {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/CMvPolynomial.lean moved from L177 to L180
• abbrev isNoZeroCoef [Zero R] (p : Unlawful σ R) : Prop in CompPoly/Multivariate/Unlawful.lean moved from L90 to L86
• private lemma totalDegree_eq_finsupp_sum (m : CMvMonomial σ) : in CompPoly/Multivariate/Restrict.lean moved from L161 to L161
• private def eval₂HornerTermSpec {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] in CompPoly/Multivariate/HornerLemmas.lean moved from L25 to L25
• def eval₂Horner {R S : Type*} {σ : Type*} [FinEnum σ] [Semiring R] [CommSemiring S] : in CompPoly/Multivariate/CMvPolynomial.lean moved from L206 to L209
• private lemma groupWeightedSpec_sortHornerGroups {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L227 to L227
• def addMonoR [Add R] (p : Unlawful σ R) (term : MonoR σ R) : Unlawful σ R in CompPoly/Multivariate/Unlawful.lean moved from L170 to L166
• noncomputable def isEmptyRingEquiv : CMvPolynomial (Fin 0) R ≃+* R in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L365 to L355
• example : (1 : CMvPolynomial (Fin 3) ℚ).degrees = 0 in tests/CompPolyTests/Multivariate/VarsDegrees.lean moved from L29 to L29
• lemma coeff_restrictTotalDegree_eq_zero_of_lt {d : ℕ} {m : CMvMonomial σ} in CompPoly/Multivariate/Restrict.lean moved from L75 to L75
• def degreeOf {R : Type*} {σ : Type*} [FinEnum σ] [Zero R] (i : σ) : CMvPolynomial σ R → ℕ in CompPoly/Multivariate/CMvPolynomial.lean moved from L233 to L237
• example : (0 : CMvPolynomial (Fin 3) ℚ).degrees = 0 in tests/CompPolyTests/Multivariate/VarsDegrees.lean moved from L23 to L23
• lemma npow_add (p : Lawful σ R) (a b : ℕ) : in CompPoly/Multivariate/Operations.lean moved from L475 to L502
• lemma map_mul (a b : CMvPolynomial σ R) : in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L227 to L217
• @[simp] lemma aeval_mul {σ : Type*} [FinEnum σ] {R S : Type*} in CompPoly/Multivariate/Operations.lean moved from L153 to L153
• lemma X_eq_monomial {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L267 to L287
• lemma rename_add (f : σ → τ) in CompPoly/Multivariate/Rename.lean moved from L249 to L252
• protected lemma grind_fromUnlawful_congr {p₁ p₂ : Unlawful σ R} in CompPoly/Multivariate/Lawful.lean moved from L95 to L95
• example (p : CMvPolynomial (Fin 3) ℚ) (i : Fin 3) : in tests/CompPolyTests/Multivariate/VarsDegrees.lean moved from L32 to L32
• lemma map_one : fromCMvPolynomial (1 : CMvPolynomial σ R) = 1 in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L96 to L97
• example : let v : Vector ℕ 2 in tests/CompPolyTests/Multivariate/CMvMonomial.lean moved from L28 to L28
• def C [BEq R] [LawfulBEq R] [Zero R] (c : R) : Unlawful σ R in CompPoly/Multivariate/Unlawful.lean moved from L112 to L108
• def npowBySq [NatCast R] [Add R] [Mul R] (p : Lawful σ R) : ℕ → Lawful σ R in CompPoly/Multivariate/Lawful.lean moved from L180 to L176
• lemma fromCMvPolynomial_finsupp_sum {σ τ : Type*} [FinEnum σ] [FinEnum τ] in CompPoly/Multivariate/Operations.lean moved from L412 to L436
• private lemma eval₂HornerTerms_fold_eq_eval₂_fold {R S : Type*} {σ : Type*} [FinEnum σ] in CompPoly/Multivariate/HornerLemmas.lean moved from L423 to L428
• lemma coeff_restrictDegree_eq_zero_of_not_le {d : ℕ} {m : CMvMonomial σ} in CompPoly/Multivariate/Restrict.lean moved from L87 to L87
• def equivFinsupp : CMvMonomial σ ≃ (σ →₀ ℕ) where in CompPoly/Multivariate/CMvMonomial.lean moved from L152 to L152
• def eval {R : Type*} {σ : Type*} [FinEnum σ] [CommSemiring R] : (σ → R) → CMvPolynomial σ R → R in CompPoly/Multivariate/CMvPolynomial.lean moved from L214 to L217
• instance instSMulZeroClass : SMulZeroClass R (CMvPolynomial σ R) where in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L371 to L361
• lemma filter_get {R : Type*} [BEq R] [LawfulBEq R] {v : R} {m : CMvMonomial σ} (a : Unlawful σ R) : in CompPoly/Multivariate/Unlawful.lean moved from L227 to L223
• protected lemma grind_add_skip [Add R] {p₁ p₂ : Lawful σ R} : in CompPoly/Multivariate/Lawful.lean moved from L146 to L142
• @[simp] lemma aeval_X {σ : Type*} [FinEnum σ] {R S : Type*} in CompPoly/Multivariate/Operations.lean moved from L323 to L346
• lemma coeff_sumToIter {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L434 to L459
• theorem ext {σ : Type*} [FinEnum σ] [Zero R] (p q : CMvPolynomial σ R) in CompPoly/Multivariate/CMvPolynomial.lean moved from L68 to L70
• lemma map_zero : fromCMvPolynomial (0 : CMvPolynomial σ R) = 0 in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L75 to L75
• @[simp] lemma aeval_C {σ : Type*} [FinEnum σ] {R S : Type*} in CompPoly/Multivariate/Operations.lean moved from L135 to L135
• example : CMvPolynomial (Fin 2) MinimalCoeff in tests/CompPolyTests/Multivariate/TypeclassMinimization.lean moved from L68 to L68
• def totalDegree {R : Type*} {σ : Type*} [FinEnum σ] [Zero R] : CMvPolynomial σ R → ℕ in CompPoly/Multivariate/CMvPolynomial.lean moved from L228 to L232
• def Lawful (σ : Type*) [FinEnum σ] (R : Type*) [Zero R] : Type _ in CompPoly/Multivariate/Lawful.lean moved from L30 to L30
• lemma fromUnlawful_fold_eq_fold_fromUnlawful {t : Unlawful σ R} in CompPoly/Multivariate/CMvPolynomial.lean moved from L117 to L120
• def toFinset [DecidableEq R] (p : Unlawful σ R) : Finset (CMvMonomial σ × R) in CompPoly/Multivariate/Unlawful.lean moved from L92 to L88
• lemma fromCMvPolynomial_X {υ : Type*} [FinEnum υ] (i : υ) : in CompPoly/Multivariate/Rename.lean moved from L230 to L233
• def sumToIter {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [Add R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L261 to L281
• lemma eval_C (c : R) : (CMvPolynomial.C c : CMvPolynomial σ R).eval vals = c in CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean moved from L39 to L39
• def leadingMonomial? : Unlawful σ R → Option (CMvMonomial σ) in CompPoly/Multivariate/Unlawful.lean moved from L215 to L211
• lemma coeff_eq {m} (a : CMvPolynomial σ R) : in CompPoly/Multivariate/MvPolyEquiv/Core.lean moved from L116 to L118
• instance instSMul : SMul R (CMvPolynomial σ R) where in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L368 to L358
• example : CMvPolynomial (Fin 2) MinimalCoeff in tests/CompPolyTests/Multivariate/TypeclassMinimization.lean moved from L77 to L77
• example {σ : Type*} [FinEnum σ] (m : σ →₀ ℕ) : (ofFinsupp m).toFinsupp = m in tests/CompPolyTests/Multivariate/CMvMonomial.lean moved from L22 to L22
• lemma totalDegree_equiv {S : Type*} {p : CMvPolynomial σ R} [CommSemiring S] : in CompPoly/Multivariate/MvPolyEquiv/Eval.lean moved from L56 to L57
• def ofList (l : List (CMvMonomial σ × R)) : Unlawful σ R in CompPoly/Multivariate/Unlawful.lean moved from L83 to L83
• def leadingTerm? : Unlawful σ R → Option (MonoR σ R) in CompPoly/Multivariate/Unlawful.lean moved from L211 to L207
• lemma eval_pow (p : CMvPolynomial σ R) (k : ℕ) : in CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean moved from L51 to L51
• example (d : ℕ) : in tests/CompPolyTests/Multivariate/Restrict.lean moved from L20 to L20
• lemma rename_C (f : σ → τ) (c : R) : in CompPoly/Multivariate/Rename.lean moved from L196 to L198
• abbrev MonoR (σ : Type*) [FinEnum σ] (R : Type*) in CompPoly/Multivariate/CMvMonomial.lean moved from L167 to L174
• lemma eval_mul (p q : CMvPolynomial σ R) : in CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean moved from L47 to L47
• lemma fromUnlawful_zero {σ : Type*} [FinEnum σ] [Zero R] : in CompPoly/Multivariate/CMvPolynomial.lean moved from L84 to L86
• def leadingTerm {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder σ] in CompPoly/Multivariate/Operations.lean moved from L75 to L75
• def C (c : R) : MonoR σ R in CompPoly/Multivariate/CMvMonomial.lean moved from L183 to L190
• def support {R : Type*} {σ : Type*} [FinEnum σ] [Zero R] (p : CMvPolynomial σ R) : in CompPoly/Multivariate/CMvPolynomial.lean moved from L224 to L227
• private lemma groupWeightedSpec_sortGroups {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L164 to L164
• lemma coeff_restrictDegree_eq_self_of_le {d : ℕ} {m : CMvMonomial σ} in CompPoly/Multivariate/Restrict.lean moved from L81 to L81
• lemma injective_toFinsupp : Function.Injective (toFinsupp (σ in CompPoly/Multivariate/CMvMonomial.lean moved from L149 to L149
• def add [Add R] (p₁ p₂ : Unlawful σ R) : Unlawful σ R in CompPoly/Multivariate/Unlawful.lean moved from L160 to L156
• @[simp] lemma aeval_pow {σ : Type*} [FinEnum σ] {R S : Type*} in CompPoly/Multivariate/Operations.lean moved from L180 to L180
• lemma eval_add (p q : CMvPolynomial σ R) : in CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean moved from L43 to L43
• def aeval {σ : Type*} [FinEnum σ] {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S] in CompPoly/Multivariate/Operations.lean moved from L126 to L126
• lemma mem_monomials_iff {w : CMvMonomial σ} : w ∈ Lawful.monomials p ↔ w ∈ p in CompPoly/Multivariate/Lawful.lean moved from L200 to L196
• def coeff {R : Type*} {σ : Type*} [FinEnum σ] [Zero R] (m : CMvMonomial σ) (p : Unlawful σ R) : R in CompPoly/Multivariate/Unlawful.lean moved from L223 to L219
• def sub [Add R] (p₁ p₂ : Unlawful σ R) : Unlawful σ R in CompPoly/Multivariate/Unlawful.lean moved from L203 to L199
• @[simp] lemma aeval_add {σ : Type*} [FinEnum σ] {R S : Type*} in CompPoly/Multivariate/Operations.lean moved from L144 to L144
• @[simp] lemma bind₁_mul {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} in CompPoly/Multivariate/Operations.lean moved from L240 to L243
• lemma map_neg (a : CMvPolynomial σ R) : in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L319 to L309
• lemma zero_eq_zero : (0 : Lawful σ R) = ⟨0, by grind⟩ in CompPoly/Multivariate/Lawful.lean moved from L114 to L114
• def sub [Add R] [Neg R] (p₁ p₂ : Lawful σ R) : Lawful σ R in CompPoly/Multivariate/Lawful.lean moved from L228 to L224
• noncomputable instance instAlgebra : Algebra R (CMvPolynomial σ R) in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L423 to L408
• lemma eval₂_equiv {S : Type*} {p : CMvPolynomial σ R} [CommSemiring S] {f : (R →+* S)} in CompPoly/Multivariate/MvPolyEquiv/Eval.lean moved from L25 to L25
• private def termsWeightedSpec {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] in CompPoly/Multivariate/HornerLemmas.lean moved from L42 to L42
• @[simp] lemma sumToIter_zero {σ : Type*} [FinEnum σ] {R : Type*} in CompPoly/Multivariate/Operations.lean moved from L439 to L464
• def X {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [One R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/CMvPolynomial.lean moved from L55 to L56
• lemma rename_id (p : CMvPolynomial σ R) : in CompPoly/Multivariate/Rename.lean moved from L273 to L276
• def mul₀ [Mul R] (t : MonoR σ R) (p : Unlawful σ R) : Unlawful σ R in CompPoly/Multivariate/Unlawful.lean moved from L174 to L170
• @[simp] lemma aeval_zero {σ : Type*} [FinEnum σ] {R S : Type*} in CompPoly/Multivariate/Operations.lean moved from L162 to L162
• @[simp] lemma aeval_one {σ : Type*} [FinEnum σ] {R S : Type*} in CompPoly/Multivariate/Operations.lean moved from L171 to L171
• lemma totalDegree_le_of_mem_monomials_restrictTotalDegree {d : ℕ} {m : CMvMonomial σ} in CompPoly/Multivariate/Restrict.lean moved from L93 to L93
• lemma sumToIter_eq {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L423 to L448
• @[simp] lemma bind₁_add {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} in CompPoly/Multivariate/Operations.lean moved from L234 to L236
• lemma mem_monomials {m : CMvMonomial σ} {up : Unlawful σ R} : in CompPoly/Multivariate/Unlawful.lean moved from L100 to L96
• def div (m₁ m₂ : CMvMonomial σ) : CMvMonomial σ in CompPoly/Multivariate/CMvMonomial.lean moved from L121 to L118
• lemma isNoZeroCoef_zero : isNoZeroCoef (σ in CompPoly/Multivariate/Unlawful.lean moved from L153 to L149
• lemma zero_eq_empty : (0 : Lawful σ R) = ∅ in CompPoly/Multivariate/Lawful.lean moved from L116 to L116
• def evalMonomial {R : Type*} {σ : Type*} [FinEnum σ] [CommSemiring R] : in CompPoly/Multivariate/CMvMonomial.lean moved from L198 to L205
• lemma bind₁_eq_aeval {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} in CompPoly/Multivariate/Operations.lean moved from L218 to L218
• def NzConst {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] (p : Lawful σ R) : Prop in CompPoly/Multivariate/Lawful.lean moved from L195 to L191
• lemma injective_ofFinsupp : Function.Injective (ofFinsupp (σ in CompPoly/Multivariate/CMvMonomial.lean moved from L146 to L146
• theorem toCMvPolynomial_fromCMvPolynomial {p : CMvPolynomial σ R} : in CompPoly/Multivariate/MvPolyEquiv/Core.lean moved from L68 to L69
• lemma fromCMvPolynomial_monomial {σ : Type*} [FinEnum σ] {R : Type*} in CompPoly/Multivariate/Operations.lean moved from L289 to L310
• lemma X_eq_monomial {υ : Type*} [FinEnum υ] (i : υ) : in CompPoly/Multivariate/Rename.lean moved from L206 to L208
• lemma toFinsupp_apply (mono : CMvMonomial σ) (i : σ) : in CompPoly/Multivariate/Rename.lean moved from L57 to L58
• lemma toFinsupp_unitMono {υ : Type*} [FinEnum υ] (i : υ) : in CompPoly/Multivariate/Rename.lean moved from L219 to L221
• def ofFinsupp (m : σ →₀ ℕ) : CPoly.CMvMonomial σ in CompPoly/Multivariate/CMvMonomial.lean moved from L133 to L130
• def npow [NatCast R] [Add R] [Mul R] : ℕ → Lawful σ R → Lawful σ R in CompPoly/Multivariate/Lawful.lean moved from L167 to L163
• abbrev HornerGroup (σ : Type*) [FinEnum σ] (S : Type*) in CompPoly/Multivariate/CMvPolynomial.lean moved from L138 to L141
• lemma eval_one : (1 : CMvPolynomial σ R).eval vals = 1 in CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean moved from L35 to L35
• instance instOfNat_zero : OfNat (Lawful σ R) 0 in CompPoly/Multivariate/Lawful.lean moved from L102 to L102
• lemma restrictTotalDegree_restrictTotalDegree (d d' : ℕ) (p : CMvPolynomial σ R) : in CompPoly/Multivariate/Restrict.lean moved from L207 to L208
• theorem finSuccEquiv_add (p q : CMvPolynomial (Fin (n + 1)) R) : in CompPoly/Multivariate/FinSuccEquiv.lean moved from L83 to L83
• lemma renameMonomial_eq (f : σ → τ) (mono : CMvMonomial σ) : in CompPoly/Multivariate/Rename.lean moved from L62 to L63
• theorem finSuccEquiv_mul (p q : CMvPolynomial (Fin (n + 1)) R) : in CompPoly/Multivariate/FinSuccEquiv.lean moved from L89 to L89
• def mul [Mul R] [Add R] [Zero R] [BEq R] [LawfulBEq R] (p₁ p₂ : Unlawful σ R) : Unlawful σ R in CompPoly/Multivariate/Unlawful.lean moved from L185 to L181
• instance instOfNat {m : ℕ} [NeZero m] [NatCast R] : OfNat (Lawful σ R) m in CompPoly/Multivariate/Lawful.lean moved from L106 to L106
• example : CMvPolynomial (Fin 1) MinimalCoeff in tests/CompPolyTests/Multivariate/TypeclassMinimization.lean moved from L74 to L74
• lemma fromCMvPolynomial_rename (f : σ → τ) in CompPoly/Multivariate/Rename.lean moved from L121 to L122
• def insertHornerTerm {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/CMvPolynomial.lean moved from L145 to L148
• def insertHornerGroupDesc {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/CMvPolynomial.lean moved from L156 to L159
• @[simp] lemma bind₁_X {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} in CompPoly/Multivariate/Operations.lean moved from L332 to L355
• lemma C_zero' : C (σ in CompPoly/Multivariate/Unlawful.lean moved from L133 to L129
• lemma coeff_restrictTotalDegree (d : ℕ) (m : CMvMonomial σ) (p : CMvPolynomial σ R) : in CompPoly/Multivariate/Restrict.lean moved from L54 to L54
• instance instDecidableEq [DecidableEq R] : DecidableEq (Lawful σ R) in CompPoly/Multivariate/Lawful.lean moved from L233 to L229
• lemma map_add (a b : CMvPolynomial σ R) : in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L25 to L25
• def toFinsupp (m : CMvMonomial σ) : σ →₀ ℕ in CompPoly/Multivariate/CMvMonomial.lean moved from L129 to L124
• private lemma mem_insertHornerGroupDesc {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L76 to L76
• @[simp] lemma bind₁_C {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} in CompPoly/Multivariate/Operations.lean moved from L228 to L229
• lemma zero_eq_empty [BEq R] [LawfulBEq R] : (0 : Unlawful σ R) = ∅ in CompPoly/Multivariate/Unlawful.lean moved from L138 to L134
• example (p q : CMvPolynomial (Fin 2) MinimalCoeff) : CMvPolynomial (Fin 2) MinimalCoeff in tests/CompPolyTests/Multivariate/TypeclassMinimization.lean moved from L85 to L85
• def eval₂ {R S : Type*} {σ : Type*} [FinEnum σ] [Semiring R] [CommSemiring S] : in CompPoly/Multivariate/CMvPolynomial.lean moved from L130 to L133
• @[simp] lemma aeval_neg {σ : Type*} [FinEnum σ] {R S : Type*} in CompPoly/Multivariate/Operations.lean moved from L189 to L189
• lemma ext_getElem? {σ : Type*} [FinEnum σ] {R} {t₁ t₂ : Unlawful σ R} in CompPoly/Multivariate/Unlawful.lean moved from L75 to L75
• private lemma eval₂HornerTerms_eq_eval₂HornerTermsSpec {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L336 to L336
• abbrev Unlawful (σ : Type*) [FinEnum σ] (R : Type*) : Type _ in CompPoly/Multivariate/Unlawful.lean moved from L34 to L34
• private def eval₂HornerTermsSpec {σ : Type*} [FinEnum σ] {S : Type*} [CommSemiring S] in CompPoly/Multivariate/HornerLemmas.lean moved from L32 to L32
• lemma foldl_add_comm {β : Type*} [AddCommMonoid β] {σ : Type*} [FinEnum σ] in CompPoly/Multivariate/Operations.lean moved from L404 to L428
• example {σ : Type*} [FinEnum σ] (m : CMvMonomial σ) : m + 0 = m in tests/CompPolyTests/Multivariate/CMvMonomial.lean moved from L25 to L25
• private lemma groupWeightedSpec_collectHornerGroups {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L236 to L236
• lemma fromCMvPolynomial_monomial {υ : Type*} [FinEnum υ] (mono : CMvMonomial υ) (c : R) : in CompPoly/Multivariate/Rename.lean moved from L81 to L82
• theorem toFinsupp_ofFinsupp {m : σ →₀ ℕ} : (ofFinsupp m).toFinsupp = m in CompPoly/Multivariate/CMvMonomial.lean moved from L143 to L141
• lemma foldl_add_comm' {β : Type*} [AddCommMonoid β] {υ : Type*} [FinEnum υ] in CompPoly/Multivariate/Rename.lean moved from L48 to L48
• private lemma groupWeightedSpec_insertHornerGroupDesc {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L147 to L147
• abbrev monomials (p : Lawful σ R) : List (CMvMonomial σ) in CompPoly/Multivariate/Lawful.lean moved from L191 to L187
• noncomputable def toCMvPolynomial (p : MvPolynomial σ R) : CMvPolynomial σ R in CompPoly/Multivariate/MvPolyEquiv/Core.lean moved from L36 to L36
• theorem eval₂Horner_eq_eval₂ {R S : Type*} {σ : Type*} [FinEnum σ] [Semiring R] [CommSemiring S] in CompPoly/Multivariate/HornerLemmas.lean moved from L447 to L453
• lemma sumToIter_add {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L443 to L469
• lemma C_eq_monomial {υ : Type*} [FinEnum υ] (c : R) : in CompPoly/Multivariate/Rename.lean moved from L158 to L159
• lemma fromCMvPolynomial_C {υ : Type*} [FinEnum υ] (c : R) : in CompPoly/Multivariate/Rename.lean moved from L186 to L188
• def bind₁ {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L211 to L211
• lemma C_zero : C (σ in CompPoly/Multivariate/Unlawful.lean moved from L128 to L124
• lemma toFinsupp_unitMono {σ : Type*} [FinEnum σ] in CompPoly/Multivariate/Operations.lean moved from L279 to L299
• lemma add_getD? [AddZeroClass R] {m : CMvMonomial σ} {p q : Unlawful σ R} : in CompPoly/Multivariate/Unlawful.lean moved from L231 to L227
• def degreeOf (m : CMvMonomial σ) (i : σ) : ℕ in CompPoly/Multivariate/CMvMonomial.lean moved from L92 to L89
• theorem finSuccEquiv_symm_apply_apply (p : CMvPolynomial (Fin (n + 1)) R) : in CompPoly/Multivariate/FinSuccEquiv.lean moved from L71 to L71
• protected lemma grind_add_skip_aggressive [Add R] {p₁ p₂ : Lawful σ R} : in CompPoly/Multivariate/Lawful.lean moved from L153 to L149
• lemma toFinsupp_zero {υ : Type*} [FinEnum υ] : in CompPoly/Multivariate/Rename.lean moved from L179 to L180
• def fromCMvPolynomial (p : CMvPolynomial σ R) : MvPolynomial σ R in CompPoly/Multivariate/MvPolyEquiv/Core.lean moved from L30 to L30
• lemma eq_iff_fromCMvPolynomial {u v: CMvPolynomial σ R} : in CompPoly/Multivariate/MvPolyEquiv/Core.lean moved from L120 to L122
• @[simp] lemma aeval_sub {σ : Type*} [FinEnum σ] {R S : Type*} in CompPoly/Multivariate/Operations.lean moved from L198 to L198
• lemma map_sub (a b : CMvPolynomial σ R) : in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L332 to L322
• @[simp] lemma sumToIter_idempotent {σ : Type*} [FinEnum σ] {R : Type*} in CompPoly/Multivariate/Operations.lean moved from L448 to L474
• instance instDecidableEq [DecidableEq R] : DecidableEq (Unlawful σ R) in CompPoly/Multivariate/Unlawful.lean moved from L218 to L214
• def add : CMvMonomial σ → CMvMonomial σ → CMvMonomial σ in CompPoly/Multivariate/CMvMonomial.lean moved from L100 to L97
• instance instEmptyCol : EmptyCollection (Lawful σ R) in CompPoly/Multivariate/Lawful.lean moved from L38 to L38
• lemma zero_def : Zero.zero (α in CompPoly/Multivariate/Lawful.lean moved from L104 to L104
• lemma not_mem_zero : x ∉ (0 : Lawful σ R) in CompPoly/Multivariate/Lawful.lean moved from L124 to L124
• lemma C_zero' : C (σ in CompPoly/Multivariate/Lawful.lean moved from L112 to L112
• abbrev HornerTerm (σ : Type*) [FinEnum σ] (S : Type*) in CompPoly/Multivariate/CMvPolynomial.lean moved from L135 to L138
• lemma coeff_restrictDegree (d : ℕ) (m : CMvMonomial σ) (p : CMvPolynomial σ R) : in CompPoly/Multivariate/Restrict.lean moved from L62 to L62
• lemma restrictDegree_restrictDegree (d d' : ℕ) (p : CMvPolynomial σ R) : in CompPoly/Multivariate/Restrict.lean moved from L216 to L217
• theorem fromCMvPolynomial_toCMvPolynomial {p : MvPolynomial σ R} : in CompPoly/Multivariate/MvPolyEquiv/Core.lean moved from L86 to L87
• abbrev monomials (p : Unlawful σ R) : List (CMvMonomial σ) in CompPoly/Multivariate/Unlawful.lean moved from L96 to L92
• def C (c : R) : Lawful σ R in CompPoly/Multivariate/Lawful.lean moved from L99 to L99
• def evalHorner {R : Type*} {σ : Type*} [FinEnum σ] [CommSemiring R] : in CompPoly/Multivariate/CMvPolynomial.lean moved from L218 to L221
• protected theorem ext (h : (i : Nat) → (_ : i < FinEnum.card σ) → m₁[i] = m₂[i]) : m₁ = m₂ in CompPoly/Multivariate/CMvMonomial.lean moved from L75 to L82
• lemma fromCMvPolynomial_X {σ : Type*} [FinEnum σ] {R : Type*} in CompPoly/Multivariate/Operations.lean moved from L316 to L338
• @[simp] lemma aeval_eq_eval₂ {σ : Type*} [FinEnum σ] {R S : Type*} in CompPoly/Multivariate/Operations.lean moved from L130 to L130
• def hornerExponent {σ : Type*} [FinEnum σ] (k : ℕ) (m : CMvMonomial σ) : ℕ in CompPoly/Multivariate/CMvPolynomial.lean moved from L141 to L144
• def add [Add R] (p₁ p₂ : Lawful σ R) : Lawful σ R in CompPoly/Multivariate/Lawful.lean moved from L140 to L136
• def divides (t₁ t₂ : MonoR σ R) : Bool in CompPoly/Multivariate/CMvMonomial.lean moved from L187 to L194
• private lemma sortHornerGroups_descending {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L118 to L118
• lemma eval_sub (p q : CMvPolynomial σ R) : in CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean moved from L68 to L68
• lemma not_mem_zero : x ∉ (0 : Unlawful σ R) in CompPoly/Multivariate/Unlawful.lean moved from L150 to L146
• lemma rename_X (f : σ → τ) (i : σ) : in CompPoly/Multivariate/Rename.lean moved from L239 to L242
• lemma mul₀_zero [Zero R] [BEq R] [LawfulBEq R] [Mul R] {t : MonoR σ R} : mul₀ t 0 = 0 in CompPoly/Multivariate/Unlawful.lean moved from L180 to L176
• def totalDegree (m : CMvMonomial σ) : ℕ in CompPoly/Multivariate/CMvMonomial.lean moved from L89 to L86
• def coeff {R : Type*} {σ : Type*} [FinEnum σ] [Zero R] (m : CMvMonomial σ) (p : CMvPolynomial σ R) : in CompPoly/Multivariate/CMvPolynomial.lean moved from L61 to L62
• def mul [Mul R] [Add R] (p₁ p₂ : Lawful σ R) : Lawful σ R in CompPoly/Multivariate/Lawful.lean moved from L157 to L153
• def leadingCoeff {σ : Type*} [FinEnum σ] {R : Type*} [Zero R] [MonomialOrder σ] in CompPoly/Multivariate/Operations.lean moved from L85 to L85
• lemma coeff_restrictTotalDegree_eq_self_of_le {d : ℕ} {m : CMvMonomial σ} in CompPoly/Multivariate/Restrict.lean moved from L69 to L69
• lemma eval_neg (p : CMvPolynomial σ R) : in CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean moved from L63 to L63
• def neg (p : Unlawful σ R) : Unlawful σ R in CompPoly/Multivariate/Unlawful.lean moved from L197 to L193
• def collectHornerGroups {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/CMvPolynomial.lean moved from L166 to L169
• def rename {σ τ : Type*} [FinEnum σ] [FinEnum τ] {R : Type*} [Zero R] [Add R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L252 to L256
• private lemma groupWeightedSpec_insertHornerTerm {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L183 to L183
• lemma coeff_restrictBy (keep : CMvMonomial σ → Prop) [DecidablePred keep] in CompPoly/Multivariate/Restrict.lean moved from L26 to L26
• lemma fromCMvPolynomial_finsupp_sum {υ : Type*} [FinEnum υ] in CompPoly/Multivariate/Rename.lean moved from L108 to L109
• lemma smul_def (r : R) (p : CMvPolynomial σ R) : r • p = C r * p in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L375 to L365
• private lemma groupWeightedSpec_groupTerms {σ : Type*} [FinEnum σ] {S : Type*} in CompPoly/Multivariate/HornerLemmas.lean moved from L207 to L207
• @[simp] lemma bind₁_id {σ : Type*} [FinEnum σ] {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L338 to L362
• lemma fromCMvPolynomial_injective : in CompPoly/Multivariate/MvPolyEquiv/Core.lean moved from L110 to L111
• def neg [Neg R] (p : Lawful σ R) : Lawful σ R in CompPoly/Multivariate/Lawful.lean moved from L222 to L218
• example (i : Fin 3) : (0 : CMvPolynomial (Fin 3) ℚ).degreeOf i = 0 in tests/CompPolyTests/Multivariate/VarsDegrees.lean moved from L20 to L20

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Style and Naming Violations

• Variable Conventions: The diff contains multiple violations of the project's variable naming rules. Specifically, carrier letters p, q, and t are used for polynomials and terms, but the diff also uses them as binders for monomials (Finsupp) and ring coefficients (R), which should ideally be m and r/c. Conversely, a, b, and t are used for polynomial values (e.g., in map_add, map_mul, foldl_eq_sum, and fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial), whereas the convention mandates p and q for CMvPolynomial types.
• Syntax (Functions): The guidelines specify a preference for fun x ↦ ... over λ x, .... While the diff avoids λ, it frequently uses the fun x => ... syntax (e.g., in CMvMonomial.ofFinsupp, CMvPolynomial.eval, CMvPolynomial.totalDegree, and CMvPolynomial.rename) instead of the preferred ↦ symbol.
• Theorem Naming (Suffixes): The lemma fromUnlawful_fold_eq_fold_fromUnlawful₀ uses a subscript ₀. While not strictly forbidden, standard project and Mathlib practice typically uses numeric suffixes like _0 to avoid character encoding ambiguities in theorem names.

Architectural and Documentation Findings

• Wiki Updates Required: This pull request introduces a major structural change by refactoring the polynomial variable indexing from Fin n to a generic type σ with a FinEnum instance. It also removes the numeric-based extend/polyCoe machinery and the HAdd/HMul mixed-arity instances in favor of explicit embedDomain calls. According to the Pull Request Guidelines, structural changes and updates to recurring contributor guidance must be reflected in docs/wiki/ within the same PR. No such updates were found in this diff.
• Progress Assessment: The refactoring of CMvPolynomial to use FinEnum successfully generalizes the multivariate API, enabling support for symbolic variable names while maintaining computability. This aligns with the roadmap for improving the flexibility of the formalization.

Positive Observations

• Documentation: Every new or significantly modified definition, including the new embedDomain function, includes a high-quality docstring.
• Naming Logic: Theorem names generally follow the _of_ logic for hypotheses and the standard symbol dictionary (e.g., eq_iff_fromCMvPolynomial, totalDegree_le_of_mem_monomials_restrictTotalDegree).
• Style: The code effectively utilizes dot notation (e.g., p.vars, m.totalDegree) and piping (|> / <|) as preferred by the style guide.

---

📄 **Per-File Summaries**

• CompPoly/Bivariate/CMvEquiv.lean: This update refactors the file to explicitly use Fin n as the variable index type for CMvPolynomial, replacing instances where the index type was implicit or relied on Nat. These changes ensure type consistency across lemmas and the bivariateEquiv definition without introducing any sorry or admit placeholders.
• CompPoly/Multivariate/CMvMonomial.lean: This change generalizes the CMvMonomial type and its operations by replacing fixed natural number indexing with a variable type σ carrying a FinEnum instance. The update modifies all core definitions—including degree calculations, arithmetic, and conversions to Finsupp—to utilize the enumeration of σ, and it introduces the ofFinsupp_zero theorem while removing the extend function.
• CompPoly/Multivariate/CMvPolynomial.lean: Generalizes the CMvPolynomial type and its associated definitions (such as C, X, eval, and degreeOf) to support variables indexed by an arbitrary type σ with a FinEnum instance, replacing the previous Fin n indexing. The changes include updates to several theorems and proofs to accommodate the more general variable type, but no sorry or admit placeholders were introduced.
• CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean: Generalizes evaluation lemmas for CMvPolynomial by replacing the fixed index type Fin n with a generic type σ satisfying the FinEnum typeclass. The modifications update existing proofs for polynomial operations like addition, multiplication, and subtraction to support this more abstract variable representation.
• CompPoly/Multivariate/FinSuccEquiv.lean: This file updates the finSuccEquiv ring equivalence and its associated theorems to explicitly use Fin n as the indexing type for CMvPolynomial. These changes modify the type signatures of existing definitions and lemmas to ensure consistency with the finite indexing convention, and no sorry or admit placeholders were introduced.
• CompPoly/Multivariate/HornerLemmas.lean: This file generalizes multivariate Horner evaluation lemmas by transitioning from a fixed variable count (using n : ℕ) to a generic finite enumerable type (using σ : Type* with [FinEnum σ]). It updates all internal specifications, sorting invariants, and evaluation proofs—including eval₂Horner_eq_eval₂ and evalHorner_eq_eval—to use FinEnum mappings and cardinality instead of Fin n indices.
• CompPoly/Multivariate/Lawful.lean: The Lawful multivariate polynomial type is generalized to use an arbitrary variable index type σ with a FinEnum constraint, replacing the previous fixed natural number indexing. This refactor updates all associated definitions and instances while removing previous logic for extending and aligning polynomials of differing variable counts.
• CompPoly/Multivariate/MvPolyEquiv/Core.lean: The changes generalize the equivalence between CMvPolynomial and MvPolynomial by replacing the Fin n index type with a generic type σ satisfying the FinEnum typeclass. This update involves modifying the core conversion definitions, associated theorems, and the polyEquiv equivalence definition to support these broader multivariate representations without introducing any sorry placeholders.
• CompPoly/Multivariate/MvPolyEquiv/Eval.lean: This change generalizes the indexing type for multivariate polynomials from Fin n to an arbitrary finite type σ with the FinEnum typeclass. It updates theorems for evaluation and degree equivalence, along with the definition of the evaluation ring homomorphism, to support this more general indexing set while maintaining proof correctness.
• CompPoly/Multivariate/MvPolyEquiv/Instances.lean: Generalizes multivariate polynomial instances and lemmas by replacing the fixed number of variables n : ℕ with an arbitrary finite type σ : Type* satisfying FinEnum σ. This update modifies several algebraic structure instances and proofs for CMvPolynomial, including the ring equivalence with MvPolynomial, without introducing any sorry placeholders.
• CompPoly/Multivariate/Operations.lean: The changes generalize multivariate polynomial variable indexing from natural numbers (Fin n) to arbitrary types satisfying the FinEnum typeclass. This refactor updates leading-term operations, evaluation maps, and variable renaming, while introducing the embedDomain function for explicit variable embedding.
• CompPoly/Multivariate/Rename.lean: Generalizes the properties and theorems for CMvPolynomial.rename by transitioning from fixed finite indexing sets (Fin n) to arbitrary types constrained by the FinEnum typeclass. This refactoring updates several key lemmas, including renameMonomial_eq and fromCMvPolynomial_rename, to utilize FinEnum.equiv for mapping between indices while maintaining the existing formal proofs.
• CompPoly/Multivariate/Restrict.lean: This PR generalizes polynomial restriction lemmas and definitions by replacing the fixed natural number indexing n with a generic type σ satisfying the FinEnum type class. Corresponding proofs for total degree and coefficient restrictions were updated to utilize FinEnum equivalences, with no sorry placeholders introduced.
• CompPoly/Multivariate/Unlawful.lean: This Lean file generalizes the Unlawful multivariate polynomial representation by replacing the fixed variable count n : ℕ with a generic finite type σ via the FinEnum typeclass. The refactor updates all internal definitions, instances, and lemmas to use the new indexing and removes the variable-padding extend function.
• CompPoly/Multivariate/VarsDegrees.lean: Generalizes several theorems regarding polynomial variables and degrees by replacing the specific index type Fin n with an arbitrary finite type σ that satisfies the FinEnum typeclass. These changes update existing lemmas to be more polymorphic without altering the underlying proof logic or introducing any sorry placeholders.
• CompPoly/Univariate/CMvEquiv.lean: This update modifies the cmvEquiv ring equivalence and its associated transport theorems to explicitly use Fin 1 as the indexing set for multivariate polynomials instead of the natural number 1. The changes refine the type signatures for several definitions and theorems related to polynomial evaluation and degree without introducing any sorry or admit placeholders.
• bench/CompPolyBench/Multivariate/CMvPolynomial.lean: Updates the buildCMvPolynomial definition to utilize Fin multivariateVars for indexing variables, ensuring type compatibility for multivariate polynomials and monomials. No new theorems or sorry placeholders were introduced.
• tests/CompPolyTests/Multivariate/CMvMonomial.lean: This change generalizes the test examples for CMvMonomial from fixed natural number dimensions to arbitrary types with a FinEnum instance. It updates existing examples to reflect this increased generality and adjusts the syntax for degree calculation tests.
• tests/CompPolyTests/Multivariate/Restrict.lean: The changes update existing test cases for multivariate polynomial degree restriction by explicitly using Fin 2 as the variable index type instead of a raw natural number. This modification aligns the examples with API changes to CMvPolynomial without introducing new theorems or using sorry placeholders.
• tests/CompPolyTests/Multivariate/TypeclassMinimization.lean: This change updates CMvPolynomial type signatures in test cases to explicitly use Fin n for variable sets and replaces implicit mixed-arity arithmetic examples with an explicit embedDomain example. It reinforces the design choice that combining polynomials over different variable types requires explicit embeddings rather than relying on mixed-arity instances.
• tests/CompPolyTests/Multivariate/VarsDegrees.lean: The changes update several test examples for multivariate polynomials by explicitly using Fin 3 as the variable index type instead of a natural number literal. These modifications ensure compatibility with the updated polynomial API without introducing new theorems, proofs, or sorry placeholders.

---

Last updated: 2026-06-26 23:41 UTC.