perf(Erdos367): narrow imports and replace proof search

[Vilin97]

Selected project

This refactors LeanPool.Erdos367, selected because its six-file development has about 13,800 lines and a transitive closure of roughly 3,700 modules. The pass removes six unused private Mathlib imports from the entry module and replaces opaque aesop proof search with direct omega, nonzero, divisibility, and witness terms in Core139, RFullLowerBound, and PellLimsup.

Semantic invariant audit

Base: 38b8ba36899903cb7d3a42bb9f8a3f5c70fdb05f

Head: d4a477e6f35ac625627332f5f2a19467f32d145a

I compiled an environment manifest from the base and head with Lean environment inspection. Both contain 236 declarations in the LeanPool.Erdos367 module closure. Every public declaration has unchanged kind, safety, universe parameters, reducibility metadata, type hash, and fully printed type. The only manifest differences are three private generated simp-companion names whose numbering changed as proof elaboration changed; their types and generated private status are unchanged. No public declaration was added, removed, renamed, or retyped.

Measurements

Lean profiler (-Dtrace.profiler=true) on base → head:

• RFullOdd.rFullPart_pow: 0.226 → 0.189 s
• RFullOdd.pow_dvd_rFullPart: 0.364 → 0.262 s
• Erdos367.prime_sq_dvd_pellN_plus2: 0.606 → 0.543 s
• Core139.T3: 1.182 → 1.225 s (a small local tradeoff for deterministic arithmetic closure)

A clean project build was measured before editing at 16.70 s with the warm pinned Mathlib cache. The later clean head run rebuilt 3,775 Mathlib/project jobs after the shared cache was invalidated, so that 690.89 s run is not used as a comparable wall-clock result.

Validation

Passed:

• lake build LeanPool.Erdos367 (warning-free)
• lake exe runLinter LeanPool.Erdos367
• #print axioms for all three registered main results: only propext, Classical.choice, and Quot.sound
• repository textual quality checks (zero errors)
• git diff --check

lake exe mk_all --check and lake exe lint-style LeanPool.Erdos367 could not link in this worktree because the shared package cache lacks native Cli objects; the linker reports missing lp_Cli_* symbols. A repository-wide lake build LeanPool was attempted and reached 8,423/9,058 jobs before interruption because this isolated checkout had to rebuild the broad pool from an empty root cache. No Lean error was reported for the changed project.

[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 risk] Replaces proof search tactics with explicit proofs in math library.

No blocking issue was identified in the four-file PR diff; the full-library build was not independently verified.

Summary

This PR narrows the Erdos367 entry module’s imports and replaces proof-search steps with explicit arithmetic, divisibility, and witness proofs. The four-file PR diff does not change theorem statements.

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

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 86 tracked declarations across 4 modified files kept their type; only proofs / definition bodies changed.

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: 349 → 349 (+0, +0.0%). Declarations: 86 → 86.

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

Files: 4 compared — 0 cheaper, 0 costlier, 4 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 Mathlib's linter.countHeartbeats, in maxHeartbeats units. Δ lines counts added/deleted lines from this PR diff.

File	Δ lines	HB base	HB head	Δ HB	Δ HB %	Wall base (s)	Wall head (s)
LeanPool/Erdos367.lean	+0/-6	0	0	+0	—	6.02	4.88
LeanPool/Erdos367/Core139.lean	+1/-1	68	68	+0	+0.0%	9.74	8.76
LeanPool/Erdos367/PellLimsup.lean	+3/-2	224	224	+0	+0.0%	17.52	18.06
LeanPool/Erdos367/RFullLowerBound.lean	+6/-3	57	57	+0	+0.0%	3.91	3.73
Total	+10/-12	349	349	+0	+0.0%	37.2	35.4

Per-project compile cost (top 2 of 2 projects by |Δ heartbeats|):

Project	Files	HB base	HB head	Δ HB	Δ HB %
(root)	1	0	0	+0	—
Erdos367	3	349	349	+0	+0.0%

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

[Vilin97]

🤖 LLM review — refactor (gpt-6-astra)

Reviewed head: 030d2ad0e276fe3915bcc972490bb0636c61abf4

Verdict: ✅ approve

The refactor removes six unused private imports and replaces six aesop calls with explicit nonzero and divisibility arguments, a finset witness, targeted simplification, and omega after arithmetic normalization. It preserves the intermediate proof structure and reusable lemmas while reducing dependence on proof search. The supplied /profile reports unchanged heartbeats (349 → 349), with no material compile-cost regression demonstrated.

Aspect	Value
Scope	import cleanup and targeted tactic rewrites
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The replacements make proof dependencies clearer without sacrificing structure or introducing actionable maintenance debt.

---

Tokens: 177,984 in / 2,370 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $1.8983 (Standard API equivalent; uncached input)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

Exact-head reconciliation\n\nReviewed current head 7ae852c3a99fa73167fb2a61afd607c537d50b1b after merging current main in an isolated worktree. The Erdos367 refactor files are unchanged; the merge only brings the already-merged mainline content up to date. The prior exact-content refactor review remains applicable, subject to fresh protected CI on this SHA. Queue normal protected squash merge once required checks pass.

[Vilin97]

Maintainer decision required

Reviewed exact current head 7ae852c3a99fa73167fb2a61afd607c537d50b1b. The substantive review is complete and the current protected checks are still running; no code or policy waiver is requested. This repository has auto-merge disabled (GitHub rejects gh pr merge --auto), so the branch cannot be safely queued for protected auto-merge. After all required checks are green, a maintainer must either enable the repository's normal auto-merge path or perform the protected squash merge. The label records only that operational decision.

[Vilin97]

/review

[Vilin97]

Maintainer re-review

Reviewed exact current head 794b78e299a54ebdfeb0660d548542867c47a4d0. The only change since the previously reviewed content head 7ae852c3a99fa73167fb2a61afd607c537d50b1b is a merge of current origin/main commit f05dc6511cf0b80cbed98a71347bbb1320f02a40, which updates the repository's already-merged index-system CI configuration. The Erdos367 refactor files are unchanged; the prior review, proof profile (349 → 349 heartbeats), and protected checks remain applicable to the content.

Fresh required checks for this exact head are queued. The branch is now current with origin/main; needs-maintainer remains for the human protected squash-merge decision because auto-merge is disabled.

[Vilin97]

Re-reviewed 9528966fcee3fe31999fc5d7eb3eacda42efdab7: maintainer blocker resolved; required CI/review remains pending.

The complete four-file refactor preserves public statements and useful proof structure while replacing proof search and removing six private imports. No actionable source defect remains. Another worker pushed the same integration tree while this cycle was running; the prepared push was stopped, and this exact remote head was independently validated. No duplicate commit was pushed.

Targeted warning-free project build, actual mk_all --module --check, Mathlib linters, style, and the unchanged repository quality checker all pass. Quality/trust checks covered byte-identical project copies with unchanged Lake/linter configuration, including the axiom and compiled-environment backdoor audits; this is project-scoped validation, not a new full-pool pass.

The older automation hold is now contained: the existing needs-manual-rebase label excludes this branch from the registry updater and is retained. The parser defect still reproduces and has its own repair in #532. Removing needs-maintainer does not re-enable that updater. No per-PR human decision or author change request remains. Ordinary full CI, documentation and the configured review must pass on this exact head before any protected merge; no merge was attempted.

[Vilin97]

Reviewed head: 2222c9203324d9adad13b495229878a488afdcbf

Verdict: approve. Posted as a comment review because GitHub does not permit the authenticated PR author to submit an approving review.

The Erdos367 refactor removes six private entry-module imports and replaces proof search with explicit nonzero, divisibility, and finite-set witness terms. The omega replacement closes the existing normalized arithmetic step in T3 without removing its documented inequality chain. Full diff and affected-source review found no actionable regression. Exact-head CI passed the full build, index check, linters, style, and repository quality checks, resolving the PR description's older local linker limitations; these checks were inspected rather than rerun locally. The advisory profile reports 349 to 349 heartbeat units and no material deterministic regression. The author's small T3 wall-time increase is a disclosed local tradeoff, not evidence of a significant compile-cost regression.

Assessment	Result
Scope	proof-search replacement and private-import pruning
Introduces technical debt	No
Maintainability	Improved
Brittleness	More robust
Risk	Low

The refactor exposes routine proof dependencies and preserves the argument and public imports, so no source repair is required before merging.

Findings: none.

Validation evidence: full build and gates, proof profile.

[Vilin97]

Updated to current main cd2e11846a1a8ae3028d9274112200bb199bcc40 at 01d70128c88eaf41948914a390f90595c242e82a after the Puiseux import merged. All four previously reviewed Erdos367 files remain byte-identical; the registry and generated root index exactly match main. The actual pinned mk_all --module --check passes. The previous full green CI and substantive review remain valid for the unchanged source; required checks must rerun on this integration commit before merging.

[Vilin97]

Carry-forward review at 9528966fcee3fe31999fc5d7eb3eacda42efdab7: incorporated main 854da85a8bc6c9219c2c04ec9d43d4a49f43aef8. The delta from the just-reviewed integration commit 01d70128c88eaf41948914a390f90595c242e82a is only generated NOTICE and README metadata. All Lean source, theorem contracts, registry and index bytes are unchanged, so the prior source review and actual index check carry forward. Fresh required CI remains necessary before normal merge.

[Vilin97]

Daily disposition: needs maintainer — protected merge operation

Reviewed exact head 5e203e4a77fd51d542a8928bd5060caab6d15d9d. The four-file refactor preserves the conditional bounds and unconditional Pell limsup results, and reduces broad proof search/import fan-out. It does not completely solve sourced Erdős problem 367 and is not accepted as a solution to it. The complete source/dependency review and recovered repairs were reconciled through the lossless main integration; fresh protected CI remains the integration authority.

Build project: pending/not yet reported, Content / non-content separation: QUEUED, Documentation preflight: SUCCESS. These are observed check states, not an assertion that unfinished checks passed.

The remaining authority boundary is operational: this repository has allow_auto_merge=false, and GitHub rejected enablePullRequestAutoMerge with “Auto merge is not allowed for this repository.” The maintainer must make protected queuing available through an authorized repository-setting decision, or remove this label and perform a normal squash merge after the required checks and current-base integration pass. This cycle does not change repository settings or bypass protection. No unresolved substantive author-actionable finding justifies another change request or closure; the label is not for draft status, missing profiling, or an old advisory score.

[Vilin97]

Independent review of exact head ad19b3018bdf925a4e299c2ea3c37e5e7cac17d8: The four-file import/proof-search refactor preserves the existing conditional bounds and unconditional Pell limsup results. Those are independently significant intermediate theorems; this PR does not completely solve sourced Erdős problem 367 and is not accepted as a solution to it. All material findings are resolved; scoped sources, provenance, licensing and novelty checks remain valid. The proof/interface delta was inspected; documentation-only or main-integration changes do not introduce a new mathematical claim. Current required checks are green and no unresolved human changes request remains. Approved by review comment because GitHub forbids self-approval.