[Vilin97]

Optimization verified locally: 36.87% faster for Zeta5Irrational, with every existing declaration preserved.

Change

The project's 214 modules contain 375,997 baseline source lines. Thousands of upper-potential certificates repeatedly normalize closed arithmetic over the reals, surrounding series checks that already run over the rationals. This pass replaces 6,326 logarithm range-reduction calculations and 6,396 geometric checks with kernel-checked rational certificates and shared transfer lemmas.

Two rational endpoint functions read the existing table1; equality lemmas connect them to the unchanged real endpoints. The analytic proofs still use the existing logarithm and arcsine-potential lemmas. All numerical bounds and existing theorem statements remain unchanged. The pass touches 59 files in this project and removes 25,749 net lines. The module headers, public imports, project card and generated aggregate retain their existing API.

Base: 595ff877b1d44314072d4baa9a6008ad4bef218d. Audited head: e0967625e99afe6824f2e41c94b7c93cf652e84c. Both use main's unchanged pinned Lean/Mathlib 4.35.0, Mathlib 56a005855ea17e0b0958f73ec801ae140b0a1679, and the same Lake options. All ten dependency checkouts are clean at their recorded revisions.

Invariant audit

Before editing, a Lean environment inspector imported the complete project at private visibility with extensions disabled. It recorded names, owning modules, kinds, fully elaborated types and binder information, universe parameters, safety, partiality, reducibility hints, non-theorem values, and inductive/constructor/recursor metadata. The comparison structurally interns expression DAGs without relying on hashes, ignoring nonsemantic expression metadata and theorem proof bodies.

All 25,865 baseline records, covering 25,862 unique declarations, remain identical: zero removals or changes. This includes the original private series certificates. The additions are seven supporting declarations (two definitions and five lemmas), their two generated equation lemmas, and 12,722 safe private kernel certificates. Every addition was classified; none is unsafe or partial. A separate source audit confirms unchanged signatures for all 15,180 original named source declarations and unchanged data-definition bodies.

Measurements

Metric	Base	Optimized
Wall time	2,742.11 s	1,731.12 s
User CPU	5,952.77 s	4,383.47 s
System CPU	440.17 s	408.62 s
Maximum child RSS	3,363,612 KiB	3,354,676 KiB

Each measurement removes only this project's generated library/IR outputs, retains identical warm dependency artifacts, and runs sequentially in isolated base/head worktrees:

/usr/bin/time -v taskset -c 12-15 lake --wfail build LeanPool.Zeta5Irrational.Imports

Both logs contain fresh successful timings for all 214 project modules and no dependency rebuilds or warnings. User CPU falls by 26.36%. Successful synchronous command-heartbeat samples fall from 4,140.080 → 1,205.197 (U_0_1), 3,970.308 → 1,227.740 (U_0_2), and 3,920.677 → 1,175.942 (U_0_3), without changing production budgets or options.

This is one controlled pair on a shared Azure VM; CPUs are not exclusive. RSS is GNU time's maximum child-process RSS, not summed simultaneous build memory. Full-repository protected CI remains required.

Validation

• Clean selected-project build with warningAsError = true; zero warnings. All 59 changed modules have fresh timings below the repository's 600-second limit (slowest: 280.0 s).
• Exact declaration manifest comparison and independent source audit.
• lake exe runLinter --no-build --only-modules=<214-module list> LeanPool.Zeta5Irrational.Imports and lake exe lint-style LeanPool.Zeta5Irrational.Imports.
• Unchanged repository quality checks on a project source view, card/declaration resolution, full compiled axiom audit and option/backdoor audit; independent traversal of private proof dependencies finds only allowed axioms.
• lake exe mk_all --module --check --repo <project-source-view> and git diff --check.
• lake shake --force --keep-public --explain LeanPool.Zeta5Irrational.Imports exits 1 with pruning suggestions and zero compiler errors. Import pruning is left out of this proof-cost pass: existing public imports are preserved, and the new explicit Linarith import records the tactic used by the shared logarithm proof even though it is currently also provided transitively.

Raw manifests, timings, profiles, source hashes and check logs are retained on the VM under /data/codex/scratch/researcher/optimization-20261115/. 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] No actionable regression was found in the shared certificate proofs or their callers.

Summary

Moves repeated arithmetic into rational certificates, then transfers the results to the existing real bounds.

• Zeta5 upper-bound proofs check repeated arithmetic in the rationals.

_{Reviews (1) · Last reviewed commit: "perf(Zeta5Irrational): share rational ce..." · Reviewed by Greptile}