perf(MetricCodes): narrow imports and simplify spectral proofs

[Vilin97]

MetricCodes exports several proof-only Mathlib modules through its long public import chain, and some spectral proofs use unrestricted arithmetic for local linear or factored inequalities. This change narrows those imports and makes the affected proof steps explicit while preserving the existing project API.

The pass:

• Uses lake shake to identify signature dependencies and makes proof-only Mathlib imports private. Retains every original public import between MetricCodes modules.
• Proves the factors in associatedEdge_pos with restricted linear arithmetic, add_pos, sq_sub_sq and mul_pos.
• Replaces nonlinear automation in harmonicAxisLift_injective with the direct order argument, and restricts the arithmetic inputs in harmonicDimension_scaled_choose.
• Reuses the existing Hamming entropy theorem for the identical Johnson result, supplies the ambient dimension at two dependent theorem applications, and removes an unused powerset simp argument.

Base: 345a941d32351dccde79aad56bb4a42b9c4d5cd2. Lean/Mathlib: the existing v4.35.0-rc3 pins, with dependency revisions verified against the committed manifest.

Before editing, an environment-inspection script captured all 10,379 project constants, including private/compiler-generated declarations. It recorded complete constant metadata, universe parameters, elaborated types, safety, and every non-theorem value as structural expression DAGs; only theorem proof bodies were erased. The comparison preserves every original declaration. Two raw differences are compiler-generated bound-variable display IDs in private arithmetic helper types: their de Bruijn structure, binder annotations and all other data agree. Every definition value agrees exactly. Import narrowing generates two additional private Lagrange equation helpers. Source declaration signatures are unchanged.

The full original manifest's canonical-record SHA-256 is 77e14c44e510b6c2d6e768174322033038ac06a0def64f1bd0d1087343f4b741. The candidate manifest's raw canonical-record SHA-256 is d39eccb64b518432e6df77e74dd6af33c22a9fe75968370959e01e91805fb3ab.

Observed clean-project measurements:

Run	Base wall (s)	Optimized wall (s)	Base maximum child RSS (KiB)	Optimized maximum child RSS (KiB)
1	681.36	582.45	2,142,896	2,140,992
2	617.40	569.93	2,145,472	2,138,796
Median	649.38	576.19	2,144,184	2,139,894

Median wall time is 11.27% lower, meeting the 10% wall-time target. Median user+system CPU time is 1013.185s → 977.150s (3.56% lower); RAM is essentially unchanged (0.20% lower). These are shared-VM observations, with limited causal attribution of the wall-time difference.

The public-import environment also preserves all 7,247 original constants with exact records; it contains only the same two additional private Lagrange helpers. The full compiled audit was repeated after the final clean rebuild with the same result.

Head: f13575d532834d022dc0f81af0cc7980e917c5ce.

Each measurement deletes only this isolated worktree's MetricCodes Lean/IR outputs, keeps exact pinned dependency artifacts warm, and runs:

LEAN_NUM_THREADS=1 /usr/bin/time -v lake --wfail build LeanPool.MetricCodes.Imports

RAM means GNU time's maximum child-process RSS, in KiB. The VM is shared, so wall-time measurements include scheduler variability. Diagnostic declaration traces are separate from these measurements. The standalone synchronous Conclusion diagnostic reported rewrite errors and its total is unavailable/excluded; every measured standard Lake build must succeed warning-free.

Local validation:

• Warning-sensitive build of all 17 project modules.
• Slow declaration linters from scripts/ci/lint-project.lean: all 17 modules / 10,381 declarations.
• lake exe lint-style LeanPool.MetricCodes.Imports.
• The unchanged repository quality functions on a selected-project view, plus actual-worktree axiom and option-backdoor audits over all 17 modules.
• The unchanged generated-index validator on the selected project's complete inventory.
• Full compiled declaration comparison and textual signature comparison.

Repository-wide CI and independent refactor review remain applicable. This PR is left open without automatic merging.

[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 impact] The reviewed refactor appears safe to merge; no actionable defect was found.

Summary

MetricCodes narrows public Mathlib imports while retaining its public project import chain.

• MetricCodes keeps its public import chain while localizing proof imports.
• Johnson edge positivity follows from explicit factor signs.
• Harmonic proofs use a direct order argument and focused arithmetic.
• Several MetricCodes proofs reuse known facts and name implicit inputs.

The reported build timings and compiled-declaration comparison were not independently repeated. External source and license claims were not re-audited; this refactor changes neither the project card nor those claims.

_{Reviews (1) · Last reviewed commit: "perf(MetricCodes): narrow imports and si..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "This refactor narrows Mathlib import exposure within MetricCodes, uses explicit arithmetic hypotheses and factored positivity arguments, and reuses an existing entropy identity. The two dimension arguments are now explicit at their call sites. I found no actionable maintenance regression; the published compilation, declaration-manifest and timing results were not independently rerun.",
"assessment": {
"scope": "import exposure and targeted spectral proof simplification",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The smaller dependency surface and direct named arguments improve maintainability while preserving the reviewed project proofs."
},
"verdict": "approve",
"findings": []
}