perf: speed up InfiniteConnesRigidity proofs and imports

[Vilin97]

Summary

Daily optimization cycle, target: LeanPool/InfiniteConnesRigidity (5 modules, 40.2k lines, imported 2026-09-13 in #393). It was selected as the most expensive project per line in the pool: its import-PR CI profile shows 30,681 maxHeartbeats units and a 639 s serial lean --profile sum for only five files, about 3× the per-line cost of the next candidate (GapCVP), and it had never had an optimization pass. A CPU-time sweep over 385 files of 25 other large projects (ClassificationOfSurfaces, PhaseRetrieval, SpherePacking, Monlib4, OSforGFF, …) found no file above 130 CPU-s, versus this project's 90–160 s files.

No statement, definition, instance, notation, or public name changes; proof terms and elaboration paths only, plus three new private helper lemmas and an import cleanup.

Measurements

Clean lake build LeanPool.InfiniteConnesRigidity with prebuilt Mathlib oleans (32-core WSL2 host, load < 3, project artifacts deleted from .lake/build/{lib/lean,ir} before each run, base and head worktrees sharing the same .lake/packages; runs interleaved head / base / head):

	base 8d2d0c5 (project files identical at 4de4e26, the PR base)	head run 1	head run 2	head run 3 (pushed state)
wall	118.0 s	93.7 s	91.8 s	93.7 s
user CPU	262.7 s	228.3 s	228.1 s	228.0 s
sys CPU	13.8 s	13.6 s	13.5 s	13.6 s

Per-module Lake times (the modules form a linear import chain, so wall ≈ their sum):

module	base	head
UniversalLattice	31 s	21 s
CarryAndCrossedProduct	29 s	21 s
SpectralAndPropertyT	24 s	22 s
GroupConstruction	15 s	13 s
FactorAndRigidity	18 s	17 s

Overall: −21 % wall, −13 % user CPU. Per-declaration attribution came from lake env lean -Dtrace.profiler=true -Dtrace.profiler.threshold=200 run with the lakefile options (maxSynthPendingDepth=3, the Mathlib linter set) and confirmed in truncated copies of the real files, e.g. l2Reindex 9.2 s → 0.4 s, crossedIndexEquiv 7.4 s → 0.4 s, polynomial_valuation_coefficient_ascent statement 5.1 s → 0.1 s, IntegerElementaryProof.upperUnitriangular_factorization 4.9 s → 0.45 s, mennickeBlock_rotation_conjugate 3.3 s → 0.45 s, unitEntry_diagonalUnitPair_apply 2.9 s → 0.35 s, unitary_mem_normalFixedSubmodule 0.61 s → 0.15 s.

Invariant audit

A declaration manifest was recorded from the base oleans and from the final head oleans with a Lean script (importModules over the five modules, every constant: kind, safety, reducibility hints, universe parameters, reducibility status, instance status and priority, simp membership, protected/private, Expr.hash of the type, hash of the value, hash of the value with all proof subterms erased via Meta.transform, and a pp.explicit rendering of the type).

Result: 4544 declarations in the base, 4546 in the head. The only differences are

• 7 removed / 9 added simp-generated auxiliary lemmas (*._simp_1_N) and 4 whose statements changed — all internal auxiliaries of the rewritten proofs;
• 3 added private helpers: MennickeIdentity.specialLinear_transvection_mul_apply (UniversalLattice) and specialLinear_mul_transvection_apply (CarryAndCrossedProduct, GroupConstruction);
• 63 declarations whose proof term changed (theorems and _proof_N auxiliaries of definitions); every definition's value and proof-erased value hash is unchanged.

#print axioms of ConnesRigidity.infiniteConnesRigidity, of the second main result, and of the edited definitions: propext, Classical.choice, Quot.sound only.

Changes

• lp reindexing (l2Reindex, crossedIndexEquiv): pass (f := fun i ↦ ‖f i‖ ^ (2 : ℝ≥0∞).toReal) to Equiv.summable_iff; expected-type propagation previously spent 5 s unfolding Summable/HasSum/Filter.map before failing and retrying. The elaborated definitions are identical (rfl-checked and manifest-checked).
• Statement elaboration: polynomial_valuation_coefficient_ascent gets let s : ℕ := / let f' : Polynomial A := ascriptions; the elaborated proposition is byte-identical (manifest), elaboration drops from 5 s to 0.1 s.
• Matrix identities over Fin 3/Fin 4 (unipotent factorizations in UniversalLattice and GroupConstruction, Mennicke block lemmas, mennickeBlock_rotation_conjugate, unitEntry_diagonalUnitPair_apply, mennickeBlock_mem_of_isUnit_topRight, Cornulier row/column root products): replace Matrix.mul_apply/Fin.sum_univ_* expansions (3⁵–4⁵ terms per entry) with entrywise transvection peeling through the private helpers, simp only lists collected in context, and ring.
• Generic hom lemmas: rw [map_mul] on UnitaryRepresentation → MonoidHom.map_mul (52 rewrite sites in SpectralAndPropertyT, each saved a 0.25 s MulHomClass search); map_star/map_mul/map_add on StarAlgEquiv → the map_star'/map_mul'/map_add' fields; mul_left_comm in a simp only → ring; mul_comm in a simpa only → div_eq_inv_mul; simp_all → simp_all only; change goals spelled with SemidirectProduct (Multiplicative D) K kDAction use the existing Lambda abbreviation.
• Imports (lake shake --force --fix): CarryAndCrossedProduct drops 6 unused public imports and demotes 8 to plain import; SpectralAndPropertyT drops 4 and demotes 2. UniversalLattice, GroupConstruction and FactorAndRigidity were already minimal.

Commands run

lake build LeanPool.InfiniteConnesRigidity                 # base + head, clean, warning-free
lake shake --force --explain / --fix LeanPool.InfiniteConnesRigidity
lake env lean -DmaxSynthPendingDepth=3 -Dweak.linter.mathlibStandardSet=true \
  -Dtrace.profiler=true -Dtrace.profiler.threshold=200 <module>.lean
lake exe runLinter --no-build LeanPool.InfiniteConnesRigidity{,.UniversalLattice,...}   # passed
lake env <mathlib>/lint-style LeanPool/InfiniteConnesRigidity.lean LeanPool/InfiniteConnesRigidity/*.lean  # clean
lake exe mk_all --check                                    # "No update necessary"
python: quality._run_option_audit(root, [the six modules]) # 0 errors
python: quality.run_checks(root, skip_lean_axioms=True)    # 0 errors mentioning this project
lake env lean --run Manifest.lean ...                      # base vs head manifest diff (above)

Limitations

• The whole-pool quality checker and runLinter LeanPool were not reproduced locally (single-project worktree without the other 158 projects' oleans); CI runs them.
• Remaining hot spots are flat: the largest is parkWoodburn_mennicke_identity (~5 s, fourteen !![…] intermediate identities, now simp only), then ~1–2 s each (rankTwoParabolicSpecialLinear_*, stabilizedTwoByTwo_mem_elementaryThree_of_topLeft_isUnit, lambdaGroupFactorUnitary_*). Statement-level costs from instance searches on ↥B (~0.3 s per declaration mentioning it) were left untouched because any shortcut instance would change the elaborated statements.

🤖 Generated with Claude Code

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

The PR appears safe to merge, with no outstanding prior findings or newly introduced actionable defects.

Summary

This PR optimizes elaboration in the five InfiniteConnesRigidity modules without changing their mathematical interfaces.

• Replaces expensive finite-matrix expansions with shared entrywise transvection lemmas and narrower simplification sets.
• Qualifies generic homomorphism rewrites and adds explicit expected types to reduce typeclass and elaboration search.
• Removes or demotes unnecessary public imports.
• Consolidates the downstream transvection helper into UniversalLattice.

_{Reviews (14) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

⚠️ 1 declaration changed their statement across 1 file — a statement change is more than a refactor. Confirm each one is intended.

⚠️ Statements changed (1)

• ConnesRigidity.polynomial_valuation_coefficient_ascent — LeanPool/InfiniteConnesRigidity/UniversalLattice.lean

Also: 3 declarations added, 0 removed. A reorganization moves declarations between files, which shows up here as an add in one file and a remove in another.

➕ Declarations added (3)

• ConnesRigidity.specialLinear_mul_transvection_apply — LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean
• ConnesRigidity.ElementaryGenerationProof.specialLinear_mul_transvection_apply — LeanPool/InfiniteConnesRigidity/GroupConstruction.lean
• ConnesRigidity.MennickeIdentity.specialLinear_transvection_mul_apply — LeanPool/InfiniteConnesRigidity/UniversalLattice.lean

Statements are compared textually against the merge base (comments and whitespace ignored; by proof terms embedded in a type are treated as proof-irrelevant), the same method as physlib's /check-golf. Anonymous instances and examples are not tracked.

Compile cost of modified files — base → head

Heartbeats: 30,667 → 30,672 (+5, +0.0%). Declarations: 2,412 → 2,415.

Per-file wall sum: 553.9 s → 411.4 s (-25.7%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal.

Files: 5 compared — 0 cheaper, 0 costlier, 5 within noise (threshold: |Δ heartbeats| ≥ 1,000 and ≥ 1%).

Both sides are elaborated against the merge-base build of the pool — sound when only proofs and definition bodies change; a file whose statements changed may fail there and is flagged ⚠. Heartbeats come from Mathlib's linter.countHeartbeats, in maxHeartbeats units. Δ lines counts added/deleted lines from this PR diff.

File	Δ lines	HB base	HB head	Δ HB	Δ HB %	Wall base (s)	Wall head (s)
LeanPool/InfiniteConnesRigidity/UniversalLattice.lean	+140/-96	2,693	2,696	+3	+0.1%	96.47	60.96
LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean	+41/-37	9,175	9,177	+2	+0.0%	173.20	112.57
LeanPool/InfiniteConnesRigidity/GroupConstruction.lean	+20/-10	2,632	2,634	+2	+0.1%	81.29	67.55
LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean	+57/-55	9,508	9,506	-2	-0.0%	94.79	80.42
LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean	+6/-12	6,659	6,659	+0	+0.0%	108.13	89.94
Total	+264/-210	30,667	30,672	+5	+0.0%	553.9	411.4

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[Vilin97]

Final exact-head review at 73ab4dd2a5 (refactor standard, 2026-09-18). This is the equivalent approval comment: GitHub does not permit self-approval on an automation-authored PR.

Scope. Proof-level optimization of LeanPool/InfiniteConnesRigidity (5 modules, 40k lines): three new private transvection-entry lemmas (specialLinear_mul_transvection_apply, specialLinear_transvection_mul_apply) replace repeated 20-lemma simp sets across the Mennicke/Cornulier block computations; bare simp [...]/simp_all [...] calls become explicit simp only [...] lists; map_mul becomes MonoidHom.map_mul where elaboration was searching; two lets in a private theorem gain type ascriptions (the one "statement change" the profiler flagged — same statement, private declaration); and unused Mathlib imports are dropped or demoted from public import to import. No public declaration, definition, instance, or notation changes; runLinter, lint-style, mk_all --check, the repository axiom audit over 690 declarations, and the option audit pass locally.

Reconciliation with main. After the v4.34.0 bump (#436) the branch conflicted in one hunk of GroupConstruction.lean (main's ← Submodule.norm_coe rename versus this PR's div_eq_inv_mul simplification; merged as simpa only [← Submodule.norm_coe, div_eq_inv_mul]), and Mathlib.Analysis.Matrix.Order had to be re-imported in SpectralAndPropertyT.lean because Mathlib 5ed29652 no longer reaches Matrix.PosSemidef.hadamard transitively. Both are in f48835e5; the project tree at this head is identical to it.

Maintainability. Improved rather than traded away: the explicit lemma lists and shared helpers are more robust to simp-set drift than the bare simp calls they replace, and the structure of every proof is preserved. Measured cost on the author's 32-core host: clean project build 118 s → 93 s wall (−21%), three interleaved runs; CI Build project is green on this head.

Merging by protected squash once the required checks report.

[Vilin97]

Final exact-head note at 4c7c75bc3f (auto-rebase merge of main after #450): project tree identical to c11de0db, which adds the shared transvection lemma (Greptile's dedup finding) on top of the reviewed f48835e5; Build project (sharded, cold cache), separation, and documentation preflight are green here and all threads are resolved. Merging by protected squash.