feat: bump lean version

[dhsorens]

Thanks Claude! Bumps to v4.29.0-rc6

CHANGELOG

• Lean v4.28.0 → v4.29.0-rc6; Mathlib v4.28.0 → v4.29.0-rc6; ExtTreeMapLemmas v4.28.0-patch-1 → v4.29.0-rc6 (lean-toolchain, lakefile.lean, lake-manifest.json).
• 36 Lean files touched: mostly tactic/instance fixes (rw → erw, Quotient.eq → Quotient.sound on quotient descent lemmas, stricter simp → dropped unused args, simp (config := { failIfUnchanged := false }), higher maxHeartbeats / maxSteps where needed).
• set_option backward.isDefEq.respectTransparency false (file-scoped): Fields/Binary/Tower/Concrete/{Field,Algebra,Basis}.lean, Fields/Binary/Tower/Equiv.lean; scoped on theorems in Tower/Abstract/Basis.lean, Tower/Support/Preliminaries.lean, ToMathlib/MvPolynomial/Equiv.lean (support_finSuccEquivNth).
• @[reducible] added on various class-valued defs (e.g. Data/RingTheory/AlgebraTower.lean toAlgebra + AlgebraTowerEquiv algebra defs; abstract/concrete binary tower algebra/module/scalar-tower helpers; Concrete/Core mkAddCommGroup/mkRing/mkDivisionRing/mkField; Concrete/Field liftConcreteBTField).
• noncomputable: CBivariate.ofPoly; CMvPolynomial.degreeOf / degrees / vars; getBTFResult; Fintype instances for ConcreteBTField k and test BTF₃.
• Lawful.lean / Unlawful.lean: set_option allowUnsafeReducibility true + attribute [local reducible] instDecidableEqOfLawfulBEq; mem_iff / zero_eq_empty proof tweaks.
• Mathlib renames in proofs: Nat.cast_le → ENat.coe_le_coe (ENat floor lemma); Array.sum_eq_sum_toList → Array.sum_toList; List.extract_eq_drop_take → List.extract_eq_take_drop.
• ENNReal.mul_inv_rev_ENNReal: statement now only ha : a ≠ 0 (drops hb); proof via ENNReal.mul_inv.
• Binary tower / GHASH / NTT / multilinear / mv poly equiv: assorted erw, convert, conv, and simp list edits; NovelPolynomialBasis: degree_Xⱼ WithBot cast path reworked, redundant CoeffVecSpace AddCommGroup instance removed, toCoeffsVec.map_smul' unfolded; Split.lean unique_linear_decomposition_succ and split_algebraMap_eq_zero_x proofs reworked.
• Multivariate/MvPolyEquiv/Instances.lean: Finsupp.single/single_eq_* steps adjusted for new simp behavior.
• Rename.lean: toFinsupp_zero finishes with Vector.getElem_zero.
• Tests Univariate/Linear.lean: test-local BEq defs @[reducible]; LawfulBEq proofs use erw on beq unfolds.

[github-actions]

🤖 Gemini PR Summary

Updates the project to Lean v4.29.0-rc6 and synchronizes dependencies, including Mathlib and ExtTreeMapLemmas.

Infrastructure

• Bumps Lean toolchain to v4.29.0-rc6 in lean-toolchain.
• Updates lakefile.lean and lake-manifest.json to track compatible versions of Mathlib and ExtTreeMapLemmas.

Elaborator and Configuration

• Sets backward.isDefEq.respectTransparency false in Fields/Binary/Tower/Concrete/{Field,Algebra,Basis}.lean and Fields/Binary/Tower/Equiv.lean.
• Applies the same transparency setting scoped to specific theorems in Tower/Abstract/Basis.lean, Tower/Support/Preliminaries.lean, and ToMathlib/MvPolynomial/Equiv.lean.
• Marks various class-valued definitions and instance constructors as @[reducible], including:
  • Data/RingTheory/AlgebraTower.lean: toAlgebra and AlgebraTowerEquiv.
  • Concrete/Core.lean: mkAddCommGroup, mkRing, mkDivisionRing, and mkField.
  • Concrete/Field.lean: liftConcreteBTField.
• Enables set_option allowUnsafeReducibility true and local reducibility for instDecidableEqOfLawfulBEq in Lawful.lean and Unlawful.lean.
• Increases maxHeartbeats and maxSteps for complex proofs in the binary tower modules.

API Changes and Computability

• Breaking Lemma Change: Simplifies ENNReal.mul_inv_rev_ENNReal by removing the hb : b ≠ 0 hypothesis.
• Marks several definitions and instances as noncomputable:
  • CBivariate.ofPoly, CMvPolynomial.degreeOf, CMvPolynomial.degrees, CMvPolynomial.vars, and getBTFResult.
  • Fintype instances for ConcreteBTField k and test case BTF₃.
• Updates proof scripts for Mathlib renames:
  • Nat.cast_le → ENat.coe_le_coe (ENat floor lemma).
  • Array.sum_eq_sum_toList → Array.sum_toList.
  • List.extract_eq_drop_take → List.extract_eq_take_drop.

Tactic and Proof Stabilization

• Systematically replaces rw with erw and updates simp calls (including failIfUnchanged := false and argument pruning) to accommodate stricter unification in Lean 4.29.
• Refactors polynomial quotient lemmas to use Quotient.sound instead of Quotient.eq.
• NovelPolynomialBasis: Reworks degree_Xⱼ cast paths, removes redundant CoeffVecSpace AddCommGroup instance, and unfolds toCoeffsVec.map_smul'.
• Split.lean: Refactors unique_linear_decomposition_succ and split_algebraMap_eq_zero_x proofs.
• Rename.lean: Updates toFinsupp_zero to use Vector.getElem_zero.
• MvPolyEquiv: Adjusts Finsupp.single and single_eq_* steps in Instances.lean for updated simp behavior.

---

Statistics

Metric	Count
📝 Files Changed	36
✅ Lines Added	210
❌ Lines Removed	193

---

Lean Declarations

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

• def mkRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Ring (ConcreteBTField k) where in CompPoly/Fields/Binary/Tower/Concrete/Core.lean
• def mkFieldInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Field (ConcreteBTField k) where in CompPoly/Fields/Binary/Tower/Concrete/Core.lean
• def liftConcreteBTField (k : ℕ) (prevBTFResult : ConcreteBTFStepResult (k in CompPoly/Fields/Binary/Tower/Concrete/Field.lean
• def ConcreteBTFieldAlgebra {l r : ℕ} (h_le : l ≤ r) : in CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean
• def binaryAlgebraTower {l r : ℕ} (h_le : l ≤ r) : Algebra (BTField l) (BTField r) in CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean
• def degrees {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Multiset (Fin n) in CompPoly/Multivariate/CMvPolynomial.lean
• def getBTFResult (k : ℕ) : ConcreteBTFStepResult k in CompPoly/Fields/Binary/Tower/Concrete/Field.lean
• def binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : in CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean
• def AlgebraTowerEquiv.toAlgebraOverRight (e : AlgebraTowerEquiv A B) (i j : ι) in CompPoly/Data/RingTheory/AlgebraTower.lean
• def vars {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n) in CompPoly/Multivariate/CMvPolynomial.lean
• def AlgebraTowerEquiv.toAlgebraOverLeft (e : AlgebraTowerEquiv A B) (i j : ι) in CompPoly/Data/RingTheory/AlgebraTower.lean
• def isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) in CompPoly/Fields/Binary/Tower/Concrete/Basis.lean
• def BTField.isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) in CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
• def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean
• instance instFintype {k : ℕ} : Fintype (ConcreteBTField k) in CompPoly/Fields/Binary/Tower/Concrete/Field.lean
• def mkDivisionRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : in CompPoly/Fields/Binary/Tower/Concrete/Core.lean
• def mkAddCommGroupInstance {k : ℕ} : AddCommGroup (ConcreteBTField k) in CompPoly/Fields/Binary/Tower/Concrete/Core.lean
• def binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : Module (BTField l) (BTField r) in CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean
• def degreeOf {R : Type} {n : ℕ} [Zero R] (i : Fin n) : CMvPolynomial n R → ℕ in CompPoly/Multivariate/CMvPolynomial.lean

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

• lemma zero_eq_empty : (0 : Lawful n R) = ∅ in CompPoly/Multivariate/Lawful.lean moved from L114 to L116
• theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0) : in CompPoly/Data/Nat/Bitwise.lean moved from L52 to L52
• lemma zero_eq_empty [BEq R] [LawfulBEq R] : (0 : Unlawful n R) = ∅ in CompPoly/Multivariate/Unlawful.lean moved from L138 to L140

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The review of the provided diff has identified more than 20 violations of the style guide. The violations are grouped by rule below:

• Rule: Operators: Put spaces on both sides of :, :=, and infix operators.

  • Violation Count: 31
  • Representative Examples:
    • CompPoly/Fields/Binary/Tower/Abstract/Basis.lean:40: (k:=l) should be (k := l)
    • CompPoly/Fields/Binary/Tower/Abstract/Split.lean:329: (l:=k-1) and (castMode:=.all) are missing spaces around := and -.
    • CompPoly/Fields/Binary/Tower/Concrete/Core.lean:1232: (k:=k) should be (k := k)

• Rule: Functions: Prefer fun x ↦ ... over λ x, .... (Note: Use of => instead of ↦ in anonymous functions).

  • Violation Count: 10
  • Representative Examples:
    • CompPoly/Multivariate/CMvPolynomial.lean:144: (fun s => Finsupp.sum s (fun _ e => e)) uses => instead of the preferred ↦.
    • CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean:1345: set f := fun x : ℕ => ...
    • tests/CompPolyTests/Univariate/Linear.lean:17: ⟨fun a b => decide (a = b)⟩

• Rule: Delimiters: Avoid using ; to separate tactics unless writing short, single-line tactic sequences.

  • Violation Count: 11
  • Representative Examples:
    • CompPoly/Fields/Binary/Tower/Abstract/Split.lean:213: erw [Algebra.smul_def, h_alg]; rfl used inside a multi-line proof block.
    • CompPoly/Fields/Binary/Tower/Abstract/Split.lean:218: ...algebraMap_adjacent_tower_succ_eq_Adjoin_of k]; exact hp uses ; to chain a tactic at the end of a long line.
    • CompPoly/Multivariate/Lawful.lean:117: unfold_projs; simp [C, Unlawful.zero_eq_empty]; rfl

• Rule: Dot Notation: Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp).

  • Violation Count: 8
  • Representative Examples:
    • CompPoly/Bivariate/ToPoly.lean:180: (toImpl_add ...).symm should be Eq.symm (toImpl_add ...)
    • CompPoly/Fields/Binary/Tower/Abstract/Basis.lean:41: hg.symm should be Eq.symm hg
    • CompPoly/Multivariate/Restrict.lean:155: (Array.sum_toList ...).symm should be Eq.symm (Array.sum_toList ...)

• Rule: Line Length: Keep lines under 100 characters.

  • Violation Count: 2
  • Representative Examples:
    • CompPoly/Fields/Binary/Tower/Abstract/Split.lean:218: Line reaches 106 characters.
    • CompPoly/Fields/Binary/Tower/Abstract/Split.lean:221: Line reaches 115 characters.

---

📄 **Per-File Summaries**

• CompPoly/Bivariate/ToPoly.lean: This change marks the ofPoly definition as noncomputable and refines several existing proofs to improve tactic robustness, specifically by substituting rw with erw and adjusting congruence applications. No new theorems are introduced, and no sorry or admit placeholders were added.
• CompPoly/Data/Nat/Bitwise.lean: This update simplifies the proof of ENNReal.mul_inv_rev_ENNReal by utilizing existing ENNReal lemmas, which allows for the removal of an unnecessary non-zero hypothesis. Additionally, it updates a lemma reference in ENat.le_floor_NNReal_iff to maintain consistency with the current library. No sorry or admit placeholders were introduced.
• CompPoly/Data/Polynomial/Frobenius.lean: This change modifies the proof of degree_dvd_of_irreducible_dvd_X_pow_card_pow_sub_X by replacing a standard rewrite with erw to resolve a definitional equality involving the cardinality of units. No new theorems or definitions are introduced, and the file contains no sorry or admit placeholders.
• CompPoly/Data/RingTheory/AlgebraTower.lean: This change marks AlgebraTower.toAlgebra and related definitions in AlgebraTowerEquiv as reducible. This is intended to improve typeclass resolution by allowing the elaborator to more easily unfold these definitions when searching for Algebra instances within a tower.
• CompPoly/Data/Vector/Basic.lean: This change modifies the proof of the theorem tail_cons by updating a lemma name in a simplification tactic to match current library naming conventions. No new theorems or definitions are introduced, and the file contains no sorry placeholders.
• CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean: This change refines the proof of the additiveNTT_correctness theorem by updating the simplification and rewrite strategy for base_coeffsBySuffix. It replaces a standard simp/rw sequence with explicit erw calls to ensure the correctness proof remains robust, without introducing any new definitions or sorry placeholders.
• CompPoly/Fields/Binary/AdditiveNTT/Impl.lean: This change marks the Fintype instance for the binary tower field BTF₃ as noncomputable. It does not introduce new theorems or definitions and contains no sorry placeholders.
• CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean: This change modifies existing proofs by replacing rw with erw in two lemmas to resolve unification issues during rewriting. No new theorems, definitions, or sorry placeholders are introduced.
• CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean: The changes refactor and stabilize several proofs related to polynomial degrees and linear maps between coefficient spaces, specifically improving the handling of natural number casts and submodule scalar multiplication. The modifications streamline existing proofs without introducing new definitions, theorems, or sorry placeholders.
• CompPoly/Fields/Binary/BF128Ghash/Basic.lean: This change refines the proof of the root_satisfies_poly theorem by adjusting the simplification and rewriting tactics used to evaluate the field's minimal polynomial. Specifically, it replaces a portion of the simp call with erw to ensure that polynomial evaluation lemmas for powers and variables are applied correctly.
• CompPoly/Fields/Binary/Common.lean: This change refactors the proof of toPoly_128_extend_256 by replacing a complex simp call with a more explicit and structured argument. It utilizes Nat.testBit_lt_two_pow directly to handle bitwise logic, improving the proof's clarity without introducing new theorems or sorry placeholders.
• CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean: This update refines several proofs in the binary field tower formalization by adjusting simplification tactics and adding congr steps to handle casting more robustly. Additionally, it marks the binaryAlgebraTower and binaryTowerModule definitions as @[reducible] to improve instance resolution. No new theorems or sorry placeholders were introduced.
• CompPoly/Fields/Binary/Tower/Abstract/Basis.lean: This PR refines and fixes proofs related to power bases and multilinear bases in binary tower fields by addressing issues with instance resolution and definitional equality. Key changes include using erw and specific compiler options (backward.isDefEq.respectTransparency) to bridge gaps where simp failed, and increasing resource limits for the complex multilinearBasis_apply theorem. No new theorems were added, and no sorry or admit placeholders were introduced.
• CompPoly/Fields/Binary/Tower/Abstract/Split.lean: This PR refines the proofs for the linear decomposition and splitting of binary tower field elements, primarily by improving the handling of algebraic mappings and dependent type casts (eqRec). The changes replace implicit convert tactics with more explicit derivation steps in unique_linear_decomposition_succ and update the simplification path for embeddings in split_algebraMap_eq_zero_x. No new theorems or sorry placeholders are introduced.
• CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean: This change marks ConcreteBTFieldAlgebra and binaryTowerModule as reducible and adjusts unification transparency settings to improve typeclass resolution and definitional equality checks within the concrete binary tower field hierarchy. No new theorems or sorry placeholders are introduced.
• CompPoly/Fields/Binary/Tower/Concrete/Basis.lean: This change refactors and optimizes proofs related to basis constructions in the concrete binary tower field, notably by marking isScalarTower_succ_right as reducible and adjusting definitional equality transparency settings. The PR streamlines the proofs of PowerBasis.cast_basis_succ_of_eq_rec_apply and multilinearBasis_apply and introduces no new theorems or sorry placeholders.
• CompPoly/Fields/Binary/Tower/Equiv.lean: This Lean file updates the environment configuration by setting the backward.isDefEq.respectTransparency option to false. This change is intended to facilitate definitional equality checks and unification during the proofs of equivalences between abstract and concrete binary tower constructions.
• CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean: This change modifies the proof environment for two theorems, linear_form_of_elements_in_adjoined_commring and its uniqueness counterpart, by disabling transparency checks during definitional equality. This adjustment is likely intended to resolve unification or elaboration issues occurring within the proofs of these theorems. No new theorems or definitions are introduced, and there are no sorry placeholders.
• CompPoly/Multilinear/Basic.lean: This change refines the proofs of mobius_apply_zeta_apply_eq_id and zeta_apply_mobius_apply_eq_id by removing redundant simplification lemmas from their respective simp blocks. No new theorems or definitions are introduced, and no sorry placeholders were added.
• CompPoly/Multilinear/Equiv.lean: This change streamlines the proofs of map_add' and map_smul' within the linearEquivMvPolynomialDeg1 definition by replacing redundant conv blocks and simp sequences with more direct rewrites. The modifications simplify the internal logic for mapping coefficients between multilinear and multivariate polynomials without introducing new definitions or theorems.
• CompPoly/Multivariate/CMvPolynomial.lean: This update marks the degreeOf, degrees, and vars definitions as noncomputable. No new theorems or proofs were added, and the changes do not introduce any sorry or admit placeholders.
• CompPoly/Multivariate/Lawful.lean: This update modifies existing proofs by making instDecidableEqOfLawfulBEq locally reducible and replacing rw with erw in the mem_iff lemma to better handle definitional equality. These changes refine the internal proof tactics without introducing new theorems, definitions, or sorry placeholders.
• CompPoly/Multivariate/MvPolyEquiv/Core.lean: This change refines existing proofs for the equivalence between standard and custom multivariate polynomials by replacing certain rewrites with erw and providing more explicit simplification steps. No new definitions or theorems are introduced, and the file contains no sorry or admit placeholders.
• CompPoly/Multivariate/MvPolyEquiv/Instances.lean: This change modifies the proof of map_mul for multivariate polynomials to ensure compatibility with beta-reduction behavior in newer Lean versions. It refines internal tactics and uses change to robustly manage expression folding and unfolding without introducing new theorems or definitions.
• CompPoly/Multivariate/Rename.lean: This change modifies the proof of the toFinsupp_zero lemma by explicitly providing the final justification using Vector.getElem_zero. No new definitions or sorry placeholders are introduced.
• CompPoly/Multivariate/Restrict.lean: This change modifies the proof of the private lemma vector_ofFn_sum_eq_finSum to update a theorem name from Array.sum_eq_sum_toList to Array.sum_toList. No new definitions or theorems are introduced, and no sorry placeholders were added.
• CompPoly/Multivariate/Unlawful.lean: This change adjusts the transparency of equality instances by making instDecidableEqOfLawfulBEq locally reducible and updates the proof of zero_eq_empty with an explicit rfl. No sorry or admit placeholders are introduced.
• CompPoly/ToMathlib/MvPolynomial/Equiv.lean: This change applies the backward.isDefEq.respectTransparency configuration option to the support_finSuccEquivNth theorem to adjust how definitional equality is handled during proof elaboration. It does not introduce new theorems or sorry placeholders.
• CompPoly/Univariate/Quotient/Core.lean: This refactors several proofs in the polynomial quotient implementation by replacing manual rewrites of quotient equality with the more idiomatic Quotient.sound. These changes simplify the proofs for operational "descending" lemmas (such as addition, multiplication, and power) without introducing new definitions or theorems.
• CompPoly/Univariate/Raw/Proofs.lean: This change modifies the proof of the equiv_mul_one lemma by updating a lemma reference from Array.sum_eq_sum_toList to Array.sum_toList. No new definitions or sorry placeholders are introduced.
• lakefile.lean: Updates the project's dependencies, mathlib and ExtTreeMapLemmas, to version v4.29.0-rc6.
• tests/CompPolyTests/Univariate/Linear.lean: This update marks custom BEq Nat instances as reducible and modifies the associated lawfulness proofs to use erw for more explicit unfolding. The changes refine existing internal proofs without introducing new theorems or sorry placeholders.
• CompPoly/Fields/Binary/Tower/Concrete/Field.lean: This change refines the concrete binary tower field implementation by marking several core definitions and Fintype instances as noncomputable or @[reducible]. It also adjusts the backward.isDefEq.respectTransparency setting to ensure proper definitional equality behavior during field construction; no new theorems or sorry placeholders are introduced.
• CompPoly/Fields/Binary/Tower/Concrete/Core.lean: This PR refactors existing proofs in ConcreteBTField for better maintainability and modifies several instance-generating definitions (such as mkFieldInstance and mkRingInstance) by marking them as @[reducible]. The changes focus on streamlining tactic use—replacing complex simp calls with more direct erw and show statements—without introducing new theorems or sorry placeholders.

---

Last updated: 2026-03-28 19:47 UTC.

[github-actions]

Build Timing Report

• Commit: 449ca93
• Message: Merge 2aeb7af into fe33688
• Ref: dhsorens/bump_to_4.29.0-rc6
• Comparison baseline: fe33688 from merge-base on master.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; test path lake test.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	260.41	244.80	-15.61	ok
Warm rebuild	1.63	1.72	+0.09	ok
Test path	18.55	16.55	-2.00	ok

Incremental Rebuild Signal

• Warm rebuild saved 243.08s vs clean (142.33x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
57.00	86.00	-29.00	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean
56.00	55.00	+1.00	CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
48.00	47.00	+1.00	CompPoly/Bivariate/ToPoly.lean
25.00	29.00	-4.00	CompPoly/Univariate/Raw/Proofs.lean
24.00	34.00	-10.00	CompPoly/Fields/Binary/BF128Ghash/Impl.lean
23.00	24.00	-1.00	CompPoly/Univariate/Lagrange.lean
21.00	21.00	+0.00	CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean
18.00	24.00	-6.00	CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean
16.00	15.00	+1.00	CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean
16.00	16.00	+0.00	CompPoly/Fields/Binary/Tower/Abstract/Core.lean
16.00	15.00	+1.00	CompPoly/Univariate/Quotient/Core.lean
15.00	17.00	-2.00	CompPoly/Fields/Binary/AdditiveNTT/Domain.lean
15.00	19.00	-4.00	CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean
13.00	16.00	-3.00	CompPoly/Univariate/Basic.lean
12.00	20.00	-8.00	CompPoly/Multivariate/Unlawful.lean
11.00	13.00	-2.00	CompPoly/Fields/Binary/Common.lean
10.00	8.90	+1.10	CompPoly/Fields/Binary/Tower/TensorAlgebra.lean
10.00	9.40	+0.60	CompPoly/Multilinear/Basic.lean
9.60	11.00	-1.40	CompPoly/Data/Nat/Bitwise.lean
9.60	10.00	-0.40	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowGcdCertificate.lean

[github-actions]

🤖 Initial AI review without external context

🤖 AI Review

Overall Summary:

1. TL;DR

The mathematical refactoring and logic in this PR are mostly sound and contain several positive maintenance fixes. However, there are significant Lean 4 technical issues that need addressing—most notably, an unintentional loss of computability in the CMvPolynomial library and a concerning, pervasive reliance on a legacy transparency unifier flag (backward.isDefEq.respectTransparency false) to bypass definitional equality issues in the binary fields tower.

2. Checklist Coverage

No explicit specification checklist was provided for this PR.

3. Key Lean 4 / Mathlib Issues

A. Legacy Transparency Override Anti-Pattern (4 files)
The PR introduces the global option set_option backward.isDefEq.respectTransparency false across several files. This is a heavy code smell in Lean 4. It forces the unifier to ignore transparency annotations (like irreducible), which completely breaks abstraction boundaries, results in fragile proofs, and can cause massive performance degradation (as evidenced by the need to bump maxHeartbeats to 800,000 in Abstract/Basis.lean).
While tightly scoped usage (e.g., set_option ... in as seen in Support/Preliminaries.lean or ToMathlib/MvPolynomial/Equiv.lean) is acceptable as a temporary workaround, global file-level overrides must be removed. The underlying dependent-type equality casts likely need to be refactored using Equiv, RingEquiv, or AlgEquiv, or by ensuring binaryTowerAlgebra is definitionally equal to Algebra.id.
Affected Files:

• CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
• CompPoly/Fields/Binary/Tower/Concrete/Basis.lean
• CompPoly/Fields/Binary/Tower/Concrete/Field.lean
• CompPoly/Fields/Binary/Tower/Equiv.lean

B. Computability Regression in Computable Multivariate Polynomials (1 file)
Marking degreeOf, degrees, and vars as noncomputable entirely defeats the purpose of the CMvPolynomial ("Computable Multivariate Polynomial") library. The noncomputability stems from taking a Finset.sup over a Multiset. You can restore full computability by pushing the mapping inside the supremum so it operates over ℕ.
Better yet, you can optimize both degreeOf and totalDegree for a computable library by directly folding over the underlying monomial list:

def degreeOf {R : Type} {n : ℕ} [Zero R] (i : Fin n) : CMvPolynomial n R → ℕ :=
  fun p => (Lawful.monomials p).foldl (fun acc m => max acc (CMvMonomial.toFinsupp m i)) 0

Affected File: CompPoly/Multivariate/CMvPolynomial.lean

C. Duplicate Typeclass Instances (1 file)
There are two identical Fintype (ConcreteBTField k) instances defined right next to each other (one with explicit (k : ℕ), one with implicit {k : ℕ}). To typeclass synthesis, these are identical and will cause redundant searches or ambiguous instance errors. Please delete one.
Affected File: CompPoly/Fields/Binary/Tower/Concrete/Field.lean

4. Nitpicks & Lean 4 Best Practices

• abbrev vs @[reducible] def: In Lean 4, abbrev is the preferred, idiomatic way to define reducible definitions. You frequently use @[reducible] def (seen in AlgebraTower.lean, Abstract/Algebra.lean, Abstract/Basis.lean, and Concrete/Algebra.lean). Replacing these with abbrev is functionally identical but cleaner.
• Tactic Mode for Data: Avoid dropping into tactic mode (:= by exact ...) to construct raw data terms (seen in AlgebraTower.lean and Abstract/Algebra.lean). Provide the definition directly, e.g., := AlgebraTower.toAlgebra h_le.
• Prop-valued defs: isScalarTower_succ_right in Concrete/Basis.lean returns a Prop (IsScalarTower). It is more idiomatic to declare this using theorem, lemma, or directly as an instance/abbrev rather than a def.

5. Overall Verdict

Changes Requested

---

📄 **Review for `CompPoly/Bivariate/ToPoly.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Data/Nat/Bitwise.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Data/Polynomial/Frobenius.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Data/RingTheory/AlgebraTower.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

• In Lean 4, abbrev is generally preferred over @[reducible] def as a more concise idiom for defining reducible definitions.
• The definitions AlgebraTowerEquiv.toAlgebraOverLeft and toAlgebraOverRight use := by exact ... to return data. It is more idiomatic to provide the term directly without dropping into tactic mode, e.g., := (e.algebraMapRightUp i j h).toAlgebra (Note: this was pre-existing in the file, but is worth cleaning up while you are modifying the attributes).

📄 **Review for `CompPoly/Data/Vector/Basic.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

(The only change in this pull request is updating the lemma name List.extract_eq_drop_take to List.extract_eq_take_drop in the simp only list of tail_cons's proof, likely to align with a recent upstream rename in Mathlib/Batteries. This is a straightforward and correct maintenance fix.)

📄 **Review for `CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/AdditiveNTT/Impl.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

• BTF₃ is defined as an abbrev for ConcreteBTField 3. Because it is an abbrev (a reducible type synonym), typeclass inference will transparently see through it and automatically find the instances for ConcreteBTField 3. Thus, explicitly declaring instances like instance : Field BTF₃, instance : DecidableEq BTF₃, and noncomputable instance : Fintype BTF₃ is strictly speaking redundant, though completely harmless and sometimes useful for speeding up instance synthesis. The addition of the noncomputable modifier perfectly resolves the computability check for this instance.

📄 **Review for `CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

Explanation:
The changes in this PR are entirely positive. The removal of the explicit AddCommGroup (CoeffVecSpace L ℓ) instance is a good application of Lean 4 / Mathlib best practices, as CoeffVecSpace L ℓ is an abbrev for Fin (2^ℓ) → L, which naturally inherits the Pi-type AddCommGroup from L. Providing an explicit instance for this can lead to typeclass diamonds or redundant searches, so deleting it is the right call. The remaining changes are isolated entirely to tactic proofs (fixing simp applicability and explicitly manipulating type casts where norm_cast seemingly struggled), all of which look correct and idiomatic.

📄 **Review for `CompPoly/Fields/Binary/BF128Ghash/Basic.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
The repeated sequence in erw [eval₂_pow, eval₂_X, eval₂_pow, eval₂_X, eval₂_pow, eval₂_X] at h is slightly unidiomatic for a proof script. If simp was struggling to apply eval₂_pow due to transparency issues, using simp_rw [eval₂_pow, eval₂_X] at h or wrapping the specific rewrites in a repeat block might be cleaner, though the current form is perfectly fine and mathematically sound.

📄 **Review for `CompPoly/Fields/Binary/Common.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

• In binaryAlgebraTower, defining the body with by exact AlgebraTower.toAlgebra h_le is a bit unidiomatic. You can provide the term directly without entering tactic mode: := AlgebraTower.toAlgebra h_le.
• Using @[reducible] def is functionally equivalent to using abbrev, which is often preferred for readability when creating reducible definitions.

📄 **Review for `CompPoly/Fields/Binary/Tower/Abstract/Basis.lean`**

Verdict: Changes Requested

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

• Anti-pattern: backward.isDefEq.respectTransparency false: The addition of set_option backward.isDefEq.respectTransparency false is a heavy code smell. It forces the unifier to completely ignore transparency settings, which can lead to unpredictable behavior, massive performance degradation, and extremely fragile proofs. This is typically a symptom of a deeper architectural issue, such as non-defeq typeclass instances (e.g., binaryTowerAlgebra vs Algebra.id) or the use of Eq.rec/cast on algebraic structures. In Lean, casting algebraic structures using propositional equality should generally be avoided in favor of Equiv, RingEquiv, or AlgEquiv.
• Performance / Heartbeat Bumps: Increasing maxHeartbeats to 800000 and maxSteps to 100000 indicates that the unifier is pathologically struggling with the equality casts and instance synthesis. While acceptable as a temporary workaround, this should be flagged for a future refactor to clean up the dependent type theory "equality hell."

Nitpicks:

• Idiomatic Reducibility: You changed def BTField.isScalarTower_succ_right to @[reducible] def. Since this definition returns a typeclass (IsScalarTower), making it reducible is the correct instinct so that typeclass inference can see through it. However, the more idiomatic Lean 4 way to write a reducible definition is to use abbrev.
• Proof Workarounds: The comment -- algebraMap from BTField (r1+1) to itself is identity, but the instance is binaryAlgebraTower which simp can't rewrite highlights the exact cause of the defeq struggles. Because binaryTowerAlgebra is not definitionally equal to Algebra.id, simp fails and you are forced to use erw and a manual show ... from by .... If binaryTowerAlgebra for $l = r$ can be refactored to be definitionally equal to Algebra.id, a huge portion of these proof hacks can be removed.

📄 **Review for `CompPoly/Fields/Binary/Tower/Abstract/Split.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

• Consider using abbrev instead of @[reducible] def. In Lean 4, abbrev is the idiomatic shorthand that does exactly the same thing (it marks the definition as reducible) but is slightly more concise. For example: abbrev ConcreteBTFieldAlgebra {l r : ℕ} (h_le : l ≤ r) : Algebra ... := ...

📄 **Review for `CompPoly/Fields/Binary/Tower/Concrete/Basis.lean`**

Verdict: Changes Requested

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

• Global Transparency Override: The addition of set_option backward.isDefEq.respectTransparency false at the top of the file is highly discouraged. This option forces the unifier (isDefEq) to ignore transparency annotations (such as irreducible), which completely breaks abstraction boundaries and can lead to severe performance cliffs or timeouts during elaboration. If this option is genuinely required for specific defeq checks to succeed, it should be tightly scoped to only the affected declarations using set_option ... in.

Nitpicks:

• Brittle simp calls in proofs: In the proof of multilinearBasis_apply, you introduced simp (config := { failIfUnchanged := false }) only [...]. This is an antipattern in proof scripts, as it suppresses failures when the simp lemmas don't apply, making the proof brittle and harder to maintain. If you aren't sure if the simp will do work, consider using try simp only [...] instead, or better yet, refine the proof so the exact required rewrites/simps are applied.
• Prop-valued def: isScalarTower_succ_right is declared as a def but returns a Prop (specifically, the IsScalarTower class). While mathematically fine, it is generally more idiomatic in Lean to use lemma or theorem for Prop-valued declarations, or to mark it directly as an instance or abbrev. (The diff just adds @[reducible], but the underlying keyword remains def).

📄 **Review for `CompPoly/Fields/Binary/Tower/Concrete/Core.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

(The addition of @[reducible] to the typeclass-constructing definitions like mkRingInstance and mkFieldInstance is a very good change. It ensures that when these functions are used via letI to construct local instances, Lean's unification engine can transparently see the underlying data—such as the specific add and mul operations—preventing defeq failures during typeclass synthesis and algebraic proofs.)

📄 **Review for `CompPoly/Fields/Binary/Tower/Concrete/Field.lean`**

Verdict: Needs Minor Revisions

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

• Duplicate Instances: The diff updates two identical Fintype (ConcreteBTField k) instances:

  noncomputable instance (k : ℕ) : Fintype (ConcreteBTField k) := (getBTFResult k).instFintype
  
  noncomputable instance instFintype {k : ℕ} : Fintype (ConcreteBTField k) :=
    (getBTFResult k).instFintype

  To the typeclass synthesis engine, these are exactly the same (whether k is explicit or implicit only affects direct term applications like instFintype (k := 2), not automated resolution). Having duplicate instances is an anti-pattern that can slow down typeclass synthesis or cause ambiguous instance errors. You should remove one of them.

Nitpicks:

• Global Unifier Option: You added set_option backward.isDefEq.respectTransparency false at the top of the file. Changing core unifier settings globally across an entire file is generally discouraged in Lean 4, as it can cause unexpected definitional equality failures or bypass intended abstraction boundaries. If this was added to fix a timeout or performance issue in a specific proof, it is much safer to scope it strictly to that specific declaration using set_option backward.isDefEq.respectTransparency false in.

📄 **Review for `CompPoly/Fields/Binary/Tower/Equiv.lean`**

Verdict: Changes Requested

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

1. Use of Legacy isDefEq Flag: The addition of set_option backward.isDefEq.respectTransparency false is strongly discouraged in Lean 4. This is a backward compatibility flag introduced to ease migration when Lean tightened its definitional equality checks regarding transparency. Relying on it indicates that some proofs in this file depend on fragile definitional unfoldings that the modern, more predictable isDefEq algorithm rightly rejects. While it can be a useful temporary workaround during a Lean version bump, leaving it permanently in the codebase can lead to fragile proofs and performance issues during typechecking. The underlying proofs should ideally be refactored (often by adding explicit dsimp, unfold, or change steps to manage definitional equality) so that this global option can be removed.

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean`**

Verdict: Needs Minor Revisions

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

• Use of backward.isDefEq.respectTransparency false: You've added set_option backward.isDefEq.respectTransparency false in to linear_form_of_elements_in_adjoined_commring and unique_linear_form_of_elements_in_adjoined_commring. While this is a known escape hatch for resolving defeq/unification timeouts in Lean 4 (especially when dealing with the algebraic hierarchy and AdjoinRoot), it is generally considered technical debt because it reverts to legacy unifier behavior. If possible, try to identify the specific terms causing the unification struggle and resolve them via explicit dsimp, unfold, or by providing explicit types in the proofs. As a short-term workaround, this is acceptable, but it should ideally be documented with a -- TODO: comment explaining exactly why the option is needed here so future maintainers know when it can be safely removed.

📄 **Review for `CompPoly/Multilinear/Basic.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multilinear/Equiv.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/CMvPolynomial.lean`**

Verdict: Changes Requested

Critical Misformalizations:
None.

Lean 4 / Mathlib Issues:
The PR marks degreeOf, degrees, and vars as noncomputable. This fundamentally violates the purpose of the CMvPolynomial ("Computable Multivariate Polynomial") library.

The noncomputability is almost certainly triggered by Finset.sup over Multiset (Fin n) inside degreeOf. In Mathlib, finding a computable SemilatticeSup instance for Multiset α can sometimes fail or fall back to classical logic depending on the context and available DecidableEq instances. By contrast, taking a Finset.sup over ℕ is completely computable (as evidenced by totalDegree in the very same file, which successfully compiles without the noncomputable keyword).

To fix this and restore computability, you can push the Multiset.count i operation inside the Finset.sup. This mathematically changes the supremum to operate directly over ℕ instead of Multiset. Once degreeOf is fully computable again, the noncomputable flags on degrees and vars can also be safely removed.

Corrected, computable version for degreeOf:

def degreeOf {R : Type} {n : ℕ} [Zero R] (i : Fin n) : CMvPolynomial n R → ℕ :=
  fun p =>
    Finset.sup (List.toFinset (List.map CMvMonomial.toFinsupp (Lawful.monomials p)))
      fun s => s i

(Note: Changing degreeOf to this definition will not break the existing proof for degreeOf_eq_count_degrees, as that proof relies purely on the structure of degrees and simplifies the RHS directly to p.degreeOf i without unfolding degreeOf's definition).

Nitpicks:
The current implementations of degreeOf and totalDegree convert the list of monomials to a Finset of Finsupp objects just to take a supremum. This is inefficient for a library explicitly geared towards computability. You could significantly optimize both definitions by folding directly over the underlying list of monomials.

For example:

def degreeOf {R : Type} {n : ℕ} [Zero R] (i : Fin n) : CMvPolynomial n R → ℕ :=
  fun p => (Lawful.monomials p).foldl (fun acc m => max acc (CMvMonomial.toFinsupp m i)) 0

(A similar list-folding optimization can be applied to totalDegree).

📄 **Review for `CompPoly/Multivariate/Lawful.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/MvPolyEquiv/Core.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/MvPolyEquiv/Instances.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/Rename.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/Restrict.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/Unlawful.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/ToMathlib/MvPolynomial/Equiv.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
The addition of set_option backward.isDefEq.respectTransparency false in is a well-known and acceptable workaround for typeclass/defeq resolution timeouts or failures involving complex definitions like MvPolynomial and Finsupp. Since it is scoped directly to the theorem support_finSuccEquivNth, it minimizes any side effects on the rest of the file.

📄 **Review for `CompPoly/Univariate/Quotient/Core.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

Reviewer Notes:
This PR is a solid proof refactoring that correctly replaces the unidiomatic rw [Quotient.eq]; simp [...] pattern with apply Quotient.sound. The associated simplifications (like reducing apply mulPowX_equiv; exact heq to exact mulPowX_equiv i p₁ p₂ heq and removing dangling rfls) make the proofs cleaner and more robust. No issues found.

📄 **Review for `CompPoly/Univariate/Raw/Proofs.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `lakefile.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `tests/CompPolyTests/Univariate/Linear.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

• The use of erw [show ... from rfl] to unfold a definition within a proof is a bit unidiomatic. Typically, you would use change ... = ... to change the goal's syntactic form, or dsimp [natBeqEq] (or unfold) to evaluate the reducible definition. However, since this is confined to a test file and achieves the intended result without performance issues, it is perfectly acceptable.