[Vilin97]

Reduce the compilation cost of the existing CompactnessAndDegeneracy project while preserving every declaration. The project has approximately 19,000 lines in two large proof files; profiling identified arithmetic searches over large contexts, repeated finite-coordinate instance search, and a graph proof that simplified its entire context to prove a two-entry vector injective.

Base: 906301dff114598197af816aefe25211ff23a6b0. Head: 64c4d3d56e1542da4e20d200ee6fefb1f17a2c17. The live repository pins Lean/Mathlib 4.35.0; those pins are unchanged (Mathlib 56a005855ea17e0b0958f73ec801ae140b0a1679).

Changes

• Restrict arithmetic searches to the hypotheses actually used, using linear arithmetic when nonlinear preprocessing is unnecessary. Preserve the named intermediate inequalities and proof structure.
• Apply the existing binomial-probability recurrence directly with simpa only [mul_assoc] in both monotonicity proofs.
• Use LinearEquiv.map_zero in the two symplectic normalizer proofs, avoiding a costly generic ZeroHomClass search.
• Use Matrix.injective_pair_iff_ne for the two-center graph witness instead of four cases followed by simp_all on the graph context.
• Remove the private Mathlib.Data.SetLike.Fintype import identified as redundant by lake shake --keep-public.

Declaration invariant audit

Before editing, import all four owned modules into Lean with private bodies loaded, extensions disabled, and trust level zero. Enumerate constants from their module environment data, including private and generated declarations. Serialize structural expression DAGs for fully elaborated types and every available non-theorem value, retaining binder names/info, expression metadata, ordered universe parameters, declaration kinds, reducibility hints, safety/partial flags, and mutual groups. Compare every field exactly except theorem proof bodies, which are recorded separately by hash.

Result: 1,918 → 1,918 declarations; zero additions, removals, or invariant differences; 68 changed theorem bodies. No alpha-renaming normalization is used. The original base manifest reproduced byte for byte after an independent clean baseline build. The repository's source statement comparator also reports no changed statements or binders. Existing definitions, instances, structures, namespaces, and public names are preserved.

Manifest SHA256, base: 3ff80e557b9d95b273f4631a6b4e5dc17eb6a1c7ec254a41bb8c1d6057b288bb.
Manifest SHA256, head: c3ceee537aea73e8178d5dae2449b086796820b2530543ca53271a8a164437ca.

Controlled measurements

Before each sample, delete only this project's root and directory outputs under .lake/build/lib/lean/LeanPool/ and .lake/build/ir/LeanPool/. Keep pinned dependencies and the compiler-linter plugin warm, then run:

taskset -c 14 env LEAN_NUM_THREADS=1 \
  lake build LeanPool.CompactnessAndDegeneracy.Imports

Final samples are ordered base/head/base/head/base/head. Every run rebuilt all four owned modules without warnings. Source hashes were checked across all samples and against the final files. No other Lean compiler jobs from this cycle ran during timed samples.

Measurement	Base samples	Optimized samples	Base median	Optimized median
Wall seconds	102.29, 100.22, 102.60	90.52, 90.93, 90.64	102.29	90.64
User CPU seconds	94.75, 94.57, 94.31	85.13, 84.99, 84.30	94.57	84.99
Peak process RSS, KiB	2002684, 2002468, 2005956	1984616, 1980908, 1982592	2002684	1982592

Observed median wall-time reduction: 11.39%. User CPU reduction: 10.13%. RAM is reported as peak process RSS, with a 1.00% median reduction; the target is met through compilation time.

Synchronous command profiling (-DElab.async=false -Dtrace.Elab.command=true -Dtrace.profiler=true -Dtrace.profiler.useHeartbeats=true, suppressing nested traces) gives 867,433,790 → 716,829,800 raw declaration heartbeats (17.36% fewer) across the two files. Representative declaration counts:

Declaration	Base	Optimized
mem_thetaBaseExtensions_of_two_common_centers	8,578,973	381,535
symplecticLineNormalizer_apply_left	9,655,096	875,301
binomialProbabilityMass_succ_le_of_ge_mode	12,295,899	1,341,199
exists_entropy_exclusion_base	14,321,138	8,271,011

Validation

Passed:

lake build LeanPool.CompactnessAndDegeneracy.Imports
lake exe runLinter --no-build LeanPool.CompactnessAndDegeneracy.Imports
lake exe lint-style LeanPool.CompactnessAndDegeneracy.Imports
lake exe mk_all --module --check
lake shake --force --keep-public LeanPool.CompactnessAndDegeneracy.Imports
PYTHONPATH=python python3 -m lean_pool.quality --repo . --static-only
git diff --check

Also passed the unchanged repository quality functions for project declaration resolution, compiled axiom auditing on all four owned modules, and compiled option/backdoor auditing with all four modules selected. All controlled builds include the repository compiler-linter plugin. shake --force permits import analysis with this project's validated build while other pool projects remain unbuilt locally. The generated indexes are already current.

The VM is shared, so wall-time results describe this controlled configuration. CI will run full-pool validation and independent refactor review. This PR remains open for review, with auto-merge disabled.

[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 issue was found in this proof-only refactor.

Summary

This proof-only refactor narrows arithmetic searches and replaces broad automation with direct lemmas.

• Lean searches only named facts in many Compactness and Degeneracy proofs.
• Binomial probability proofs use the recurrence with a direct rewrite.
• The two-center graph proof gets injectivity directly from distinct centers.
• Symplectic coordinate proofs name the linear equivalence’s zero rule.

_{Reviews (1) · Last reviewed commit: "perf(CompactnessAndDegeneracy): reduce p..." · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

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

Reviewed head: 64c4d3d56e1542da4e20d200ee6fefb1f17a2c17

Verdict: ✅ approve

The refactor restricts arithmetic searches to explicit facts and replaces broad searches with direct recurrence, injectivity, and linear-equivalence lemmas. It retains intermediate inequalities, proof structure, and reusable helpers, making dependencies clearer and failures easier to localize. No actionable maintenance regression was found. The targeted build stopped when fetching pinned Mathlib returned HTTP 403, so compilation and reported speedups were not independently verified.

Aspect	Value
Scope	proof elaboration optimization
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The refactor makes proof dependencies explicit and removes unnecessary search without sacrificing structure or reusability.

---

Tokens: 1,172,137 in / 7,550 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $4.8018 (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]

Independent source review at 64c4d3d56e1542da4e20d200ee6fefb1f17a2c17.

{
"summary": "This refactor makes proof dependencies in CompactnessAndDegeneracy more explicit. Arithmetic tactics use the facts needed at each step, binomial monotonicity uses the existing recurrence, the symplectic proofs name the linear equivalence's zero lemma, and the graph witness uses the existing injective-pair characterization. Intermediate inequalities and reusable helpers remain intact; no maintenance regression was found.",
"assessment": {
"scope": "proof elaboration optimization",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The changes reduce unnecessary proof search while retaining the mathematical argument and its debugging structure."
},
"verdict": "approve",
"findings": []
}

I reviewed both complete file diffs and all 78 changed written proof commands. The 932 written declaration headers and non-proof commands are retained; the only import deletion is private. Two independent source reviews reached the same conclusion.

Authored validation is qualified on the exact head: all six applicable workflows completed successfully, including the canonical Build project and the pool's index, build, lint, style and repository-quality steps. Six required contexts were valid source-scope skips. This does not independently establish the author's private timing or elaborated-environment measurements.

Source acceptance is recorded here. Protected integration still requires the applicable validation of the current main and the native merge candidate.