perf(NashEmbedding): cut median project build time by 12.45%

[Vilin97]

NashEmbedding imports the entire Mathlib.Tactic umbrella in 39 implementation modules. This narrows those imports to a shared tactic facade, preserves the full re-export at the canonical project entry point, and simplifies the Sobolev weight estimates.

• Keep tactic registrations explicit in NashEmbedding.Tactics, with shake: keep-all; retain Mathlib.Tactic at LeanPool.NashEmbedding with shake: keep for its existing public API.
• Import function-series continuity, real-power asymptotics and the original inner-product instances explicitly. The instance import preserves the original elaborated normed-space paths.
• Prove the small-frequency estimate using weighted sum-of-squares bounds; prove the exponential estimate by monotonicity; replace repeated whole-context normalization in the refined weight inequality with scalar estimates.
• Replace whole-context nonlinear arithmetic in the fixed-sequence tame bound and resolvent product estimate with targeted linear arithmetic and direct order lemmas. Simplify three norm-bucket comparisons by monotonicity.
• Supply local additive-group and module instances explicitly in the product-metric smoothness proof, avoiding repeated higher-order typeclass search.
• Add lattice-coordinate bounds and use them in the local-finiteness argument for periodic approximation.
• Remove six unused compiler-private proof-helper stubs and their compatibility comments, addressing configured review2181.

Base: f78a2fd57e35b09afea00517fbd384dd30124471. Measured head: 1e2200876d06278e7d7160a5355daee9af4094fe. Current cleanup head: af6d938289b4f6b23b92cdbbc3fa2997942d03d2. Uses current main's pinned Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e; no pin changes.

The following timings, profiles and environment inventories were reported for measured head 1e2200876d06278e7d7160a5355daee9af4094fe. They have not been rerun for the cleanup head, which removes 32 lines in one file and preserves all remaining source bytes.

Revision	Run	Wall seconds	User seconds	System seconds	Max process RSS KiB
base	1	121.95	307.20	34.97	1,981,436
head	1	112.15	277.99	30.74	1,812,036
head	2	113.61	277.83	30.54	1,811,896
base	2	129.77	311.02	34.82	1,956,352
base	3	133.93	314.71	34.72	1,972,244
head	3	118.38	280.96	30.70	1,814,984

Median wall time: 129.77 → 113.61 seconds (12.45% lower). Median maximum process RSS: 1,972,244 → 1,812,036 KiB (8.12% lower).

Median user CPU time is 311.02 → 277.99 seconds (10.62% lower). The 10% wall-time target is met.

Both revisions use /usr/bin/time with lake --wfail build LeanPool.NashEmbedding.Imports. Each run deletes only this project's artifacts under .lake/build/lib/lean and .lake/build/ir; pinned dependency artifacts and the filesystem cache remain warm. Three runs per revision use the counterbalanced order base/head/head/base/base/head, with identical settings and no source edits or overlapping local validation jobs during measurement. RSS is GNU time's maximum single-process resident set, rather than aggregate concurrent memory. The VM is shared, so wall time has scheduling noise.

The isolated MultiplicationBootstrap profile (lake env lean --profile -DElab.async=false …) changes user CPU time from 18.40 to 13.51 seconds and maximum RSS from 2,167,164 to 1,829,120 KiB. The Sobolev.Basic import environment shrinks from 4,759 modules / 447,139 constants to 3,800 / 369,067; AmbientMetric shrinks from 5,008 / 467,526 to 4,417 / 424,626. The complete entry-point API remains intact.

The author's pre-edit Lean environment-manifest comparison at measured head 1e2200876d06278e7d7160a5355daee9af4094fe covered 1,533 unique pre-existing declarations, including private and generated declarations. It compared fully qualified names, universe parameters, declaration kinds and safety, elaborated types, non-theorem bodies, reducibility/mutual metadata and inductive data, excluding theorem proof bodies, bound-variable alpha names and nonsemantic expression metadata. The author reported no differences or removals at that revision and preservation of 386,945 exported public names, with two added public lattice-coordinate lemmas. These are historical observations. The current cleanup intentionally removes six unused source-written compiler-private compatibility stubs; no fresh compiled declaration/export census is claimed for it. All remaining definitions, theorem statements and proof text are byte-identical to the measured head.

Import analysis used lake shake --force --keep-public LeanPool.NashEmbedding.Imports without --fix. It still reports redundant-import suggestions; those re-exports are retained for API stability.

Historical validation reported for measured head 1e2200876d06278e7d7160a5355daee9af4094fe:

• Warning-failing project builds for every measured run.
• CI's scripts/ci/lint-project.lean over all 58 project modules: 1,541 declarations, zero findings.
• lake exe lint-style LeanPool.NashEmbedding.Imports.
• lake exe mk_all --module --check and git diff --check.
• uv run python -m lean_pool.quality --repo .. --static-only for repository-wide static checks.
• Repository quality functions _audit_axioms, _run_option_audit and _check_project_declarations on all project modules: 841 source declarations plus the compiled environment audit, zero findings.
• Pre/post declaration manifests and exported-name inventories; unchanged measured-source fingerprints; the post-measurement manifest again reports zero differences.

Only NashEmbedding sources and its generated project import index change. LeanPool.lean, the registry, dependency pins and all gates/configuration remain unchanged. Whole-pool validation and independent review remain required in CI. This PR does not enable auto-merge or request a protected merge.

The cleanup at af6d938289b4f6b23b92cdbbc3fa2997942d03d2 has a complete one-file source-delta review and exact Git blob readback. Local compilation and benchmarking have not been repeated. Fresh hosted CI and automatic configured review are required before protected integration.

[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 defect was found in the latest changes; whole-pool validation remains required before merging.

Summary

This PR narrows tactic imports and replaces costly proof steps in NashEmbedding. The latest revision removes six unused private proof helpers.

• NashEmbedding modules use a smaller shared tactic facade.
• Sobolev weight estimates use simpler exponential and sum bounds.
• Periodic approximation bounds the lattice shifts it needs.
• Perturbation estimates use focused order and arithmetic steps.
• Product-metric smoothness fixes its bundle instances locally.

_{Reviews (2) · Last reviewed commit: "Remove unused compiler-private compatibi..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "At 1e22008, this refactor narrows implementation imports through an explicit tactic facade while retaining Mathlib.Tactic at the canonical entry point. The small-frequency and refined Sobolev weight arguments now expose their scalar inequalities, the tame/resolvent estimates name their arithmetic inputs, and periodic approximation reuses two coordinate bounds. I reviewed the complete 43-file delta. The existing statements and mathematical hypotheses remain intact at source level. The author's environment-manifest and timing reports are retained as attributed evidence; I did not repeat those measurements. Current-head CI and the automatic configured review remain separate pending integration requirements.",
"assessment": {
"scope": "tactic import narrowing and structured proof optimization",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The explicit scalar estimates, reusable coordinate bounds and preserved entry-point re-export improve maintainability without an actionable source defect."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

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

Reviewed head: af6d938289b4f6b23b92cdbbc3fa2997942d03d2

Verdict: ✅ approve

The refactor centralizes tactic imports while retaining the full entry-point re-export, replaces broad arithmetic searches with explicit estimates, and extracts reusable lattice-coordinate bounds. The rewritten proofs preserve useful intermediate steps and make dependencies clearer. No actionable maintenance regression was found. Compilation and reported speedups were not independently verified because this checkout lacks dependency artifacts.

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

The explicit estimates, restricted arithmetic calls, and reusable bounds improve maintainability without introducing actionable technical debt.

---

Tokens: 1,326,355 in / 5,989 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $5.3953 (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.

[Vilin97]

Reviewed af6d938289b4f6b23b92cdbbc3fa2997942d03d2 against its sole parent 1e2200876d06278e7d7160a5355daee9af4094fe. The full delta removes six unused compiler-private theorem stubs and their two preservation comments: 32 deleted lines in one file. Every remaining source byte, including the mathematical definitions, theorem statements and proof text, is unchanged. The published Git blob matches the reviewed cleanup.

This addresses configured review2181's concrete maintenance finding. I withdraw my earlier justification for preserving those stubs as a compatibility cost; the rest of the 43-file mathematical/import review remains supported by the unchanged source. Source verdict: approve, advisory quality4.

The timing and compiled-manifest observations concern the historical 1e22 revision. I have not repeated local compilation, a compiled declaration census or benchmarks for this cleanup. New-head hosted checks, automatic configured review and the current-main validation predicate remain pending; no queue admission or merge has been requested.

[Vilin97]

/review

Please review current head af6d938289b4f6b23b92cdbbc3fa2997942d03d2. It removes the six unused private theorem stubs identified in configured review 2181 at 1e2200876d06278e7d7160a5355daee9af4094fe, as documented in the exact-head source review.

The exact-head CI run has passed index validation, build, lint, text style, repository quality, and canonical Build project.