[Vilin97]

Proves that Mathlib's riemannZeta 5 is an irrational real number. This imports Moritz Firsching's completed Zeta5 development, following Aabir Fauzan's September 17 preprint, together with its reusable polynomial irrationality criterion, Andréief identity, moment formulas, logarithmic-energy machinery, and prime-adic determinant bounds.

• Upstream: https://github.com/mo271/Zeta5/tree/f19a1960609f7d38e7b63fd2acb05e6f60a7b741 (Apache-2.0).
• Eligibility: the proof-completion commit 2c80b320d06b4395605edbd413649d19094507af is dated September 23, 2026, 12:22:05 UTC; release v4.34.0-rc1 followed at 20:14:14 UTC. Public announcement: https://x.com/AlexKontorovich/status/2102870642555269554 (September 23, 21:20:05 UTC). The acquisition window is September 20, 10:56:43 UTC through September 27, 10:56:43 UTC, end exclusive. The September 17 paper alone would not qualify; the completed formalization does.
• Mathematical source: A. Fauzan, ζ(5) is irrational, Theorem 1.1, https://doi.org/10.5281/zenodo.22826419.
• Provenance is mix: upstream explicitly declares manual formalization in formalization.yaml; this port includes substantial AI proof refactoring. Moritz Firsching's authorship and copyright are retained.

The dependency closure contains 208 upstream modules from the dependency closure of Apery.Main after removing unused reference normalization scaffolding, renamed to Zeta5Irrational, one new reusable upper-certificate helper, and the project entry module. It reuses MooreBound.chebyshev_asymptotic; no second PNT library, upstream challenge wrappers, numerical experiments, or CI code is imported. Registry/history and open/merged PR/issue checks found no duplicate. The existing zeta(3) project proves a different special value.

The card explicitly distinguishes the proof from the preprint's stronger numerical claim: the formalization uses cutoff 400, full rank loss, direct class-wise partial fractions, and the positive decay rate -800*(Aeff + U), rather than asserting the paper's rate 139/5. The unconditional final irrationality theorem has no extra hypotheses.

Ported to the repository's exact Lean 4.34.0 and Mathlib 5ed2965256430c3649e86755f9576b54eca72435. Changes include module/public-import boundaries, targeted imports, removal of every resource override and diagnostic command, warning repairs, and proof decomposition to satisfy existing size limits. No gate, review rule, workflow, or waiver is changed.

Measured optimization work:

Measurement	Original baseline	Final cleanup b00b44fc5
Clean full project build, warm dependencies	979.67 s wall; 11017.05 s user CPU	1538.75 s wall; 8808.14 s user CPU
Maximum resident set size	9534900 KiB	7450076 KiB

Command: lake build LeanPool.Zeta5Irrational.Main, deleting every project module trace, with warm Mathlib/MooreBound and default Lake concurrency on the shared Azure VM. The final run compiled all 209 retained implementation modules without edits during execution; the removed obsolete module's trace was also cleared. The entry module was then rebuilt. Final user CPU is about 20% lower and maximum RSS about 22% lower than baseline, but the final wall time is worse. Shared VM load and parallel scheduling limit causal interpretation of wall time. GNU time's maximum RSS is a process maximum, not summed concurrent memory.

An earlier optimized proof revision (cb12fc3e5) measured 580.80 s wall / 8219.64 s user / 7677700 KiB. That remains historical evidence and is not presented as the final revision's timing. Earlier paired Common and 16-certificate profiles improved 4.12→2.84 s and 5.29→4.14 s, respectively.

The final import cleanup was also checked with paired single-thread profiles (lake env lean -j1 --profile) using identical proof bodies and warm dependencies. Constants improved 1.66→1.13 s wall, 0.98→0.65 s user, and 1752136→920028 KiB. The first three inner-table proofs stayed comparable: 18.98→18.51 s wall, 18.27→17.90 s user, and 1969664→1711136 KiB. No further material safe proof simplification was evident from those profiles.

The optimization factors 6,396 arcsine certificates through two general lemmas without changing their statements; replaces repeated real-arithmetic expansions by exact rational certificates checked with decide +kernel; splits large interval proofs; simplifies 1,242 interval-count branches; and removes thousands of irrelevant imports. The rational certificates use kernel reduction, not native execution.

Generated tables account for approximately 94.4% of the 347,381 source lines after style wrapping (118 files). Merged companion tooling PR #541 preserves exact integer parameters and 461 shared proof templates that regenerate all 118 modules byte-for-byte. Every output hash matches this import. The tool reproduces the preserved certificates, not the original numerical search or stronger bounds. Its Python suite passes all 490 tests. The original upstream generators remain linked for search provenance; they do not reproduce this port. The imported Lean is the canonical certificate set. It uses ordinary arithmetic proofs and the project's analytic certificate interface, rather than serialized Lean terms or compiler internals. No external generator is needed to check the result.

Final review cleanup at b00b44fc50beb974417bfdff2898aeedd83cfdde removes the unused Normalization/InnerData subsystem and recurring unrelated import bundles. The unchanged vSK definition now lives in Legendre; vS_eq states its valuation formula directly, without the two redundant rfl bridges. Every generated certificate proof body is unchanged.

Final local validation:

• Complete clean project and entry builds passed with zero warnings; lake exe mk_all --module --check passes.
• All 210 project modules pass static quality/card/header/file-size/proof-size/prohibited-text checks and style checks.
• All 15 slow linters pass across 210 modules and 16,703 declarations.
• Compiled audit of 14,899 named axiom closures and every owned declaration's option/trust backdoors finds zero issues; only permitted standard axioms occur.
• Final compiled comparison retains 15,140 public/generated declarations. The 50 removed declarations all belong to unused reference normalization scaffolding. Every retained definition body has the same compiled hash. Five additional type hashes differ: the valuation formula is checked directly, and all four derivative theorems prove their exact old types including explicit instances. The previous 44 original-type compatibility proofs also pass on this final head. Endpoint and certificate type hashes match.
• Companion tools: preserve reproducible Zeta5 certificate generation #541 at 37c58c2b1 reproduces all 118 files byte-for-byte at this commit; Ruff and all 490 Python tests pass. The content PR changes no Python.

Upstream build and Comparator passed at the pinned revision. The upstream statement also matches the attributed Formal Conjectures benchmark; this import contains the completed proof closure, not its open challenge wrapper. The primary PDF's Theorem 1.1 and stronger numerical claim were checked directly; its separate bound on the irrationality exponent is not claimed here.

Current CI 36331168268 passes every required check on main-integrated head c0b7f368f245292c8165fd86508ca73dc99e5b1d. Greptile reviewed 212 files with zero comments. GPT approved all five rubrics at f0a9f24e9; the complete PR diff is byte-identical after main integration. The separate thorough review approves the current head, all threads are resolved, and GitHub reports CLEAN. No gate or protection bypass is used.

Citation follow-up: preserved the parallel reviewer’s 715bb2622 corrections and added explicit (6.9)/(6.14) constants in f0a9f24e94702d0639775ed313b88c0ad4b8863d. The final five files differ from measured b00b44fc5 only in comments; the full compiled declaration inventory is identical. The warning-free rebuild, all 15 slow linters, static/style/index checks and full compiled trust audit pass again. All 118 archived generated files are unchanged. Content CI 36327012420 passed before main integration, and current CI 36331168268 also passes. Tooling CI 36326982656 passed before #541 merged as 91d0ec39f. The complete before/after PR diff has SHA-256 d6b32870e5b1d8eae7512723f9b8f5194bc6102ffe3539f5df13d1d7bc54d051. The automatic current-commit GPT refresh remains queued; the completed approval covers this identical content diff.

[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 risk] Adds a mathematical formalization library for zeta function irrationality.

No outstanding finding from this review prevents merging this PR.

Summary

This PR adds a completed Lean formalization of the irrationality of riemannZeta 5.

• Registers and imports the project, including its polynomial irrationality criterion, analytic and arithmetic estimates, and numerical certificates.
• The stated headline matches the unconditional irrational_five theorem. The project card distinguishes the formalized decay estimate from the stronger constant in the cited paper.

_{Reviews (7) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[Vilin97]

/review

The current head is 73fe1f4. Local project build, style, all slow linters, complete axiom/option audits, and original-type compatibility checks pass; full repository CI is still running and remains required before merge. Please review the complete source in bounded portions. The tested certificate-regeneration companion is #541; the unused reference-only normalizer identified by Greptile has been removed. The PR body records the quantitative deviation from the paper and the measured 979.67 s → 580.80 s clean-build improvement.

[Vilin97]

{
"review": "Thorough acquisition-agent source review, conducted separately from the configured Greptile and GPT reviews. This is the importing agent's review, not an independent human approval.",
"commit": "c0b7f368f245292c8165fd86508ca73dc99e5b1d",
"conclusion": "approve",
"coverage": "Complete pinned upstream closure and final imported source were inspected in bounded packets. All 209 retained implementation modules (95 non-UV and 114 UV), the entry module, generated root and registry are covered. The removed Normalization module was also reviewed. Every certificate template/file was inventoried; complete compiled declaration/type/axiom audits supplement representative implementation slices. The final diff changes imports, deletes unused reference scaffolding and moves the unchanged valuation definition; every generated proof body is identical.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The headline is unconditional irrationality of Mathlib riemannZeta at five, and the two supporting card claims match their quantifiers and bounds.",
"proves_the_claim": "proves_it",
"claim_note": "irrational_five constructs an irrational real x with riemannZeta 5 = (x : Complex); main_estimate supplies a positive decay constant for all sufficiently large n, and the generic criterion quantifies over every positive natural denominator. The bridge from the real reciprocal-power series to Mathlib riemannZeta is proved. The final theorem has no context carrying the desired conclusion. The main estimate constructs degree-37n integer polynomials with positive exponentially small values and supplies the positive rate used by the criterion.",
"assumed_inputs": "The headline has no hypotheses. The generic criterion explicitly assumes eventual integer polynomial approximants and denominator-weighted decay, exactly as its informal statement says. The prime number theorem is reused as an already proved MooreBound theorem, not assumed in a structure field.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate headline was found in the checked Mathlib revision, pool, registry, history, PRs, or issues.",
"already_formalized": "",
"novelty_note": "The closest pooled result is Zeta3Irrational.zeta3_irrational, whose conclusion concerns riemannZeta 3; it does not establish the value at five.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "The unconditional individual zeta(5) irrationality result, with substantial reusable analytic and arithmetic infrastructure, is a strong fit for the pool. This significance judgment concerns the formal theorem and its proof closure, not announcement prestige.",
"fit": "good_fit",
"level": "research",
"branch": "analytic number theory",
"mode": "mixed",
"significance_one_sentence": "The development proves irrationality of the individual zeta value at five and supplies reusable polynomial, determinant, valuation, moment, and logarithmic-energy arguments.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "Checked the primary Zenodo PDF, pinned upstream source/license and authorship metadata. The final comments explicitly label the quantitative variants of (6.7), (6.9), (6.12), (6.14) and Proposition 6.3, including changed constants and applicable domains. The card discloses the weaker positive decay rate; the separate irrationality-exponent bound 260 is not claimed.",
"source_match": "matches",
"findings": [],
"source_url": "https://zenodo.org/records/22826419"
},
"quality": {
"verdict": "pass",
"bottom_line": "The unused Normalization/InnerData reference subsystem and recurring unrelated import bundles have been removed. The used vSK definition and valuation formula remain intact. All local quality, trust and slow-linter checks pass. The exact certificate archive is reproduced by separately tested PR #541.",
"code_quality": 4,
"findings": []
},
"engineering_notes": [
"Apache-2.0 verified at upstream f19a1960609f7d38e7b63fd2acb05e6f60a7b741; original authorship/copyright retained. Upstream metadata declares manual authorship; mix accurately records substantial AI proof refactoring in this port.",
"208 upstream dependency modules remain after removing unused reference normalization scaffolding. One reusable certificate helper and one entry are added. Existing MooreBound PNT is reused; no second PNT library, challenge wrapper, numerical experiment or CI code is vendored.",
"Card fidelity: cutoff 400, full rank loss, direct class-wise partial fractions, and positive c=-800(Aeff+U), rather than the preprint rate 139/5. The irrationality-exponent bound 260 is not claimed. The final irrationality statement has no extra hypothesis.",
"347,381 implementation lines, 327,764 generated (about 94.4%). Companion #541 preserves exact integer parameters, 461 templates, 118 outputs and hashes; this regenerates preserved certificates, not a search for stronger bounds. New bounds require mathematical and kernel validation.",
"Clean baseline: 979.67 s wall, 11,017.05 s user, 9,534,900 KiB maximum RSS. Earlier optimization cb12: 580.80 s wall, 8,219.64 s user, 7,677,700 KiB. Final b00 cleanup: 1,538.75 s wall, 8,808.14 s user, 7,450,076 KiB. Same warm dependencies, default Lake concurrency and deleted project traces on a shared VM. Final user CPU is 20% lower and maximum RSS 22% lower than baseline, but wall time is worse. Historical wall improvement is not presented as the final result; maximum RSS is not summed concurrent memory.",
"Paired single-thread final import profiles with identical bodies: Constants 1.66 to 1.13 s wall, 0.98 to 0.65 s user, 1,752,136 to 920,028 KiB; first three inner-table proofs 18.98 to 18.51 s wall, 18.27 to 17.90 s user, 1,969,664 to 1,711,136 KiB. Previous Common/certificate pairs also improved. No material safe proof simplification was evident from these profiles beyond the completed refactors; expensive exact certificate arithmetic remains explicit.",
"Optimizations factor 6,396 certificate statements through two general helpers, simplify 1,242 count branches, replace repeated real expansions by exact rational kernel certificates, split long proofs, remove resource overrides/diagnostics and narrow imports. No gate, waiver, theorem strength or useful generality was changed.",
"Final API comparison: 15,140 retained public/generated declarations; 50 unused reference-module declarations intentionally removed; all retained definition bodies match prior compiled hashes. Exactly five additional theorem-type hashes differ: valuation formula checked directly; four derivatives independently prove the exact old types including explicit instances. The earlier 44 original-type compatibility proofs also pass on the final head. Endpoint and certificate types match."
],
"validation": {
"local": "Final f0 citation revision rebuilt warning-free. All 210 modules pass style/static quality/index checks and all 15 slow linters (16,703 declarations). Its fresh compiled audit again checks 14,899 named axiom closures and every owned declaration’s option/trust backdoors: zero findings. Full 15,140-declaration inventory is identical to measured b00. The 44 prior type checks, valuation formula and four exact old derivative types including explicit instances passed. Changes after the controlled measurement are comments only. The c0 main integration was independently checked to leave all Lean/toolchain files byte-identical to f0, and its local index/build/reproduction checks passed.",
"ci": "Current CI 36331168268 passed at c0b7f36: project and challenge/solution builds, generated indexes, linters, style, and repository quality/trust gates. The required Build project, Documentation preflight and Content / non-content separation checks all pass. GitHub reports CLEAN against current main 91d0ec3; strict protection is enabled, both review threads are resolved, and no required human approval is configured. Earlier full CI 36327012420 also passed the identical source at f0.",
"configured_reviews": "Greptile reviewed current c0: 212 files, zero comments, success. GPT approved f0 at 15:26:24 UTC with all five rubrics passing (job 1068). The entire binary PR diff before and after main integration is byte-identical: 17,307,734 bytes, SHA-256 d6b32870e5b1d8eae7512723f9b8f5194bc6102ffe3539f5df13d1d7bc54d051. That completed approval covers the exact current content. Automatic current-commit refresh 1078 was queued at merge; no separate c0 verdict is claimed. Tooling GPT approved 37c58; merged ce9 retained identical renderer/archive/tests plus a README guide link.",
"merge_condition": "Satisfied for a normal protected squash merge of exact head c0b7f36. Significance, correctness, licensing, provenance, trust and maintainability have no unresolved material finding. No administrator bypass, protection change, gate change, suppression or waiver is used."
},
"action": "approve",
"resolved_findings": [
{
"kind": "unused-scaffolding",
"resolution": "Removed the entire unused InnerData subsystem and ellA, plus the earlier mKM/mKM_pos. Moved unchanged vSK to Legendre; vS_eq uses it directly; removed two redundant rfl bridges. All 50 removed public/generated declarations belonged to the unused reference module. The main proof and useful mN API remain intact."
},
{
"kind": "irrelevant-imports",
"resolution": "Removed 536 broad import edges and supplied 669 explicit mathematical/tactic providers where necessary. Gamma, Chebyshev and primality plugins remain at actual consumers. Complete clean build is warning-free; paired profiles show reduced constants-module time/RSS and comparable inner-table proof cost."
},
{
"kind": "certificate-regeneration",
"resolution": "Tool PR #541 at 37c58c2 pins b00b44f and regenerates all 118 modules byte-for-byte. All 461 shared templates and exact integer records were verified; every proof body is unchanged. Its 490 tests, Ruff, Greptile and GPT pass. Current required Lean CI is still running."
},
{
"kind": "unlabelled-variant",
"resolution": "Preserved the parallel daily-review job’s 715bb26 fixes for (6.7), (6.12) and Proposition 6.3, and added the remaining (6.9)/(6.14) constants and consistent module summaries in f0a9f24. Checked the paper’s pages 19–20 directly. Every comment-stripped code token and the full compiled declaration inventory are identical to the measured b00 revision."
}
],
"protection_resolution": "The earlier needs-maintainer disposition requested either enabling auto-merge or arranging serialized current-main integration and normal protected merging. The autonomous acquisition task already authorizes the latter. Main integration is complete and all current required checks pass, so that disposition is resolved and its stale label can be removed. Repository auto-merge settings remain unchanged.",
"result": {
"state": "merged",
"merge_commit": "2369278b36ee14d71e74ee4a6f874ac53d5474e9",
"merged_at": "2026-09-27T17:10:16Z",
"method": "normal protected squash; no bypass",
"metadata_commit": "504c1718290248c7eba3e05b3e71624fa7cee7fc",
"post_merge_validation": "Generated metadata workflow passed. Fresh merged checkout passes all 490 Python tests, Ruff check/format and all118 certificate byte comparisons. The prior optional NOTICE freshness failure is resolved. All Lean/toolchain files remain byte-identical to the approved and CI-passing c0 head."
}
}

[Vilin97]

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: f0a9f24e94702d0639775ed313b88c0ad4b8863d

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All three headline results match the card, including unconditional irrationality of Mathlib’s riemannZeta 5.
Novelty	✅ pass	Searches of pinned Mathlib and existing pool sources found no duplicate of the ζ(5) irrationality theorem or its determinant-polynomial estimate.
Significance	✅ pass	Worth pooling: substantial research mathematics with maintainable certificates; generated tables occupy 327,764 of 347,381 implementation lines (94.4%), use ordinary arithmetic tactics and project analytic lemmas, and all 118 modules reproduce byte-for-byte using the archived tooling in companion #541.
Sources	✅ pass	Fauzan’s Theorem 1.1 supports the irrationality claim, numerical variants are explicitly labelled, and Firsching’s prior formalization is credited.
Code quality (advisory)	✅ pass	The development is competently modularized around reusable valuation, energy, and certificate lemmas; no material code-quality issue warrants maintainer discussion.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The irrationality theorem and main estimate have no extra hypotheses. The reusable criterion assumes eventual positive polynomial evaluations and decay for every positive natural denominator, exactly as disclosed in the card.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	analytic number theory
Mode	mixed
Code quality	3 / 5

Statement check: The Lean proves that riemannZeta 5 equals the complex coercion of an irrational real, and establishes the stated eventual degree-37n polynomial estimate with a positive decay constant.

The project establishes irrationality of ζ(5), supported by substantial developments in polynomial approximation, Hankel determinants, logarithmic energy, and prime-adic bounds.

---

Tokens: 5,366,532 in / 36,288 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $110.0522 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/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]

/review

Please refresh the completed review of 73fe1f4 to current head b00b44f. Both concrete quality findings are repaired:

• Removed the unused Normalization/InnerData reference subsystem. Moved the identical vSK definition to Legendre and restated vS_eq directly using it; the two redundant rfl bridges are gone. The valuation formula and all headline hypotheses/conclusions are unchanged.
• Audited the recurring Gamma, Multinomial, Chebyshev, prime and square-root plugin imports throughout the project. Removed unused occurrences and supplied precise calculus/integral/tactic providers where needed. Prime arithmetic remains only where literal primality cases require it; Gamma and Chebyshev remain at actual consumers.

The complete project rebuilt with zero warnings, generated indexes pass, all 210 source modules pass style/static quality. The fresh clean measurement, full slow-linter pass, and compiled trust audit are running; final CI remains mandatory. All table proof bodies are unchanged. Companion #541 is being refreshed to reproduce the final header changes byte-for-byte, retaining its tested renderer and exact certificate data. No policy or waiver changed.

[Vilin97]

/review

Please review exact head 715bb2622521c10b1ee25ea934c2d2496c3164aa after the validated proof-sharing/API cleanup. Full targeted project build, linters, style and trust/quality checks passed; controlled before/after module profiles were collected. Prior valid repairs were preserved.

[Vilin97]

/review

The current head adds only citation clarifications to the previously measured and audited proof. The parallel daily-review job's valid 715bb26 commit is preserved. I checked the primary PDF's Section 6 and added the remaining variant labels for (6.9) and (6.14): 5h + 6h log K versus (120 + sqrt(2))h + 2h log K, and 22h log K + 50h versus 18h log K + 160h. The earlier patch already identifies the reported (6.7), (6.12) and Proposition 6.3 changes. Their module summaries and wrapper citations now agree.

All five affected files have identical comment-stripped code to b00b44f. Full incremental project build is warning-free; all-module style, changed-module slow linters, static checks and indexes pass. The final clean measurement and paired profiles are recorded in the PR body, including the worse final wall time; no uniform wall-time improvement is claimed. Full compiled audits are being refreshed and current CI remains required. The 118 generated certificate files are unchanged, so companion #541 still reproduces them exactly.

[Vilin97]

Disposition: needs-maintainer — protected merge operation.

Reviewed exact head f0a9f24e94702d0639775ed313b88c0ad4b8863d.

The unconditional ζ(5) irrationality theorem is complete and significant. All changed files, endpoint/dependency closure and bounded certificate slices were audited. The generator reproduced all 118 generated modules; trust/declaration checks passed. The source-variant constants are now explicitly disclosed, including the comment-only follow-up at this head. The stronger paper decay-rate/irrationality-exponent constants are not claimed.

Repair validated: Labeled the different sum/integral, regularization and real-bound constants as source variants; the subsequent author follow-up extends those annotations, with executable Lean unchanged. The targeted build, declaration/style linters, and source-scoped trust/quality audit passed. Module profiles are recorded; shared-host timing is not treated as a deterministic performance guarantee.

Protected-check snapshot: Build project: not reported; Content / non-content separation: SUCCESS; Documentation preflight: SUCCESS; GitHub merge state BLOCKED. GitHub rejected protected auto-merge with Auto merge is not allowed for this repository. No auto-merge is registered.

Exact maintainer decision: Authorize repository protected auto-merge, or arrange serialized current-main integration and normal protected merging. There is no remaining material mathematical/code blocker supporting requested changes or closure; current protection prevents immediate merge and automation cannot change repository settings under this task. Remove this label before merging.

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 3345.93 s (= 55.77 min) — user 12903.70 s, sys 199.07 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 62,978 maxHeartbeats units across 211 files (347,379 added LOC).

Sum of lean --profile: 9382695.9 ms (= 9382.70 s). Import-excluded time: 9105935.9 ms (= 9105.94 s).

Count-heartbeats wall-clock total: 9438.33 s. Repeated import cost inside lean --profile: 276760.0 ms (= 276.76 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Decls	Errors
LeanPool/Zeta5Irrational/Table/Intervals.lean	10,382	5,472	247.47	250.71	249.40	1.31	1368	0
LeanPool/Zeta5Irrational/Growth/InnerSum.lean	2,235	1,040	177.18	178.09	176.77	1.32	260	0
LeanPool/Zeta5Irrational/Arith/OuterEntryMain.lean	586	848	9.21	11.42	10.13	1.29	30	0
LeanPool/Zeta5Irrational/Table/U00.lean	4,604	816	111.74	99.57	98.28	1.29	204	0
LeanPool/Zeta5Irrational/Table/U01.lean	2,903	816	60.45	59.40	58.12	1.28	204	0
LeanPool/Zeta5Irrational/Table/U02.lean	2,259	816	38.29	43.26	41.96	1.30	204	0
LeanPool/Zeta5Irrational/Table/U03.lean	2,393	816	48.07	46.66	45.39	1.27	204	0
LeanPool/Zeta5Irrational/Table/U04.lean	2,547	816	47.56	50.22	48.93	1.29	204	0
LeanPool/Zeta5Irrational/Table/U05.lean	2,631	816	52.19	52.99	51.70	1.29	204	0
LeanPool/Zeta5Irrational/Table/U06.lean	2,788	816	55.37	55.65	54.39	1.26	204	0
LeanPool/Zeta5Irrational/Table/U07.lean	2,848	816	55.53	57.12	55.84	1.28	204	0
LeanPool/Zeta5Irrational/Table/U08.lean	2,934	816	58.96	60.38	59.10	1.28	204	0
LeanPool/Zeta5Irrational/Table/U09.lean	3,066	816	60.83	62.33	61.04	1.29	204	0
LeanPool/Zeta5Irrational/Table/U10.lean	3,066	816	60.81	61.82	60.54	1.28	204	0
LeanPool/Zeta5Irrational/Table/U11.lean	3,096	816	65.28	63.54	62.26	1.28	204	0
LeanPool/Zeta5Irrational/Table/U12.lean	3,281	816	67.67	68.60	67.30	1.30	204	0
LeanPool/Zeta5Irrational/Table/U13.lean	3,288	816	69.24	69.53	68.26	1.27	204	0
LeanPool/Zeta5Irrational/Table/U14.lean	3,284	816	70.99	69.94	68.66	1.28	204	0
LeanPool/Zeta5Irrational/Table/U15.lean	3,351	816	72.24	70.78	69.48	1.30	204	0
LeanPool/Zeta5Irrational/Table/U16.lean	3,501	816	69.89	73.20	71.93	1.27	204	0
LeanPool/Zeta5Irrational/Table/U17.lean	3,504	816	67.93	72.29	70.99	1.30	204	0
LeanPool/Zeta5Irrational/Table/U18.lean	3,496	816	74.67	72.29	71.02	1.27	204	0
LeanPool/Zeta5Irrational/Table/U19.lean	3,536	816	73.83	74.91	73.62	1.29	204	0
LeanPool/Zeta5Irrational/Table/U20.lean	3,708	816	80.29	79.25	77.98	1.27	204	0
LeanPool/Zeta5Irrational/Table/U21.lean	3,714	816	78.69	78.51	77.23	1.28	204	0
LeanPool/Zeta5Irrational/Table/U22.lean	3,711	816	83.40	79.94	78.67	1.27	204	0
LeanPool/Zeta5Irrational/Table/U23.lean	3,707	816	84.05	81.02	79.76	1.26	204	0
LeanPool/Zeta5Irrational/Table/U24.lean	3,874	816	82.60	81.80	80.52	1.28	204	0
LeanPool/Zeta5Irrational/Table/U25.lean	3,935	816	82.20	82.82	81.54	1.28	204	0
LeanPool/Zeta5Irrational/Table/U26.lean	3,927	816	80.75	82.74	81.46	1.28	204	0
LeanPool/Zeta5Irrational/Table/U27.lean	3,933	816	78.50	82.52	81.25	1.27	204	0
LeanPool/Zeta5Irrational/Table/U28.lean	3,960	816	81.91	84.23	82.97	1.26	204	0
LeanPool/Zeta5Irrational/Table/U29.lean	4,156	816	85.19	88.24	86.96	1.28	204	0
LeanPool/Zeta5Irrational/Table/U30.lean	4,160	816	87.11	88.41	87.13	1.28	204	0
LeanPool/Zeta5Irrational/Table/U31.lean	4,159	816	87.31	89.37	88.08	1.29	204	0
LeanPool/Zeta5Irrational/Table/U32.lean	4,150	816	82.70	91.90	90.62	1.28	204	0
LeanPool/Zeta5Irrational/Table/U33.lean	4,213	816	74.67	93.69	92.41	1.28	204	0
LeanPool/Zeta5Irrational/Table/U34.lean	4,364	816	86.83	100.63	99.32	1.31	204	0
LeanPool/Zeta5Irrational/Table/U35.lean	4,371	816	85.59	99.56	98.20	1.36	204	0
LeanPool/Zeta5Irrational/Table/U36.lean	4,364	816	80.72	99.81	98.53	1.28	204	0
LeanPool/Zeta5Irrational/Table/U37.lean	4,361	816	84.98	101.29	99.99	1.30	204	0
LeanPool/Zeta5Irrational/Table/U38.lean	4,467	816	87.22	101.39	100.09	1.30	204	0
LeanPool/Zeta5Irrational/Table/U39.lean	4,617	816	85.30	103.31	102.00	1.31	204	0
LeanPool/Zeta5Irrational/Table/U40.lean	4,624	816	84.98	102.80	101.49	1.31	204	0
LeanPool/Zeta5Irrational/Table/U41.lean	4,612	816	83.43	102.37	101.09	1.28	204	0
LeanPool/Zeta5Irrational/Table/U42.lean	4,611	816	85.13	101.58	100.28	1.30	204	0
LeanPool/Zeta5Irrational/Table/U43.lean	4,762	816	88.33	103.64	102.34	1.30	204	0
LeanPool/Zeta5Irrational/Table/U44.lean	4,829	816	91.47	107.50	106.19	1.31	204	0
LeanPool/Zeta5Irrational/Table/U45.lean	4,829	816	92.31	105.90	104.57	1.33	204	0
LeanPool/Zeta5Irrational/Table/U46.lean	4,831	816	94.20	111.06	109.74	1.32	204	0
LeanPool/Zeta5Irrational/Table/U47.lean	5,003	816	94.30	112.29	110.98	1.31	204	0
LeanPool/Zeta5Irrational/Table/U48.lean	5,063	816	99.92	113.46	112.17	1.29	204	0
LeanPool/Zeta5Irrational/Table/U49.lean	5,051	816	98.53	112.54	111.23	1.31	204	0
LeanPool/Zeta5Irrational/Table/U50.lean	5,058	816	94.24	112.13	110.81	1.32	204	0
LeanPool/Zeta5Irrational/Table/U51.lean	5,291	816	107.12	119.26	117.93	1.33	204	0
LeanPool/Zeta5Irrational/Table/U52.lean	5,284	816	104.04	117.87	116.56	1.31	204	0
LeanPool/Zeta5Irrational/Table/U53.lean	5,463	816	105.79	120.68	119.33	1.35	204	0
LeanPool/Zeta5Irrational/Table/U54.lean	5,593	816	100.34	125.61	124.31	1.30	204	0
LeanPool/Zeta5Irrational/Table/U55.lean	5,559	816	100.27	127.10	125.78	1.32	204	0
LeanPool/Zeta5Irrational/Table/U56.lean	3,379	612	73.41	81.40	80.08	1.32	153	0
LeanPool/Zeta5Irrational/Growth/InnerTable.lean	8,268	500	1808.23	1459.94	1458.65	1.29	125	0
LeanPool/Zeta5Irrational/Growth/InnerPrime.lean	323	450	20.28	17.59	16.26	1.33	6	0
LeanPool/Zeta5Irrational/Arith/OuterBasis.lean	180	420	5.41	3.62	2.29	1.33	16	0
LeanPool/Zeta5Irrational/Arith/OuterEntries.lean	321	355	6.59	7.60	6.25	1.35	13	0
LeanPool/Zeta5Irrational/Table/Common.lean	555	260	14.71	11.46	10.17	1.29	65	0
LeanPool/Zeta5Irrational/Potential.lean	526	180	17.75	18.38	16.95	1.43	45	0
LeanPool/Zeta5Irrational/HermiteIBP.lean	462	164	16.02	19.02	17.74	1.28	41	0
LeanPool/Zeta5Irrational/Arith/InnerAlloc.lean	352	162	7.41	9.04	7.74	1.30	21	0
LeanPool/Zeta5Irrational/Arith/Val.lean	227	155	3.49	2.77	1.55	1.22	31	0
LeanPool/Zeta5Irrational/Growth/TailIntegral.lean	375	140	13.86	14.63	13.38	1.25	35	0
LeanPool/Zeta5Irrational/Hermite.lean	514	132	19.88	14.46	13.10	1.36	33	0
LeanPool/Zeta5Irrational/Norm.lean	333	128	12.98	6.36	5.11	1.25	26	0
LeanPool/Zeta5Irrational/Normalization.lean	172	128	6.51	1.93	0.68	1.25	32	0
LeanPool/Zeta5Irrational/Arith/ClassCount.lean	260	121	5.70	4.24	2.94	1.30	18	0
LeanPool/Zeta5Irrational/Arith/SmallPrimeF.lean	321	120	7.66	6.53	5.26	1.27	20	0
LeanPool/Zeta5Irrational/TableCheck.lean	335	112	8.28	5.65	4.35	1.30	28	0
LeanPool/Zeta5Irrational/Arith/Pullback.lean	277	104	5.96	6.56	5.26	1.30	26	0
LeanPool/Zeta5Irrational/Arith/DirectBound.lean	199	99	4.81	3.32	2.02	1.30	16	0
LeanPool/Zeta5Irrational/ZeroMass.lean	394	94	29.82	28.02	26.75	1.27	20	0
LeanPool/Zeta5Irrational/Arith/BinomBasis.lean	255	92	5.28	4.25	2.90	1.35	23	0
LeanPool/Zeta5Irrational/EnergyAtoms.lean	309	92	7.50	10.46	9.16	1.30	23	0
LeanPool/Zeta5Irrational/HermiteIntegrals.lean	411	92	22.72	19.47	18.24	1.23	23	0
LeanPool/Zeta5Irrational/Degree.lean	210	88	4.35	4.29	3.00	1.29	22	0
LeanPool/Zeta5Irrational/EnergyConst.lean	350	84	26.73	22.01	20.69	1.32	21	0
LeanPool/Zeta5Irrational/Growth/OuterTable.lean	976	80	249.29	295.56	294.22	1.34	20	0
LeanPool/Zeta5Irrational/Arith/PoleVal.lean	271	78	7.71	6.26	4.97	1.29	13	0
LeanPool/Zeta5Irrational/Growth/ClassSum.lean	223	72	6.84	6.15	4.86	1.29	18	0
LeanPool/Zeta5Irrational/Growth/TailPrime.lean	572	72	61.74	39.70	38.41	1.29	18	0
LeanPool/Zeta5Irrational/Arith/TauBound.lean	152	60	4.20	3.15	1.87	1.28	9	0
LeanPool/Zeta5Irrational/Growth/TableGen.lean	147	57	68.83	49.18	47.91	1.27	8	0
LeanPool/Zeta5Irrational/ArcsinePotential.lean	240	56	6.71	6.81	5.49	1.32	14	0
LeanPool/Zeta5Irrational/Arith/DirectPoly.lean	328	54	8.04	5.91	4.61	1.30	9	0
LeanPool/Zeta5Irrational/Growth/ClassData.lean	170	54	6.49	5.55	4.24	1.31	9	0
LeanPool/Zeta5Irrational/Arith/ClassFrame.lean	197	52	6.30	4.36	3.02	1.34	13	0
LeanPool/Zeta5Irrational/Growth/Assembly4.lean	127	52	11.25	7.88	6.54	1.34	13	0
LeanPool/Zeta5Irrational/Kernel.lean	250	52	12.39	6.61	5.38	1.23	13	0
LeanPool/Zeta5Irrational/Arith/IntPoly.lean	93	51	2.80	2.15	0.89	1.26	6	0
LeanPool/Zeta5Irrational/Arith/InnerWeights.lean	218	50	6.36	3.86	2.58	1.28	10	0
LeanPool/Zeta5Irrational/Growth/OuterPrime.lean	326	49	22.62	11.40	10.12	1.28	8	0
LeanPool/Zeta5Irrational/Andreief.lean	150	48	4.89	3.06	1.75	1.31	6	0
LeanPool/Zeta5Irrational/Arith/SmallPrimeRes.lean	215	48	4.74	3.55	2.27	1.28	8	0
LeanPool/Zeta5Irrational/EnergyBlocks.lean	238	48	6.58	5.18	3.73	1.45	12	0
LeanPool/Zeta5Irrational/Table/V00.lean	1,379	48	22.57	31.78	30.45	1.33	12	0
LeanPool/Zeta5Irrational/Table/V01.lean	1,410	48	23.63	32.58	31.27	1.31	12	0
LeanPool/Zeta5Irrational/Table/V02.lean	1,509	48	24.12	32.30	30.98	1.32	12	0
LeanPool/Zeta5Irrational/Table/V03.lean	1,395	48	21.41	27.88	26.55	1.33	12	0
LeanPool/Zeta5Irrational/Table/V04.lean	1,294	48	24.62	26.74	25.42	1.32	12	0
LeanPool/Zeta5Irrational/Table/V05.lean	1,223	48	23.23	24.27	22.93	1.34	12	0
LeanPool/Zeta5Irrational/Table/V06.lean	1,225	48	23.52	25.54	24.25	1.29	12	0
LeanPool/Zeta5Irrational/Table/V07.lean	1,229	48	23.28	25.50	24.22	1.28	12	0
LeanPool/Zeta5Irrational/Table/V08.lean	1,228	48	23.64	25.46	24.19	1.27	12	0
LeanPool/Zeta5Irrational/Table/V09.lean	1,234	48	22.31	24.74	23.46	1.28	12	0
LeanPool/Zeta5Irrational/Table/V10.lean	1,239	48	23.64	25.05	23.78	1.27	12	0
LeanPool/Zeta5Irrational/Table/V11.lean	1,232	48	23.94	25.18	23.90	1.28	12	0
LeanPool/Zeta5Irrational/Table/V12.lean	1,227	48	22.01	25.85	24.57	1.28	12	0
LeanPool/Zeta5Irrational/Table/V13.lean	1,239	48	25.36	26.22	24.94	1.28	12	0
LeanPool/Zeta5Irrational/Table/V14.lean	1,230	48	28.36	26.00	24.73	1.27	12	0
LeanPool/Zeta5Irrational/Table/V15.lean	1,229	48	25.61	24.83	23.56	1.27	12	0
LeanPool/Zeta5Irrational/Table/V16.lean	1,243	48	22.53	25.29	24.02	1.27	12	0
LeanPool/Zeta5Irrational/Table/V17.lean	1,249	48	25.21	25.42	24.15	1.27	12	0
LeanPool/Zeta5Irrational/Table/V18.lean	1,251	48	24.67	26.07	24.65	1.42	12	0
LeanPool/Zeta5Irrational/Table/V19.lean	1,244	48	23.71	26.13	24.85	1.28	12	0
LeanPool/Zeta5Irrational/Table/V20.lean	1,234	48	25.06	27.07	25.77	1.30	12	0
LeanPool/Zeta5Irrational/Table/V21.lean	1,240	48	25.72	27.17	25.86	1.31	12	0
LeanPool/Zeta5Irrational/Table/V22.lean	1,244	48	22.70	27.47	26.18	1.29	12	0
LeanPool/Zeta5Irrational/Table/V23.lean	1,233	48	25.31	28.03	26.71	1.32	12	0
LeanPool/Zeta5Irrational/Table/V24.lean	1,397	48	24.52	27.55	26.26	1.29	12	0
LeanPool/Zeta5Irrational/Table/V25.lean	1,438	48	24.35	27.80	26.49	1.31	12	0
LeanPool/Zeta5Irrational/Table/V26.lean	1,449	48	26.73	28.31	26.97	1.34	12	0
LeanPool/Zeta5Irrational/Table/V27.lean	1,447	48	24.93	27.37	26.01	1.36	12	0
LeanPool/Zeta5Irrational/Table/V28.lean	1,427	48	23.83	27.88	26.53	1.35	12	0
LeanPool/Zeta5Irrational/Table/V29.lean	1,435	48	26.99	27.84	26.53	1.31	12	0
LeanPool/Zeta5Irrational/Table/V30.lean	1,443	48	26.43	27.92	26.62	1.30	12	0
LeanPool/Zeta5Irrational/Table/V31.lean	1,446	48	26.21	28.55	27.22	1.33	12	0
LeanPool/Zeta5Irrational/Table/V32.lean	1,443	48	25.87	29.17	27.83	1.34	12	0
LeanPool/Zeta5Irrational/Table/V33.lean	1,431	48	25.83	28.88	27.57	1.31	12	0
LeanPool/Zeta5Irrational/Table/V34.lean	1,415	48	27.57	29.14	27.82	1.32	12	0
LeanPool/Zeta5Irrational/Table/V35.lean	1,420	48	25.24	29.56	28.21	1.35	12	0
LeanPool/Zeta5Irrational/Table/V36.lean	1,424	48	28.19	29.32	28.02	1.30	12	0
LeanPool/Zeta5Irrational/Table/V37.lean	1,421	48	29.14	29.42	28.12	1.30	12	0
LeanPool/Zeta5Irrational/Table/V38.lean	1,418	48	26.63	28.08	26.75	1.33	12	0
LeanPool/Zeta5Irrational/Table/V39.lean	1,452	48	26.39	30.11	28.81	1.30	12	0
LeanPool/Zeta5Irrational/Table/V40.lean	1,451	48	26.11	28.41	27.03	1.38	12	0
LeanPool/Zeta5Irrational/Table/V41.lean	1,444	48	24.49	28.12	26.81	1.31	12	0
LeanPool/Zeta5Irrational/Table/V42.lean	1,439	48	26.30	28.48	27.16	1.32	12	0
LeanPool/Zeta5Irrational/Table/V43.lean	1,439	48	28.80	29.12	27.78	1.34	12	0
LeanPool/Zeta5Irrational/Table/V44.lean	1,445	48	27.05	28.41	27.08	1.33	12	0
LeanPool/Zeta5Irrational/Table/V45.lean	1,442	48	25.42	28.49	27.17	1.32	12	0
LeanPool/Zeta5Irrational/Table/V46.lean	1,440	48	25.03	28.93	27.60	1.33	12	0
LeanPool/Zeta5Irrational/Table/V47.lean	1,433	48	29.93	29.10	27.78	1.32	12	0
LeanPool/Zeta5Irrational/Table/V48.lean	1,441	48	27.28	29.27	27.95	1.32	12	0
LeanPool/Zeta5Irrational/Table/V49.lean	1,441	48	27.66	29.44	28.12	1.32	12	0
LeanPool/Zeta5Irrational/Table/V50.lean	1,444	48	26.98	29.42	28.11	1.31	12	0
LeanPool/Zeta5Irrational/Table/V51.lean	1,434	48	28.77	29.43	28.09	1.34	12	0
LeanPool/Zeta5Irrational/Table/V52.lean	1,442	48	26.64	30.20	28.89	1.31	12	0
LeanPool/Zeta5Irrational/Table/V53.lean	1,452	48	28.36	29.74	28.41	1.33	12	0
LeanPool/Zeta5Irrational/Table/V54.lean	1,482	48	27.61	28.92	27.64	1.28	12	0
LeanPool/Zeta5Irrational/Table/V55.lean	1,462	48	28.18	29.16	27.87	1.29	12	0
LeanPool/Zeta5Irrational/CircleAtoms.lean	141	44	3.81	2.65	1.35	1.30	11	0
LeanPool/Zeta5Irrational/EnergyBound.lean	365	44	14.30	13.19	11.78	1.41	11	0
LeanPool/Zeta5Irrational/Measure.lean	80	44	8.44	2.61	1.41	1.20	11	0
LeanPool/Zeta5Irrational/Table/V56.lean	1,265	44	18.43	26.58	25.27	1.31	11	0
LeanPool/Zeta5Irrational/ArcsineAtoms.lean	179	40	4.23	3.13	1.89	1.24	10	0
LeanPool/Zeta5Irrational/Arith/BasisChange.lean	118	40	3.92	2.72	1.40	1.32	10	0
LeanPool/Zeta5Irrational/Arith/PoleFun.lean	100	40	4.24	1.99	0.71	1.28	10	0
LeanPool/Zeta5Irrational/Construction.lean	93	40	3.79	1.73	0.46	1.27	10	0
LeanPool/Zeta5Irrational/Positivity.lean	261	40	10.13	5.04	3.76	1.28	10	0
LeanPool/Zeta5Irrational/Weight.lean	169	40	10.09	4.14	2.89	1.25	10	0
LeanPool/Zeta5Irrational/Arith/OuterFrame.lean	259	36	6.94	4.08	2.79	1.29	6	0
LeanPool/Zeta5Irrational/Constants.lean	60	36	3.64	1.61	0.41	1.20	9	0
LeanPool/Zeta5Irrational/PrimeSumStep.lean	144	36	7.93	2.79	1.58	1.21	9	0
LeanPool/Zeta5Irrational/EnergyFinal.lean	244	32	10.62	10.67	9.19	1.48	8	0
LeanPool/Zeta5Irrational/Growth/Assembly3.lean	179	32	5.96	6.69	5.40	1.29	8	0
LeanPool/Zeta5Irrational/Moments.lean	180	32	10.10	3.63	2.33	1.30	8	0
LeanPool/Zeta5Irrational/PrimeSum.lean	149	32	12.40	4.83	3.61	1.22	8	0
LeanPool/Zeta5Irrational/PrimeSumIntegral.lean	301	32	18.55	8.55	7.33	1.22	8	0
LeanPool/Zeta5Irrational/Stirling.lean	194	32	20.73	7.48	6.25	1.23	8	0
LeanPool/Zeta5Irrational/Arith/MomentVal.lean	128	30	4.02	2.87	1.57	1.30	5	0
LeanPool/Zeta5Irrational/Arith/OuterEntry.lean	162	30	5.16	3.37	2.09	1.28	5	0
LeanPool/Zeta5Irrational/Energy.lean	349	28	9.76	7.79	6.47	1.32	7	0
LeanPool/Zeta5Irrational/EnergyRaw.lean	254	28	6.91	5.97	4.52	1.45	7	0
LeanPool/Zeta5Irrational/Gaussian.lean	107	28	4.40	2.68	1.34	1.34	7	0
LeanPool/Zeta5Irrational/Growth/Assembly1.lean	196	28	6.47	4.92	3.56	1.36	7	0
LeanPool/Zeta5Irrational/Growth/Assembly2.lean	93	28	4.86	3.91	2.58	1.33	7	0
LeanPool/Zeta5Irrational/Growth/Constants.lean	135	28	5.01	4.16	2.83	1.33	7	0
LeanPool/Zeta5Irrational/Growth/TableIntegrals.lean	99	28	16.58	6.32	5.04	1.28	7	0
LeanPool/Zeta5Irrational/Arith/SmallPrime.lean	119	24	4.58	2.36	1.10	1.26	4	0
LeanPool/Zeta5Irrational/Arith/SmallPrimeTau.lean	226	24	7.98	5.25	3.98	1.27	4	0
LeanPool/Zeta5Irrational/Arith/TEntry.lean	111	24	3.69	2.40	1.12	1.28	6	0
LeanPool/Zeta5Irrational/Certificates.lean	166	24	23.49	15.84	14.61	1.23	6	0
LeanPool/Zeta5Irrational/EnergyLimit.lean	103	23	3.71	2.46	1.10	1.36	5	0
LeanPool/Zeta5Irrational/MainEstimate.lean	116	20	7.22	3.00	1.70	1.30	5	0
LeanPool/Zeta5Irrational/PartialFractions.lean	140	20	7.93	3.40	2.14	1.26	5	0
LeanPool/Zeta5Irrational/Arith/Unimodular.lean	179	16	4.84	3.15	1.58	1.57	3	0
LeanPool/Zeta5Irrational/Criterion.lean	142	16	3.94	3.88	2.66	1.22	4	0
LeanPool/Zeta5Irrational/HermiteFormula.lean	211	16	10.70	5.97	4.65	1.32	4	0
LeanPool/Zeta5Irrational/PotentialV.lean	79	16	9.98	2.34	1.04	1.30	4	0
LeanPool/Zeta5Irrational/Table/Tail.lean	185	16	25.98	8.63	7.33	1.30	4	0
LeanPool/Zeta5Irrational/Growth.lean	149	12	10.04	9.36	7.96	1.40	3	0
LeanPool/Zeta5Irrational/Growth/PieceIdx.lean	74	12	7.92	1.73	0.53	1.20	3	0
LeanPool/Zeta5Irrational/Growth/TablePrime.lean	105	12	15.61	4.82	3.55	1.27	3	0
LeanPool/Zeta5Irrational/Legendre.lean	81	12	5.62	2.01	0.75	1.26	3	0
LeanPool/Zeta5Irrational/RealBound.lean	134	12	18.04	7.43	6.14	1.29	3	0
LeanPool/Zeta5Irrational/DetIntegral.lean	78	8	4.27	2.20	0.89	1.31	2	0
LeanPool/Zeta5Irrational/Main.lean	43	8	5.85	1.65	0.33	1.32	2	0
LeanPool/Zeta5Irrational/Table/UpperCertificate.lean	39	8	8.38	2.00	0.67	1.33	2	0
LeanPool/Zeta5Irrational/Zeta5.lean	34	8	2.40	1.64	0.34	1.30	2	0
LeanPool/Zeta5Irrational/Arith/LowRank.lean	80	6	3.69	2.17	0.90	1.27	1	0
LeanPool/Zeta5Irrational/PNT.lean	33	4	5.88	1.93	0.30	1.63	1	0
LeanPool/Zeta5Irrational/Table/Bracket.lean	132	4	9.95	3.16	1.87	1.29	1	0
LeanPool/Zeta5Irrational.lean	25	0	2.67	3.46	0.24	3.22	0	0
Total	347,379	62,978	9438.33	9382.70	9105.94	276.76	15158	0

Aggregate phase totals

Phase	Time
interpretation	2680444.0 ms (= 2680.44 s)
norm_num	2348831.1 ms (= 2348.83 s)
typeclass inference	1663497.9 ms (= 1663.50 s)
tactic execution	932196.2 ms (= 932.20 s)
type checking	381071.3 ms (= 381.07 s)
simp	352599.9 ms (= 352.60 s)
import	276760.0 ms (= 276.76 s)
ring	192913.6 ms (= 192.91 s)
share common exprs	155279.8 ms (= 155.28 s)
elaboration	113419.7 ms (= 113.42 s)
process pre-definitions	101368.8 ms (= 101.37 s)
tacticAnalysis	48713.7 ms (= 48.71 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.Zeta5Irrational.Growth.InnerTable	863.00 s
LeanPool.Zeta5Irrational.Table.Intervals	249.00 s
LeanPool.Zeta5Irrational.Growth.OuterTable	239.00 s
LeanPool.Zeta5Irrational.Table.U55	165.00 s
LeanPool.Zeta5Irrational.Table.U54	165.00 s
LeanPool.Zeta5Irrational.Table.U53	158.00 s
LeanPool.Zeta5Irrational.Table.U51	152.00 s
LeanPool.Zeta5Irrational.Table.U52	151.00 s
LeanPool.Zeta5Irrational.Table.U50	146.00 s
LeanPool.Zeta5Irrational.Table.U48	146.00 s
LeanPool.Zeta5Irrational.Table.U49	145.00 s
LeanPool.Zeta5Irrational.Table.U44	143.00 s

Comment truncated to fit GitHub's 64 KB limit. This PR profiles 211 files; the per-file table shows only the 211 hottest by heartbeats. The full table and raw lean --profile output for every file are in the run's step summary and proof-profile artifact.

Advisory only — never blocks merge.