[Vilin97]

SpherePacking is a 55,580-line analytic project with a long compilation chain. This change reduces elaboration work in eight existing modules while preserving every existing declaration, including private and compiler-generated declarations.

The main changes are:

• Replace 311 linear-programming searches with explicit linear combinations and 16 more with direct uses of existing facts, selected from successful measured candidates. Supply explicit facts to the remaining arithmetic searches, and replace successful aggressive conversions, inequality searches, and continuity searches with cheaper conversions or named lemmas.
• Prove the imaginary gamma-product identity directly from Euler's reflection formula and Complex.sin_mul_I. Normalize the centered-kernel identity with explicit cast rewrites and ring, avoiding ordered associative/commutative simplification.
• Narrow broad simplification to the named local definitions and required cast lemmas at measured sites; retain successful cheaper numeric and positivity proofs. Shorten the derivative/integral interchange proof by normalizing the successor derivative before applying the integral commutation lemma.
• Factor the duplicated polynomial frequency-ratio estimate into one private theorem. Reduce the cubic-growth estimates to real polynomial inequalities at the start, and reuse the existing lower norm bound.
• Use explicit product/power inequalities in the cubic-window, Gaussian-error and gamma-tail estimates, and cache canonical Euclidean instances at seven measured proof sites.
• Remove seven private imports after eliminating incidental instance/simplification dependencies. The loaded import graph shrinks from 5,059 to 4,910 modules (149 fewer). Their compiled artifacts total 124.7 MiB; this figure is dependency size, not measured peak RAM. Public imports stay identical.

SpherePacking was selected from larger existing projects after inspecting its compilation chain and profiles; MetricCodes, GapCVP and ClassificationOfSurfaces were also considered. No project is imported or vendored. Project membership, definitions, statements, names, attributes, metadata, generated indexes and repository gates are unchanged.

Declaration invariant

Exact base: edbe5bd56f476cc2965564676b66199f281ab714. Tested head: f48357d7f74416891ac8428e0743efe2fd4c0916.

Current main advanced during this cycle to 56e877945082f3dab9f43c8e3d80435118a91446. The selected project/card, pinned toolchain/dependencies, and relevant contribution/review rules are unchanged between the recorded base and that revision. The isolated author branch is preserved without rebasing to chase main.

Before editing, a standalone Lean environment-inspection program imported LeanPool.SpherePacking.Imports with importAll := true and enumerated each owned module's constNames. It serialized every declaration's name, universe parameters, full raw Expr type, kind/safety/reducibility metadata, inductive/constructor/recursor metadata, and every non-theorem value. Only theorem proof bodies were excluded from comparison.

PASS: all 3,858 original declarations are present and every recorded field is byte-identical. No binder-name or type normalization was used. Head has 3,867 declarations: the new private ratio lemma and eight private simplification lemmas generated by the gamma proof. No declaration is shadowed or replaced.

Manifest SHA-256 values:

• Base: 11aa00091cf9452248876e4dc783c774932461a720fd2c714213a137b409a9ee
• Head: d802a16c175ec3fb62ffcf95ff50a72bf01430ba78494b18193e10d23a65be31

A separate source audit verifies all 2,192 parsed original declaration signatures exactly, and all non-theorem/non-import commands byte-for-byte. It allows only the seven recorded private-import removals and checks public import commands exactly. Audit programs, raw manifests, source snapshots and logs are retained at /data/codex/scratch/researcher/optimization-20261102T1315 on the VM.

Compilation measurements

Trial	Source	Wall seconds	User CPU seconds	Total CPU seconds	Peak RSS KiB
1	base	248.80	437.34	451.35	2,144,404
2	head	184.45	385.78	393.99	2,036,480
3	head	213.11	395.77	404.14	2,041,192
4	base	266.42	433.34	444.83	2,142,360
5	base	253.94	429.45	438.47	2,154,124
6	head	190.65	381.54	390.28	2,050,220

Median wall time: 253.94 → 190.65 seconds (24.92% lower).
Mean wall time: 256.39 → 196.07 seconds (23.53% lower); paired geometric reduction: 23.64%.
Median total CPU time: 444.83 → 393.99 seconds (11.43% lower). Median peak RSS: 2,144,404 → 2,041,192 KiB (4.81% lower).

Method: six complete project rebuilds in the predetermined order base, head, head, base, base, head. Each trial deletes only this project's .lake/build/lib/lean/LeanPool/SpherePacking* and .lake/build/ir/LeanPool/SpherePacking* outputs. Pinned dependencies remain built and filesystem caches remain warm. Both versions use the same worktree, dependencies, machine and command, with two Lean workers, matching the original controlled baseline:

LEAN_NUM_THREADS=2 /usr/bin/time -v lake --wfail build LeanPool.SpherePacking.Imports

No other profiling or validation process from this cycle runs during timed trials. The shared VM has substantial unrelated load, so observed wall-time changes have that limitation; user CPU time and peak RSS are reported alongside them. These measurements cover the selected project, including unchanged modules and generated imports, rather than the whole pool. /usr/bin/time -v peak RSS is the maximum individual process high-water mark, not the sum of simultaneous child processes.

Synchronous command profiling, including kernel checking, measured 3,102,024 → 1,236,158 raw heartbeats for the direct gamma-product proof (60.15% fewer). The centered-kernel rewrite measured 5,505,419 → 500,845, and the derivative/integral proof 34,977,354 → 29,307,174, against matching imported environments. The kernel profile preceded removal of one unused simplifier argument, which the warning-fatal build caught and which is absent from the final source.

Earlier exploratory passes are retained separately. Before the import/helper/instance changes, a six-trial run with LEAN_NUM_THREADS=2 gave median wall times 173.57 → 163.89 seconds (5.58%). An earlier default-worker pass gave medians 195.04 → 164.74 seconds (15.54%), means 188.09 → 179.88 seconds (4.36%), user CPU 404.74 → 373.77 seconds (7.65%), and peak RSS 2,145,784 → 2,056,288 KiB (4.17%). Its spread prompted the additional proof pass above; it is not the final-source measurement. A later default-worker checkpoint, before the final direct-arithmetic pass, gave median wall time 206.20 → 184.32 seconds (10.61%), mean 206.59 → 187.56 (9.21%), paired geometric reduction 8.95%, median CPU total 430.12 → 396.85 (7.74%), and peak RSS 2,152,032 → 2,053,592 KiB (4.57%). The final controlled series is reported above.

Validation

• Warning-fatal full selected-project build: lake --wfail build LeanPool.SpherePacking.Imports
• The repository's slow declaration linters: lake env lean --run scripts/ci/lint-project.lean over all ten project modules — 3,867 declarations passed
• lake exe lint-style LeanPool.SpherePacking.Imports
• lake exe mk_all --module --check
• Exact compiled-manifest and source-signature/frozen-command audits
• Scoped existing repository quality functions: headers, forbidden tokens/options, file/proof sizes, reachability, project card/schema/declarations, public axiom closure, and the backdoor audit over every project declaration
• git diff --check
• lake shake --force --keep-public --explain LeanPool.SpherePacking.Imports inspected during dependency analysis

The existing repository pin is Lean/Mathlib 4.35.0-rc3, Mathlib c55e6e786f49471c72fbddbec5415808896aec1e; it is unchanged. Full repository CI and independent review remain required. This PR is open for review, with auto-merge disabled and no queue or merge action. The infrastructure recovery hold remains respected; daily documentation publishing is assessed separately from protected validation workflows.

[greptile-apps]

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

[Medium impact] No blocking issue was found in this proof-only refactor.

Summary

Replaces broad proof searches with explicit facts across eight existing SpherePacking modules.

• SpherePacking builds its proofs with less elaboration work.

The previous-review comparison was not used: the two commits have different merge bases with the supplied target commit. The full PR diff was reviewed instead. No previous finding threads were supplied.

_{Reviews (2) · Last reviewed commit: "Merge current main for SpherePacking com..." · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 2,193 tracked declarations across 8 modified files kept their type; only proofs / definition bodies changed.

Also: 1 declaration 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 (1)

• CohnElkies.polynomial_uniform_frequency_ratio_le — LeanPool/SpherePacking/GammaAnalysis.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: 6,551,785 → 6,024,828 (-526,956, -8.0%). Commands: 3,631 → 3,632.

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

Files: 8 compared — 7 cheaper, 0 costlier, 1 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 disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted to maxHeartbeats units. Failed measurements are not classified as cheaper or costlier. Δ lines counts added/deleted lines from this PR diff.

File	Δ lines	HB base	HB head	Δ HB	Δ HB %	Wall base (s)	Wall head (s)
LeanPool/SpherePacking/HarmonicAnalysis.lean	+383/-296	772,864	562,481	-210,384	-27.2%	140.85	115.38
LeanPool/SpherePacking/RadialConstruction.lean	+258/-235	678,281	607,938	-70,343	-10.4%	137.10	134.31
LeanPool/SpherePacking/GammaAnalysis.lean	+368/-477	694,070	624,678	-69,392	-10.0%	174.11	125.07
LeanPool/SpherePacking/MellinAnalysis.lean	+221/-195	706,051	643,808	-62,243	-8.8%	145.65	126.97
LeanPool/SpherePacking/SaddleAnalysis.lean	+184/-150	593,533	533,866	-59,668	-10.1%	88.27	89.71
LeanPool/SpherePacking/Foundations.lean	+142/-114	733,433	695,158	-38,275	-5.2%	129.69	163.67
LeanPool/SpherePacking/Conclusion.lean	+9/-26	416,644	407,036	-9,608	-2.3%	112.62	98.18
LeanPool/SpherePacking/PackingBound.lean	+31/-30	1,956,907	1,949,864	-7,043	-0.4%	219.86	222.98
Total	+1,596/-1,523	6,551,785	6,024,828	-526,956	-8.0%	1148.2	1076.3

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

[Vilin97]

{
"summary": "At f48357d, this eight-file SpherePacking refactor replaces broad proof search with explicit arithmetic certificates, named analytic lemmas and targeted rewrites. The original written declaration headers, non-theorem data, scopes and public imports are preserved; the new private gamma-ratio lemma has two callers. The proof arguments and their domain, sign and integrability conditions remain intact. This is a static source approval: the author's private compiled-manifest and timing claims were not independently validated, and hosted CI, current-main qualification and native queue checks remain separate. Public advisory profiling reports 8.1% fewer heartbeats across all eight files; its parallel-load wall totals are not a controlled project benchmark.",
"assessment": {
"scope": "targeted arithmetic and analytic proof rewrites with private-import narrowing",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "The refactor makes the existing arguments more explicit and reduces duplicated reasoning without an actionable maintenance regression."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

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

Reviewed head: c149b237ebd2389e2ded6e88762d2be8383933f4

Verdict: ✅ approve

The refactor replaces broad searches with explicit facts and named lemmas, narrows simplification, shares the frequency-ratio estimate, and removes seven private imports while retaining useful proof structure. No actionable maintainability regression was found. The current CI build step succeeded, but linting and remaining validation are pending. Independent local compilation was blocked by HTTP 403 when fetching Mathlib.

Aspect	Value
Scope	proof elaboration and private-import refactor
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

Explicit proof dependencies and shared estimates improve maintainability without obscuring the mathematical arguments.

---

Tokens: 3,462,171 in / 10,807 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $14.0108 (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.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Static source continuation at c149b237ebd2389e2ded6e88762d2be8383933f4: the reviewed SpherePacking refactor is preserved in the normal merge with current main c1dd32a. I checked all eight complete resulting file bodies against the accepted source and current-main compatibility edits. The import resolution retains main’s SpecificFunctions.Deriv and integral Asymptotics imports while preserving the reviewed removal of Contractible. All other projects, registration, toolchain and gate inputs are literal current main. No mathematical statement was weakened. Source assessment remains approve; complete validation and configured review must now be checked on this new head, followed by the protected native queue. The old head’s CI is not credit for this revision. The previous unmergeable queue entry was removed solely to permit this branch repair.

[Vilin97]

/review