Reduce MetricCodes spectral and harmonic proof elaboration cost

[Vilin97]

MetricCodes repeatedly used nonlinear search for scalar identities already implied by squared equalities and positivity. This replaces that search with direct Mathlib lemmas and makes coordinate and linear-map elaboration explicit. The change covers 13 theorem proofs across eight files.

All existing statement syntax, definitions, universes, safety levels, names, imports, attributes, namespace exports, the project card and generated indexes remain unchanged.

Base: 0c1132c7a9a2b320f9c37556412a4733e45c6a47.
Head: c4842def77880bb16e60d1f39ae4cb6fd43b061f.
Toolchain: the repository's existing Lean/Mathlib v4.35.0-rc3 pins. Main was 5de7c4e86d2907ee4f6410ce10cfb21d212219dd immediately before commit; MetricCodes, these pins and the applicable contribution/review policies were unchanged since the recorded base. The branch preserves its validated base checkpoint.

MetricCodes has roughly 112,000 lines across 17 modules. It was selected from five large candidates using an existing recording whose 17 MetricCodes sources are byte-identical to this base. It had the highest recorded source-capture total among those candidates: 443.892 seconds, versus 301.758 for PhaseRetrieval, 156.152 for SpherePacking, 142.408 for EhrhartVolumeInequality and 89.147 for NonSoficGroup. That recording identified the nonlinear edgeLimit_sq_div_zero proof and expensive coordinate/operator conversions. This is selection evidence, not a claim of a global optimum over the pool.

Concrete changes:

• Rewrite div_pow and Real.sq_sqrt before clearing denominators in edgeLimit_sq_div_zero.
• Use sq_eq_sq₀ for uniqueness of nonnegative square roots and linear_combination for an already derived polynomial identity.
• Use Real.inner_apply directly in coordinate pairings.
• Simplify the specific root-complex compositions needed by the intertwining proofs, and apply adjoint-row hypotheses with explicit simplification lists.
• Specify the continuous operator in self-adjointness, use direct continuity composition, restrict unit-scalar simplification and apply an established operator identity directly.

Before editing, an external Lean environment inspector imported all 17 modules with importAll := true, trust level zero and extensions disabled. It serialized full elaborated expression DAGs, universe parameters, declaration kinds, safety/partial flags, reducibility hints, associated declarations, inductive/recursor data and all non-theorem values. The comparator ignores expression metadata and theorem proof bodies. It checks generated private declarations as well as public declarations, keyed by module and name.

Final audit: 10,372 pre-existing entries; zero missing, zero changed; seven new generated proof helpers, for 10,379 total. Source review confirms that every diff is inside an existing theorem proof and that imports, notation, namespaces, exports and attributes are unchanged. The all-declaration axiom traversal found only Classical.choice, propext and Quot.sound.

Manifest SHA-256:

• Base: 5c88ab724675dbfc3899c020147a121df102c92013acf3038140065518520538
• Head: c542b859747f546e11b6b2c7504028ed54ec9b43a9a701d729c652b52c9336dd

Three clean project builds per revision were run in the predeclared order base/head/base/head/base/head on the same Azure VM. Before each lake build LeanPool.MetricCodes.Imports, all MetricCodes artifacts under the worktree's .lake/build/lib/lean and .lake/build/ir were deleted. Pinned dependency caches remained warm and Lake used its normal parallelism. GNU time recorded wall/user/system time and peak compiler RSS. No local profiles or linters ran alongside these six builds. All six passed without warnings.

Pair	Base wall s	Head wall s	Base user CPU s	Head user CPU s	Base peak RSS KiB	Head peak RSS KiB
1	595.19	599.65	997.40	955.06	2,193,632	2,140,644
2	682.72	725.33	1020.20	999.91	2,186,568	2,146,704
3	766.38	562.33	1044.53	930.89	2,181,064	2,144,360

The predeclared per-revision median wall time is 682.72 → 599.65 seconds (12.17% lower). Median user CPU is 1020.20 → 955.06 seconds (6.39% lower); median peak compiler RSS is 2,186,568 → 2,144,360 KiB (1.93% lower).

These are observed shared-VM measurements. Other VM workloads were uncontrolled, baseline wall time varied substantially, and two paired head wall runs were slower. The median point estimate meets the requested 10% wall-time target; it does not establish a repeatable 10% causal wall-time gain on every CI run. User CPU fell in all three pairs. The initial exploratory native build was 761.66 seconds and is excluded from this controlled comparison.

Successful serial diagnostics used each module's native --setup file with -DElab.async=false -Dtrace.Elab.command=true -Dtrace.profiler=true -Dtrace.profiler.useHeartbeats=true -Dtrace.profiler.threshold=1000000000000000000. These timings and heartbeat counts are separate from native parallel build measurements.

Declaration (short name)	Base heartbeats	Head heartbeats
coupledDegreeCoordinates_pairing	98,277.284	9,891.843
clebschNormSq_succ_mul	24,357.939	11,940.378
johnsonMiddleSignedScalar_eq_sqrt_hattedDiagonal	87,110.806	12,329.468
johnsonLowerOffDiagonalScalar_eq_sqrt_source	36,113.340	3,153.649
edgeLimit_sq_div_zero	126,119.381	5,614.230

The instrumented serial module times were Binary 173.533465 → 94.424273 seconds, Rates 228.242240 → 113.392967, and HarmonicAnalysis 274.448111 → 202.543170. An instrumented baseline Rigidity run exceeded the normal heartbeat budget and is excluded from file-time comparisons; no limit was increased. Normal native builds passed.

Validation:

• lake --wfail build LeanPool.MetricCodes.Imports, plus the six clean native builds and warning scans.
• lake env lean --run scripts/ci/lint-project.lean <all 17 project modules>: passed, 10,379 declarations.
• lake exe lint-style LeanPool.MetricCodes.Imports: passed.
• Existing repository quality functions, externally scoped to all 17 project files and the unchanged metric-codes.yaml: headers, forbidden constructs/options, size limits, card/declaration resolution, axioms and compiled option/backdoor audit passed. No checker or gate was modified.
• Independent all-declaration axiom traversal and final declaration-manifest comparison: passed.
• python3 scripts/project-indexes.py --repo <MetricCodes-only projection> --module --check: passed with the unchanged official generator. No modules were added, removed or moved, so indexes need no edits.
• git diff --check: passed.
• lake shake --force --keep-public LeanPool.MetricCodes.Imports: analyzed the built target and reported two redundant-public-import suggestions (exit 1); imports were preserved.

Whole-pool integration and protected PR checks remain for CI. Full logs, source snapshots, manifests, inspector/comparator, timing scripts and exact-head checkpoint are preserved under /data/codex/scratch/vilin/optimization-20261016/.

Leave this PR open for normal protected review. No merge, queue entry or auto-merge is requested by this cycle.

[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 proof-only refactor appears safe to merge, with no actionable issue found.

Summary

This refactor replaces proof search with direct identities and explicit conversions in 13 existing proofs across eight files. The full diff stays inside theorem proofs; statements, definitions, imports, attributes, and project metadata remain unchanged.

• Scalar proofs use direct identities instead of broad arithmetic search.
• MetricCodes proofs spell out key conversions more directly.

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

[Vilin97]

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

Reviewed head: c4842def77880bb16e60d1f39ae4cb6fd43b061f

Verdict: ✅ approve

This refactor replaces nonlinear search with direct algebraic lemmas and makes coordinate, continuity, and operator conversions explicit across 13 proofs. Intermediate mathematical facts remain visible, and explicit simplification lists reduce dependence on tactic defaults. Reviewing the full diff, surrounding proofs, and callers revealed no actionable maintenance regression. Builds and benchmarks were not reproduced because compiled dependencies are absent.

Aspect	Value
Scope	proof elaboration and tactic rewrites
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The refactor reduces proof-search dependence while retaining proof structure and reusable results.

---

Tokens: 536,522 in / 6,515 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $2.2438 (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]

{
"summary": "Reviewed exact c4842de: all eight complete diffs and 13 changed proof commands preserve the existing declaration interfaces. Direct square-root uniqueness and polynomial identities replace nonlinear search; explicit coordinate, continuity and operator conversions retain the mathematical steps. The refactor improves maintenance without an actionable regression.",
"assessment": {
"scope": "13 theorem proof bodies across eight MetricCodes modules",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "Targeted lemmas and explicit conversions reduce proof-search and elaboration dependence while retaining all existing statements and surrounding source."
},
"verdict": "approve",
"findings": [],
"validation": {
"head": "c4842def77880bb16e60d1f39ae4cb6fd43b061f",
"source": "Complete eight-file comparison; independent source check preserves all 13 declaration headers and every byte outside those proof bodies. No definitions, imports, attributes, namespaces, cards or gates change.",
"checks": "Current-head Build project and Build pool succeed; all eight required GitHub Actions contexts are complete with their applicable SUCCESS or workflow-scope SKIPPED results. Configured refactor review 2149 approves this exact head; no unresolved review threads.",
"measurements": "Contributor measurements remain attributed. Median wall time is 682.72 to 599.65 seconds, but two paired head wall runs are slower and shared VM load is uncontrolled. This review claims no repeatable causal 10% speedup and does not replay the successful builds or environment inspector.",
"integration": {
"status": "MERGED through the protected native queue",
"source_head": "c4842def77880bb16e60d1f39ae4cb6fd43b061f",
"merge_commit": "ec8d6a90ffebe2406a65c982dd52dbc46499a44f",
"merged_at": "2026-10-16T10:30:11Z",
"native_run": 38885730712,
"build_pool": 116923043087,
"required_Build_project": 116928995442,
"all_eight_required_contexts": "Completed SUCCESS or legitimate scope SKIPPED from app15368",
"validation": "Native index/build/lint/style/quality pipeline succeeded; validated cache reuse is not described as a fresh cold rebuild.",
"attribution": "Earlier Root normal queue admission completed; no second merge or enrollment request.",
"remaining_PR_integration_work": "None; current-main post-merge validation is tracked separately."
}
}
}