Optimize InfiniteConnesRigidity matrix and operator proofs

[Vilin97]

The existing 40,274-line InfiniteConnesRigidity project has a large import closure and concentrated compilation costs in finite matrix calculations and nested Hilbert-space operator proofs. This factors those arguments into reusable lemmas, uses Mathlib's extensionality results, removes 28 unused private imports, and removes four superseded private helper proofs whose callers have been replaced.

• Compute the Mennicke word using whole three-by-three shear and block-product equalities; reuse entry elimination in the remaining finite matrix proofs. Share four-by-four entry elimination across the parabolic, Cornulier root-product, row-clearing and triangular-factorization calculations. Eliminate impossible equal root indices before computing parabolic entries.
• Prove bicommutant membership and equality of generated bicommutants once, then apply them to the crossed-product generators.
• Compose matrix coefficient maps before evaluating them; reuse constant-matrix evaluation in the Suslin path proofs.
• Establish conjugation through an intertwining identity and reuse it for the factor, Haar-action and Fourier operators. Apply the general vacuum theorem to the split-factor vacuum; use direct equality chains for the concrete factor generators.
• Factor normalized-displacement calculations and the quantitative orthogonal-residual estimate used by the pullback Kazhdan-pair proof. Transport centralizer membership at the star-algebra level before specializing to Hilbert-space operators.
• Replace broad simplifier searches throughout the touched foundation, spectral, carry, group and factor theorem proofs with explicit lemma lists, retaining required unfoldings. Use span extensionality for the diagonal generators and polynomial ring-hom composition for symbolic base change.
• Lower the speculative additive-group instance priority locally in the foundation module, matching the other implementation modules; its imported priority remains 1,000. Prove the semidirect-product conjugation identity in a generic commutative group before specializing it.
• Check the Fourier covariance maps on the scalar generator 1; use ContinuousLinearMap.ext_on for the dense character span; obtain the quotient uniformizer inverse directly from its defining relation.

Measurement baseline: 49cfa8b01a2ac02678202883192a00935ec4a14d. Measured refactor head: 69cb4616a5bd200e83584910c80f84d427af3b94. Cleanup head: 20ea9bdfd14306b2b55e2b120a5eb1eb2266ec23.

The cleanup removes the private lemmas splitFourierEquiv_single_smul, lambdaDelta_apply, splitVacuum_apply and fourierUnitary_single_smul, together with their attached scope wrappers. Their callers already use the shared replacements. All other source bytes are preserved apart from four redundant separator lines.

The measurements, compiled-declaration manifests and validation results below describe the measured refactor head 69cb4616a5bd200e83584910c80f84d427af3b94 before this cleanup. They are historical author validation. The cleanup intentionally removes those four named private declarations; it makes no claim that the old all-declarations-preserved manifest or timing results were reproduced at the cleanup head. Current-head CI and independent review are separate requirements.

Uses the existing Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e pins.

Revision	Run	Wall seconds	User seconds	System seconds	Max process RSS KiB
base	1	185.75	298.76	6.75	2,295,520
head	1	171.81	271.59	6.68	2,196,868
head	2	164.61	268.33	6.50	2,196,280
base	2	189.92	302.92	6.82	2,294,444
base	3	167.50	288.52	6.88	2,289,296
head	3	161.40	266.09	6.58	2,194,076

Median clean build wall time: 185.75 → 164.61 seconds (11.38% lower). Median maximum process RSS: 2,294,444 → 2,196,280 KiB (4.28% lower). Median user CPU time: 298.76 → 268.33 seconds (10.19% lower).

Each measurement runs /usr/bin/time around lake --wfail build LeanPool.InfiniteConnesRigidity.Imports. Before each run, only this project's artifacts under .lake/build/lib/lean/LeanPool and .lake/build/ir/LeanPool are removed. Dependency artifacts and the filesystem cache stay warm. Three runs per revision use the counterbalanced order base/head/head/base/base/head, with identical options, frozen source hashes, and no other local compilers or active profiling/Lean validation processes. RSS is the maximum single-process resident set, not aggregate concurrent memory. The Azure VM is shared, so scheduling adds wall-time variation. Pilot builds and diagnostic profiles are excluded from these totals.

Synchronous declaration timers identified the Mennicke identity, parabolic matrix calculations, and operator conjugation/Fourier proofs as concentrated costs. These diagnostic profiles are separate from the clean-build measurements. The lattice module's environment shrinks from 5,021 modules / 471,412 constants to 4,707 / 437,456; the spectral module shrinks from 5,225 / 486,948 to 5,111 / 477,703.

The pre-edit Lean environment manifest records every owned declaration, including private and generated declarations. The comparison checks fully qualified names, exact universe parameter lists, elaborated types, safety/partial flags, every non-theorem body, reducibility and mutual metadata, and inductive/constructor/recursor data. Only theorem proof bodies, bound-variable alpha names and nonsemantic expression metadata are excluded. All 4,580 original declarations match; none disappears. 14 supporting lemmas and 48 generated private simplifier lemmas are added. The independent source audit preserves all 2,545 original named signatures. All 362,601 original exported public names remain; six supporting lemmas are added publicly. All existing public imports remain. At the measured refactor head, private auxiliaries were retained even when their callers were replaced to preserve that exact original declaration set. The later cleanup deliberately removes the four unused private helpers listed above.

Historical author validation at 69cb4616a5bd200e83584910c80f84d427af3b94:

• Warning-failing project builds, including every measured clean build.
• CI's lake env lean --run scripts/ci/lint-project.lean over all seven project modules: 4,642 declarations, zero findings.
• lake exe lint-style LeanPool.InfiniteConnesRigidity.Imports.
• The unmodified repository quality checker on an exact project-only validation view: headers, forbidden code/options, size limits, registry/card/reachability/index checks, axiom checks and the compiled backdoor audit.
• lake exe mk_all --module --check --repo <project-only validation view> and lake shake --force --keep-public LeanPool.InfiniteConnesRigidity.Imports.
• Source-signature, full declaration-manifest and public-export comparisons; frozen measured-source fingerprints; git diff --check.

Only this existing project's five Lean implementation files change. Its registry card, generated imports, LeanPool.lean, dependency pins and gates remain fixed. Whole-pool CI and independent refactor review remain required. Auto-merge is not enabled.

[greptile-apps]

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

[Low impact] No blocking code issue was found in the latest private-helper cleanup.

Summary

Refactors matrix and operator proofs into shared lemmas and removes unused private imports. The latest revision deletes four private helpers whose callers were replaced earlier.

• The Mennicke word is computed through whole-matrix steps.
• Four-by-four matrix proofs share one entry-checking helper.
• Operator proofs reuse shared conjugation and bicommutant results.
• Spectral proofs reuse normalized-displacement and residual estimates.
• Suslin path proofs compose coefficient maps before evaluating matrices.
• Touched proofs use explicit simplification rules and fewer private imports.

_{Reviews (2) · Last reviewed commit: "refactor(InfiniteConnesRigidity): remove..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "At 69cb461, I reviewed all five complete diffs and the helper/caller contracts. The Mennicke calculation retains its named intermediate matrices while sharing shear and block-product identities. Intertwining, bicommutant, dense-span and normalized-displacement lemmas replace repeated operator and Kazhdan arguments with the same hypotheses. Explicit simplifier lists preserve the mathematical structure, and the instance-priority adjustment is local. Public imports, the project entry/card, dependency pins and gates remain fixed. Four superseded private helpers are deliberately retained for original-declaration compatibility; this small, unchanged residue is acceptable. The timing and compiled-manifest results in the description are attributed author validation, not runs reproduced by this review. Hosted validation and the current configured review remain separate admission requirements.",
"assessment": {
"scope": "matrix and operator proof refactor",
"introduces_tech_debt": true,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "Shared lemmas improve reuse and robustness; the small, explicitly retained private-helper residue does not require a pre-merge source change."
},
"verdict": "approve",
"findings": [
{
"file": "LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean",
"line": 3509,
"rule": "dead-leftover",
"comment": "splitFourierEquiv_single_smul, lambdaDelta_apply (4169) and splitVacuum_apply (4185) lose their callers after the ext_ring/general-vacuum substitutions. Their unchanged private proofs are deliberately retained for the documented original-declaration manifest. This is a small maintenance residue that I accept; no pre-merge repair is required."
},
{
"file": "LeanPool/InfiniteConnesRigidity/GroupConstruction.lean",
"line": 7890,
"rule": "dead-leftover",
"comment": "fourierUnitary_single_smul similarly becomes unused when the conjugation proof checks the scalar generator 1. Retaining its unchanged private declaration is part of the same bounded compatibility choice, not a correctness or public-API defect requiring a repair."
}
]
}

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: 20ea9bdfd14306b2b55e2b120a5eb1eb2266ec23

Verdict: ✅ approve

The refactor shares matrix calculations, operator conjugation arguments and displacement estimates while preserving intermediate proof structure. Explicit simplifier dependencies and Mathlib extensionality lemmas reduce reliance on broad automation. The four superseded private helpers are removed, and the replacement helpers have callers. Independent compilation and timing verification were blocked because Lake’s Mathlib fetch returned HTTP 403.

Aspect	Value
Scope	proof refactoring and import pruning
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The refactor improves reuse and makes proof dependencies more explicit without introducing actionable maintenance debt.

---

Tokens: 1,685,879 in / 8,441 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $6.8701 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

I have reconciled configured review 2184 with my earlier acceptance of the bounded private-helper residue. I am applying the prepared two-file cleanup to remove the four unused private helpers and their attached scope wrappers (70 deletions including separator lines). The shared replacement proofs are retained.

The original measurements and compiled-declaration comparisons remain historical evidence for 69cb4616a5bd200e83584910c80f84d427af3b94; the cleanup intentionally changes the private declaration set. I will label that scope in the description. Fresh current-head CI and the normal configured review remain required.

[Vilin97]

{
"summary": "At 20ea9bd, the reviewed matrix/operator refactor at 69cb is retained and the four superseded private helpers identified in review 2184 are removed. I checked the complete two-file follow-up diff: four private theorem blocks, their attached scope wrappers and surplus separators, with 70 deletions and no additions. Forward and inverse patches reconstruct the authenticated source exactly, and the published commit has 69cb as its sole parent. Every other source byte, public declaration, import, card, pin and gate is retained. The earlier timing and compiled-manifest results are explicitly historical for 69cb; they are not transferred to this head. Current-head hosted validation and the configured review remain separate requirements.",
"assessment": {
"scope": "matrix/operator refactor and unused private-helper cleanup",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The shared proofs retain their structure, and the unused private proofs flagged by the configured review have been removed."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

/review

Please review current head 20ea9bdfd14306b2b55e2b120a5eb1eb2266ec23. It removes the four unused private helpers identified in configured review 2184 at 69cb4616a5bd200e83584910c80f84d427af3b94, as documented in the exact-head source review.

The current-head CI run passed index validation, build, lint, text style, repository quality and canonical Build project.