bump 4.32

[alexanderlhicks]

had to bump some heartbeats/recdepth unfortunately.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: bump 4.32

ℹ️ This PR modifies 2 file(s) under CompPoly/ToMathlib/ — consider whether a corresponding upstream PR is needed.

This PR bumps the project to Lean 4.32, adapting to upstream API changes in MvPolynomial and AddMonoidAlgebra, removing the custom MProd type in favor of the standard product type, and raising heartbeat/recursion-depth limits where needed to accommodate more expensive elaboration. No sorries or admits are introduced.

---

Statistics

Metric	Count
📝 Files Changed	20
✅ Lines Added	122
❌ Lines Removed	88

---

Lean Declarations

✏️ Added: 3 declaration(s)

CompPoly/Fields/Binary/BF128Ghash/Impl.lean (3)

• instance instDivisionRingConcreteBF128Ghash : DivisionRing ConcreteBF128Ghash where
• instance instRingConcreteBF128Ghash : Ring ConcreteBF128Ghash where
• instance instSemigroupConcreteBF128Ghash : Semigroup ConcreteBF128Ghash where

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• CompPoly/Bivariate/ToPoly.lean: The proof of ofPoly_zero (which states ofPoly (0 : R[X][Y]) = 0) was simplified by removing two unnecessary lines: erw [Finsupp.support_zero] and exact Finset.sum_empty. The simp +decide tactic now suffices on its own.
• CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean: In NTTStage_correctness, two congr tactics were adjusted: one was replaced with congr 1 (at line 768 of the original file) and another with simp only [h_v_eq] (at line 852). Additionally, set_option maxHeartbeats 10000000 was added at the start of that lemma (now line 663).
• CompPoly/Fields/Binary/BF128Ghash/Basic.lean: The proof of root_satisfies_poly was rewritten from an one-liner using AdjoinRoot.eval₂_root to a calc block that explicitly reduces the root equation to AdjoinRoot.mk ghashPoly ghashPoly = 0. The new proof relies on set_option maxRecDepth 100000 to handle the large recursion depth, and the same option is also added to BF128Ghash_card (though its body is unchanged). No sorry or admit were introduced.
• CompPoly/Fields/Binary/BF128Ghash/Impl.lean: The diff modifies Impl.lean to replace anonymous instance blocks for Ring, DivisionRing, and Field with named instances (instSemigroupConcreteBF128Ghash, instRingConcreteBF128Ghash, instDivisionRingConcreteBF128Ghash, instFieldConcreteBF128Ghash), explicitly threading these instances through toRing/toDivisionRing fields instead of using inferInstance. It also adds explicit npow fields (npowRecAuto, npow_zero, npow_succ) to the instRingConcreteBF128Ghash definition, and replaces two simp proofs (nsmul_zero, zsmul_zero') in the AddCommGroup instance with rfl.

Additionally, set_option maxRecDepth 100000 and set_option maxHeartbeats 10000000 are added before the instDivisionRingConcreteBF128Ghash instance.

• CompPoly/Fields/Binary/Tower/Concrete/Basis.lean: In minPoly_of_powerBasisSucc_generator, the argument to congrArg was changed from q.toFinsupp.2 (an incorrect projection) to q.toFinsupp.coeff (the proper field name for the coefficient function of the underlying Finsupp), fixing the proof so that it correctly references the coefficient of the polynomial's support.
• CompPoly/Multivariate/MvPolyEquiv/Core.lean: The fromCMvPolynomial definition is updated: its body now wraps the Finsupp.mk term in an AddMonoidAlgebra.ofCoeff call, adapting to an upstream API change in how MvPolynomial (an abbreviation for AddMonoidAlgebra) is constructed. The coeff_eq lemma is changed from a := rfl definition to a by rfl proof block, which is a cosmetic refactor (likely to make the binder a explicit in the term, or to satisfy a changed elaboration requirement). No sorry or admit is introduced.
• CompPoly/Multivariate/MvPolyEquiv/Instances.lean: The diff refactors Instances.lean to replace the earlier MonoidAlgebra (multiplicative) representation with AddMonoidAlgebra (additive) across several lemmas. Specifically, foldl_eq_sum and fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial now use AddMonoidAlgebra.coeff instead of Finsupp.sum on the raw fromCMvPolynomial term. The map_mul proof is rewritten to operate on additive monoid algebra: multiplication a₁ * a₂ becomes addition a₁ + a₂, MonoidAlgebra.single becomes AddMonoidAlgebra.single, and the type of monomial exponents shifts from Multiplicative (Fin n →₀ ℕ) to (Fin n →₀ ℕ). The auxiliary lemma fromCMvPolynomial_F₁_eq_F₃ and the set bindings F₁, F₂, F₃ are updated accordingly. In the CommSemiring instance, the npow_succ proof is made explicit, using pow_succ to show x ^ (n + 1) = x ^ n * x. No sorry or admit are introduced.
• CompPoly/Multivariate/Operations.lean: Fixed the statement of fromCMvPolynomial_finsupp_sum by replacing two occurrences of the direct Finsupp.sum on fromCMvPolynomial a with AddMonoidAlgebra.coeff (fromCMvPolynomial a), aligning the lemma's hypotheses and conclusion with the actual type of the summand (AddMonoidAlgebra.coeff a provides the coefficient value, not the full polynomial).
• CompPoly/Multivariate/Rename.lean: The diff modifies two lemmas in CompPoly/Multivariate/Rename.lean to use the explicit accessor AddMonoidAlgebra.coeff on the underlying AddMonoidAlgebra representation of a CMvPolynomial, replacing previously implicit uses of fromCMvPolynomial as a direct Finsupp. Specifically, in fromCMvPolynomial_finsupp_sum, the original Finsupp.sum (fromCMvPolynomial a) g is changed to Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial a)) g, with a corresponding adjustment in the right-hand side. In fromCMvPolynomial_rename, the expression Finsupp.sum (fromCMvPolynomial p) (fun μ c => ...) is similarly updated to Finsupp.sum (AddMonoidAlgebra.coeff (fromCMvPolynomial p)) (fun μ c => ...). These changes ensure the code explicitly accesses the coefficient function of the additive monoid algebra, likely to align with a refactoring where fromCMvPolynomial no longer directly provides a Finsupp sum coercion.
• CompPoly/ToMathlib/MvPolynomial/Equiv.lean: This diff simplifies the proof of support_finSuccEquivNth. The old proof used the lemma support_coeff_finSuccEquivNth and explicit rw/simpa chains involving coeff/mem_support_iff/Finsupp.ne_iff. The new proof instead uses simp with ne_eq, MvPolynomial.ext_iff, coeff_zero, not_forall, and finSuccEquivNth_coeff_coeff, then provides a direct ⟨…⟩ argument in each direction based on insertNth_apply_same and insertNth_self_removeNth (via simpa). No new theorems or definitions are added, and the statement of support_finSuccEquivNth itself is unchanged.
• CompPoly/ToMathlib/Polynomial/BivariateDegree.lean: The file CompPoly/ToMathlib/Polynomial/BivariateDegree.lean is modified in a single location: the definition of evalX. Previously, evalX directly wrapped a Finsupp.mapRange in a Polynomial constructor. The change replaces this direct Finsupp.mapRange construction with an AddMonoidAlgebra.ofCoeff call applied to the coefficients of the mapped Finsupp, aligning the implementation with a newer or more idiomatic API for constructing Polynomial objects from coefficient data. No new theorems, definitions, or sorry/admit are introduced.
• CompPoly/Univariate/CMvEquiv.lean: In the private lemma mvToUnivariate_eq_map_finSuccEquiv, the proof of the MvPolynomial.C r case is expanded: it now explicitly uses change to rewrite with MvPolynomial.coeff (0 : Fin 0 →₀ ℕ) (MvPolynomial.C r) and adds a subsequent simp [MvPolynomial.coeff_C] to fill in the previously implicit equality. This fills a gap in the equational reasoning without adding any sorry or admit.
• CompPoly/Univariate/DivisionCorrectness.lean: The proof of the private lemma raw_divModByMonicAux_go_spec is refactored. The change rewrites the goal at two change statements to expose the full expression of step directly in the goal, rather than introducing the intermediate name step. The first constructor block is updated to use the rewritten equality hrel', which replaces hrel. The set_option maxHeartbeats 10000000 pragma is added to the lemma to increase the allowed heartbeat limit, likely because the refactored proof is more expensive to elaborate.
• CompPoly/Univariate/NTTFast/Correctness/Basic.lean: Refactored foldl_push_size and foldl_push_getD to replace the custom MProd record with the standard Array R × R pair type, updating all field accesses accordingly (b.fst/b.snd → b.1/b.2, ⟨...⟩ → (...)). This eliminates a dependency on the now-removed MProd structure without changing the theorems' statements or proofs.
• CompPoly/Univariate/NTTFast/Correctness/Pair.lean: The diff replaces all uses of the custom MProd type with the standard product type × (i.e., Array R × Array R) in the runStagesDIFRadix4PairWithTwiddles_eq_pair theorem and its auxiliary hfoldFst and hfoldSnd lemmas, and replaces constructor with apply Prod.ext to adapt the proof accordingly. This change simplifies the code by using Lean's built-in product type instead of a custom wrapper.
• CompPoly/Univariate/Quotient/Core.lean: In CompPoly/Univariate/Quotient/Core.lean, the proof of the zsmul_succ' field of the AddCommGroup (QuotientCPolynomial R) instance was modified: the previous simpa [zsmulRec] using nsmul_succ n a was replaced by an explicit change statement followed by exact nsmul_succ n a. This refactors the proof to avoid relying on the zsmulRec lemma, making the reasoning more direct.
• CompPoly/Univariate/ToPoly/Core.lean: In CompPoly/Univariate/ToPoly/Core.lean, the Raw.toPoly' definition is modified: the argument to Polynomial.ofFinsupp is now wrapped with AddMonoidAlgebra.ofCoeff. The theorem Raw.toPoly and the function toPoly for CPolynomial remain unchanged.
• 3 file(s) filtered as noise (lockfiles, generated, or trivial): lake-manifest.json, lakefile.lean, lean-toolchain

---

Last updated: 2026-07-14 12:20 UTC.

[github-actions]

Build Timing Report

• Commit: 7896ca8
• Message: Merge eca0eee into 0ec1f6e
• Ref: 432
• Comparison baseline: 0ec1f6e 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	377.45	1349.69	+972.24	exit 1
Warm rebuild	1.40	-	-	-
Test path	35.40	-	-	-

Incremental Rebuild Signal

• Clean:warm comparison is unavailable because one of the build measurements is missing.

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
63.00	43.00	+20.00	CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
42.00	45.00	-3.00	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean
29.00	28.00	+1.00	CompPoly/Bivariate/Deriv.lean
22.00	21.00	+1.00	CompPoly/Bivariate/ToPoly.lean
21.00	14.00	+7.00	CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean
19.00	20.00	-1.00	CompPoly/Univariate/Raw/Proofs.lean
19.00	19.00	+0.00	CompPoly/Univariate/NTTFast/Correctness/Radix4DIT.lean
17.00	17.00	+0.00	CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean
15.00	16.00	-1.00	CompPoly/Fields/KoalaBear/Fast.lean
15.00	15.00	+0.00	CompPoly/Univariate/NTTFast/Correctness/Radix4DIF.lean
13.00	6.80	+6.20	CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean
12.00	12.00	+0.00	CompPoly/Univariate/Basic.lean
12.00	12.00	+0.00	CompPoly/Univariate/NTT/Forward.lean
12.00	12.00	+0.00	CompPoly/Bivariate/Factor.lean
12.00	9.50	+2.50	CompPoly/Univariate/NTTFast/Correctness/DIF.lean
11.00	12.00	-1.00	CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean
10.00	10.00	+0.00	CompPoly/Data/Nat/Bitwise.lean
9.50	11.00	-1.50	CompPoly/Fields/Binary/AdditiveNTT/Domain.lean
9.20	8.10	+1.10	CompPoly/Fields/Basic.lean
9.20	9.80	-0.60	CompPoly/Multilinear/Basic.lean