perf(SpherePacking): parallelize independent bounds and share estimates

[Vilin97]

The selected project, SpherePacking, has 55,730 source lines across eight mathematical modules and two indexes, with duplicated analytic estimates and a long serial dependency chain. It previously compiled its packing-bound module after the entire saddle/Mellin/radial chain, although its compiled declarations use no declarations from that chain. This patch makes the branches independent and combines them explicitly in Conclusion. It also shares repeated analytic estimates and simplifies the polynomial-decay integrability proof.

Measured clean project build median: 181.677488s → 155.180243s (14.58% less wall time). Only three existing SpherePacking files change; the project card, aggregate indexes, public imports, and all existing statements/definitions are preserved.

Scope and mathematical changes

• Replace PackingBound's private RadialConstruction import with the actual Mathlib dependencies. Conclusion imports RadialConstruction privately, allowing Lake to compile the packing and analytic branches concurrently. Environment inspection of every owned declaration's type and value confirms that PackingBound has no dependency on another SpherePacking module. lake shake --force --keep-public --explain LeanPool.SpherePacking.PackingBound guided the import selection; public imports were retained. CompletePartialOrder is retained because changing the order instance would change existing elaborated types/definitions.
• Add two private weighted-envelope estimate lemmas and reuse them for the plus/minus shifted-line and vertical-spectrum estimates, removing duplicated analytic arguments. Existing theorem propositions remain identical.
• Prove polynomial-decay integrability from continuous local integrability and a cocompact tail bound by (1 + t²)⁻¹, avoiding an unnecessary compact-region bound. An isolated comparison of the two proof bodies used 5,273 → 2,107 heartbeats. Gamma-argument positivity uses direct ordered-addition lemmas; two linear arithmetic calls explicitly list their needed hypotheses.

Exact semantic invariant

Measured base: f7cc971b1fb41f7c968104f3820293df1d999d66. Head: 917aa8a1c4408aaecb4a56220486c04f73cc1f6c.

Immediately before committing, the worktree HEAD was verified at the measured base, all ten saved base sources matched that commit, and the final files matched the audited source hashes. Freshly fetched main was f78a2fd57e35b09afea00517fbd384dd30124471; the selected project, pinned toolchain/dependencies, and applicable policy/review files were unchanged from the measured base.

Before editing, a Lean environment inspector imported all ten owned modules with importAll := true, including private and generated declarations. It recorded complete expression DAGs for elaborated types, universe parameters, names/module ownership, safety/partial flags, declaration kinds, reducibility, constructors/recursors and every non-theorem value. The comparison ignores expression metadata only; binder names and universe structure are compared without alpha-normalization. Theorem proof bodies alone are omitted.

Result: all 3,856 pre-existing declarations are identical; none missing or changed. Exactly two private helper theorems are added (3,858 total). A separate source audit verifies unchanged pre-existing theorem statement syntax, non-proof declarations/values, namespace commands and public-import lines. PackingBound's entire mathematical body is byte-identical to base. The all-declaration axiom audit found only propext, Quot.sound, and Classical.choice.

Controlled measurements

All runs used the unchanged repository-pinned Lean/Mathlib v4.35.0-rc3, on the same Azure VM (16 logical CPUs, AMD EPYC 9V45, 125 GiB RAM), with LEAN_NUM_THREADS=2 and the same Lake scheduling settings. Before each run, only SpherePacking outputs in .lake/build/lib/lean and .lake/build/ir were removed; pinned dependency artifacts were retained. No owned profiling/audit jobs ran during measurements. /usr/bin/time -v recorded process resource usage; a monotonic stopwatch measured the complete command. All nine baseline/final runs below passed with warnings as errors. The reported medians use the three fresh alternating base→head pairs: base-3/head-6, base-4/head-7, base-5/head-8. Initial base-1/base-2 and the first final-source head-5 are shown for transparency and excluded from these paired medians. Earlier experimental optimized sources are excluded entirely.

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

Source	Wall seconds	Maximum process RSS (KiB)
base-1	187.664468	2,150,748
base-2	197.796299	2,154,764
head-5	157.517787	2,144,496
base-3	176.584575	2,137,816
head-6	152.913596	2,135,192
base-4	181.677488	2,135,404
head-7	155.527129	2,141,820
base-5	187.271302	2,161,636
head-8	155.180243	2,138,256

In the last matched pair, module logs recorded Foundations/PackingBound at 25s/32s on base and 28s/36s on head; PackingBound overlapped the analytic chain on head. Total user CPU time was 375.96s → 377.51s, so this is a wall-time improvement through scheduling rather than a demonstrated reduction in total CPU work.

The result meets the 10% wall-time target. Most of the gain comes from removing build serialization; it depends on available CPU capacity. The VM and OS cache are shared, and this is a clean project build with warm dependency artifacts, not a cold full-pool build. GNU time's maximum RSS is the maximum for an individual process, not the sum of concurrent compiler processes; no aggregate-RAM improvement is claimed.

Validation

Passed on the final source:

lake --wfail build LeanPool.SpherePacking.Imports
lake env lean --run scripts/ci/lint-project.lean LeanPool.SpherePacking.Conclusion LeanPool.SpherePacking.Foundations LeanPool.SpherePacking.GammaAnalysis LeanPool.SpherePacking.HarmonicAnalysis LeanPool.SpherePacking.Imports LeanPool.SpherePacking.MellinAnalysis LeanPool.SpherePacking.PackingBound LeanPool.SpherePacking.RadialConstruction LeanPool.SpherePacking.SaddleAnalysis LeanPool.SpherePacking
lake exe lint-style LeanPool.SpherePacking.Imports
lake exe mk_all --module --check
(cd python && uv run python -m lean_pool.quality --repo .. --static-only)
git diff --check

The repository's project-card/declaration resolution, public axiom and environment option/injection audits were also run for all ten SpherePacking modules, followed by the stricter 3,858-declaration axiom-union audit and the complete base/head manifest comparison. Full-pool protected validation and independent refactor review remain for CI. No gates, options, waivers, toolchain files, or unrelated projects are changed. No merge or auto-merge is requested.

[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] This refactor appears safe to merge; no actionable issue was found in the changed proofs or imports.

Summary

This refactor lets PackingBound compile independently of the analytic branch and joins both branches in Conclusion.

• SpherePacking builds the packing and analytic branches independently.
• Plus and minus bounds reuse shared weighted estimates.
• Polynomial-decay integrability uses a tail bound outside a compact set.

The supplied measurements report a 14.58% reduction in project build wall time, not reduced total CPU work. Measurements and the declaration audit were not rerun. External source and license claims are unchanged and were not independently reverified.

_{Reviews (1) · Last reviewed commit: "perf(SpherePacking): parallelize bounds ..." · Reviewed by Greptile}

[Vilin97]

Source/refactor review for 917aa8a1c4408aaecb4a56220486c04f73cc1f6c: approve. Maintainability and robustness improve; risk is low; advisory quality 4/5.

I reviewed all three complete base/head diffs and the changed helper, wrapper and integrability proofs. PackingBound's mathematical body and public imports are preserved; Conclusion now imports the analytic branch directly. The two private weighted-envelope lemmas share the plus/minus estimates with their original hypotheses and bounds. The decay proof keeps the same all-moments statement and uses continuity for local integrability plus the explicit tail bound by 2 * C / (1 + t^2). I found no substantive introduced debt or obvious statement weakening.

The reported 14.58% wall-time gain is consistent with removing a serial import dependency. The author correctly separates that scheduling gain from total CPU and aggregate-memory claims. I relied on the supplied compiled-declaration preservation audit under the refactor policy and did not rerun that audit or the benchmark.

Source accepted at this head. Current-head CI, the configured refactor review, current-main qualification and normal protected native-queue validation remain the integration requirements.

[Vilin97]

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

Reviewed head: 917aa8a1c4408aaecb4a56220486c04f73cc1f6c

Verdict: ✅ approve

The refactor separates PackingBound from the analytic dependency chain and joins the branches explicitly in Conclusion. Shared envelope lemmas remove duplication while preserving the calculation steps, and the integrability proof replaces compact-region bookkeeping with local integrability and an explicit tail estimate. Arithmetic dependencies become more targeted. A targeted build was blocked by HTTP 403 while fetching pinned Mathlib, so compilation and the reported speedup were not independently verified.

Aspect	Value
Scope	dependency reorganization and shared analytic estimates
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The changes reduce module coupling and duplicated proofs without losing mathematical structure or introducing opaque automation.

---

Tokens: 918,642 in / 6,417 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $3.7708 (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.