Reduce MetricCodes proof elaboration cost

[Vilin97]

MetricCodes has expensive arithmetic, calculus, and tensor/linear-map elaboration spread across roughly 112,000 lines and 17 modules. This refactor reduces proof search and repeated elaboration while preserving every original declaration. The observed three-build median wall time is 584.36 → 562.09 seconds (3.811% reduction).

MetricCodes was selected from the large completed-project profiles because its long derivative/arithmetic proofs and repeated adjoint/tensor arguments offered concrete remaining opportunities. Fresh synchronous diagnostic command profiles identified the spectral-margin derivative and several 5–9 second linear-map proofs. Earlier MetricCodes optimizations were already merged before this baseline; this cycle changes exactly this one project.

Base: b25d6804654bbfd206eb31cdbd6360d1f63d5cd1. Head: 216782909c1daee9b3659094e01b6d94d121c27f.
The branch was prepared in an isolated worktree. Immediately before committing, current main was fetched at 2aaa7220788257635be774b855528c4f0be6f3bd; it had no intervening changes to this project, repository policies, the toolchain, or dependency pins. The branch was not rebased to chase main. The existing repository pins are Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e.

Changes

• Replace redundant nonlinear arithmetic with linear arithmetic; bound arithmetic search with explicit support sets. Use structural associativity/commutativity proofs where normalization was unnecessary.
• Simplify the spectral-margin derivative and boundary factor calculations before clearing denominators. Remove local facts absent from the elaborated proofs.
• Reuse 14 earlier theorems with exactly identical propositions and give direct theorem arguments explicitly where inference repeated expensive work.
• Factor spanning-range adjoint orthogonality, abstract adjoint composition, and finite-sum composition lemmas; reuse them in the padded-Pieri and mixed-rotation proofs. Cancel the injective polynomial inclusion at the linear-map level in the weighted Chevalley–Eilenberg square-zero proof.
• Use selected explicit equation lemmas and restrict unfolding. No modules or imports changed; a read-only lake shake --force --keep-public LeanPool.MetricCodes.Imports audit found no useful dependency-closure reduction that preserved all original private/generated declarations.

There are 14 changed Lean files, 900 insertions, and 1,323 deletions. Only the selected project's proof files changed. The project card and generated module indexes require no updates.

Invariant audit

Before editing, an immutable compiled base snapshot and declaration manifest were recorded. Lean environment inspection enumerates selected modules' constNames, including private and compiler-generated declarations. For non-theorems, the audit compares full ConstantInfo with Lean structural equality, including elaborated bodies, types, universe parameters, safety, and inductive/recursor metadata. For theorems, it compares the exact ConstantVal and mutual-declaration list, excluding only proof bodies. Compact hashes are an index, not the equality test.

The final independent cold build was audited again: 10,381 original declarations, 10,396 head declarations, 15 additions, zero changed or removed original declarations. Module ownership and the complete compact manifests also agree for every original. All 51 immutable base compiled-artifact checksums remain unchanged. The additions comprise five optimization helper theorems and ten generated theorem auxiliaries. Existing declaration statements, definitions, names, universes, and safety are preserved; source review also confirms existing notation and declaration attributes were not edited.

Measurements

Three complete clean-project builds per revision, with identical warm pinned dependencies, ordinary repository Lake settings, and no concurrent compiler/profiler jobs from this optimization task. All 17 project modules were freshly rebuilt on every run. Build order: base/head, head/base, base/head. The benchmark used independent build directories and deleted selected-project compiled artifacts before each run.

/usr/bin/time -f 'wall_seconds=%e peak_rss_kib=%M user_seconds=%U system_seconds=%S' \
  lake --wfail build LeanPool.MetricCodes.Imports

Pair	Revision	Wall seconds	Peak RSS KiB	User CPU seconds	System CPU seconds
1	base	504.06	2,144,632	912.53	14.42
1	head	574.81	2,126,500	908.12	14.63
2	head	545.12	2,113,784	859.31	16.48
2	base	584.36	2,137,904	934.59	14.74
3	base	601.09	2,148,808	947.05	14.65
3	head	562.09	2,129,580	889.45	14.50

Median wall time: 584.36 → 562.09 seconds (3.811% reduction). Median peak single-process RSS: 2,144,632 → 2,126,500 KiB (0.845% reduction). Median user CPU: 934.59 → 889.45 seconds (4.830% reduction).

The requested 10% wall-time or RSS target was not met. Optimization continued through the six-hour alternative stopping condition (2026-10-19 21:15:09 through 2026-10-20 03:15:09 UTC). The measurements do not establish the requested 10% improvement.

Diagnostic proof elaboration examples, separate from the wall-time result: the weighted differential square-zero command decreased from 51,945 to 2,018 heartbeats; the root exterior bracket square command decreased from 110,077 to 45,938 heartbeats. These local figures do not establish a whole-project percentage.

Supplementary scheduling control

After all six ordinary native builds completed, eight proof-heavy changed modules were compiled in adjacent base/head pairs with lake env lean --threads=4 --setup ... --json -o ... -i ... -c ... SOURCE, alternating pair order by module. Each compiler invocation was timed independently with GNU time. This is one diagnostic pair per selected module, with warm pinned dependencies and fresh outputs; its summed times cover only this subset and are not a whole-project build result.

Module	Base wall seconds	Head wall seconds	Base user CPU seconds	Head user CPU seconds
Foundations	35.17	30.16	54.34	44.67
Rates	29.58	24.91	47.83	38.72
HarmonicAnalysis	48.08	51.96	73.71	70.47
Hierarchy	33.99	36.20	49.30	42.50
Branching	47.35	42.26	63.79	60.36
Rigidity	55.07	47.54	71.81	60.17
SpectralDecomposition	51.89	54.55	77.05	74.93
Conclusion	88.22	89.84	136.61	134.24

Subset summed wall: 389.35 → 377.42 seconds (3.064% reduction). Subset summed user CPU: 574.44 → 526.06 seconds (8.422% reduction). These figures are not extrapolated to the remaining project modules.

Validation

All local selected-project checks passed:

lake --wfail build LeanPool.MetricCodes.Imports
lake env lean --run /data/codex/scratch/vasilin97/metriccodes-optimize-20261019/Audit.lean --compare /data/codex/scratch/vasilin97/metriccodes-optimize-20261019/base/.lake/build/lib/lean
lake env lean --run /data/codex/scratch/vasilin97/metriccodes-optimize-20261019/Audit.lean /data/codex/scratch/vasilin97/metriccodes-optimize-20261019/final-manifest-compact.jsonl
lake --wfail build +LeanPool
lake env lean --run scripts/ci/lint-project.lean LeanPool.MetricCodes LeanPool.MetricCodes.Binary LeanPool.MetricCodes.Branching LeanPool.MetricCodes.Conclusion LeanPool.MetricCodes.Foundations LeanPool.MetricCodes.HarmonicAnalysis LeanPool.MetricCodes.Hierarchy LeanPool.MetricCodes.HighestWeights LeanPool.MetricCodes.Imports LeanPool.MetricCodes.Interlacing LeanPool.MetricCodes.MatrixPerron LeanPool.MetricCodes.Rates LeanPool.MetricCodes.Representation LeanPool.MetricCodes.Rigidity LeanPool.MetricCodes.RootComplex LeanPool.MetricCodes.SpectralDecomposition LeanPool.MetricCodes.Weyl
lake --wfail exe lint-style LeanPool.MetricCodes.Imports
PYTHONPATH=/data/codex/scratch/lean-pool-optimize-2026-10-19/python python3 -m lean_pool.quality --repo /data/codex/scratch/vasilin97/metriccodes-optimize-20261019/quality-project
PYTHONPATH=/data/codex/scratch/lean-pool-optimize-2026-10-19/python python3 -m lean_pool.indexes --repo /data/codex/scratch/vasilin97/metriccodes-optimize-20261019/quality-project --module --check
git diff b25d6804654bbfd206eb31cdbd6360d1f63d5cd1 HEAD --check

The quality/trust and generated-index checks used an isolated project-only mirror with the unchanged official checkers, repository configuration, selected source, original project card, and audited compiled artifacts. The Mathlib/Batteries declaration linters covered all 17 modules. These are scoped local checks; repository-wide CI and independent review remain required. No CI, lint configuration, waivers, or other projects were modified.

Limits

This is a shared Azure VM, so elapsed-time scheduling varies between runs; all three paired results are reported. A 02:37:35 UTC snapshot showed a one-minute load average of 38.32 on 16 logical CPUs. The native wall-time median is an observation, not a statistically isolated estimate of the effect. GNU time's peak RSS is the maximum resident set of an individual process, not aggregate memory across concurrent Lake jobs. Explicit equation-lemma references may need adjustment in a future definition refactor. The audit intentionally treats every pre-existing private/generated declaration as part of the invariant, which prevented several otherwise valid import/unfolding changes.

Exact Lean environment comparison used for the invariant audit

Build the base and head project separately using the pinned toolchain, save this as Audit.lean, then from the head worktree run lake env lean --run /absolute/path/Audit.lean --compare /absolute/base/worktree/.lake/build/lib/lean. Passing an output filename instead of --compare ... records the compact declaration manifest. The original compiled snapshot was preserved before edits; the final comparison also uses freshly rebuilt head artifacts.

import Lean
open Lean

def selected (name : Name) : Bool :=
  name == `LeanPool.MetricCodes || (`LeanPool.MetricCodes).isPrefixOf name

def declarations (environment : Environment) : Array (Name × Name × ConstantInfo) := Id.run do
  let mut seen : NameSet := {}
  let mut result := #[]
  for (moduleName, data) in environment.header.moduleNames.zip environment.header.moduleData do
    if selected moduleName then
      for name in data.constNames do
        unless seen.contains name do
          seen := seen.insert name
          if let some information := environment.find? name then
            result := result.push (name, moduleName, information)
  return result

def kind (information : ConstantInfo) : String :=
  match information with
  | .axiomInfo _ => "axiom"
  | .defnInfo _ => "definition"
  | .thmInfo _ => "theorem"
  | .opaqueInfo _ => "opaque"
  | .quotInfo _ => "quotient"
  | .inductInfo _ => "inductive"
  | .ctorInfo _ => "constructor"
  | .recInfo _ => "recursor"

def sameInformation (before after : ConstantInfo) : Bool :=
  match before, after with
  | .thmInfo left, .thmInfo right =>
    left.toConstantVal == right.toConstantVal && left.all == right.all
  | _, _ => before == after

def manifest (environment : Environment) (path : String) : IO Unit := do
  let output ← IO.FS.Handle.mk path .write
  let rows := declarations environment
  for (name, moduleName, information) in rows do
    let valueHash := match information with
      | .thmInfo _ => Json.null
      | _ => toJson <| information.value? (allowOpaque := true) |>.map (fun value => toString (hash value))
    let safety := match information with
      | .defnInfo value => reprStr value.safety
      | _ => toString information.isUnsafe
    output.putStrLn <| (Json.mkObj [
      ("name", toJson name.toString), ("module", toJson moduleName.toString),
      ("kind", toJson (kind information)),
      ("universes", toJson (information.levelParams.map Name.toString)),
      ("safety", toJson safety), ("type_hash", toJson (toString (hash information.type))),
      ("value_hash", valueHash)]).compress
  IO.println s!"Recorded {rows.size} declarations; compiled snapshots retain full expressions."

def comparison (before after : Environment) : IO UInt32 := do
  let originals := declarations before
  let replacements := declarations after
  let mut current : NameMap ConstantInfo := {}
  for (name, _, information) in replacements do
    current := current.insert name information
  let mut errors := 0
  for (name, _, information) in originals do
    match current.find? name with
    | none =>
      IO.println s!"REMOVED {name}"
      errors := errors + 1
    | some replacement =>
      unless sameInformation information replacement do
        IO.println s!"CHANGED {name}: type={information.type == replacement.type}, universes={information.levelParams == replacement.levelParams}, safety={information.isUnsafe == replacement.isUnsafe}, kind={kind information == kind replacement}"
        errors := errors + 1
      current := current.erase name
  for (name, _) in current do IO.println s!"ADDED {name}"
  IO.println s!"Exact structural audit: {originals.size} base declarations, {replacements.size} head declarations, {current.size} additions, {errors} differences."
  return if errors == 0 then 0 else 1

def main (arguments : List String) : IO UInt32 := do
  initSearchPath (← findSysroot)
  let imports : Array Import := #[{ module := `LeanPool.MetricCodes.Imports }]
  if arguments.head? == some "--compare" then
    let originalPaths ← searchPathRef.get
    searchPathRef.set ((arguments[1]! : System.FilePath) :: originalPaths)
    let before ← importModules imports {}
    searchPathRef.set originalPaths
    let after ← importModules imports {}
    return ← comparison before after
  let environment ← importModules imports {}
  manifest environment arguments[0]!
  return 0

[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 refactor appears mergeable; no actionable issue was found in the changed code.

Summary

This PR reduces proof elaboration work across 14 MetricCodes files. It narrows arithmetic search, reuses existing theorems, and shares repeated arguments about linear maps.

• MetricCodes proofs take less work for Lean to elaborate.

_{Reviews (1) · Last reviewed commit: "Optimize MetricCodes proof elaboration" · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 5,368 tracked declarations across 14 modified files kept their type; only proofs / definition bodies changed.

Also: 5 declarations added, 0 removed. A reorganization moves declarations between files, which shows up here as an add in one file and a remove in another.

➕ Declarations added (5)

• MetricCodes.Spherical.HigherYoungActualGraphAssembly.adjoint_comp_composed_maps — LeanPool/MetricCodes/Branching.lean
• MetricCodes.Spherical.linearMap_comp_sum_comp — LeanPool/MetricCodes/Conclusion.lean
• MetricCodes.centered_square_difference — LeanPool/MetricCodes/Foundations.lean
• MetricCodes.one_sub_centered_square — LeanPool/MetricCodes/Foundations.lean
• MetricCodes.Spherical.adjoint_composition_eq_zero_of_spanning_ranges — LeanPool/MetricCodes/SpectralDecomposition.lean

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: 11,019,346 → 10,301,125 (-718,222, -6.5%). Commands: 8,202 → 8,209.

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

Files: 11 compared — 8 cheaper, 0 costlier, 3 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 disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted to maxHeartbeats units. Failed measurements are not classified as cheaper or costlier. Δ lines counts added/deleted lines from this PR diff.

File	Δ lines	HB base	HB head	Δ HB	Δ HB %	Wall base (s)	Wall head (s)
LeanPool/MetricCodes/Rates.lean	+180/-178	788,391	603,799	-184,592	-23.4%	170.67	84.98
LeanPool/MetricCodes/Foundations.lean	+156/-185	719,636	540,429	-179,208	-24.9%	120.02	77.78
LeanPool/MetricCodes/Hierarchy.lean	+201/-244	640,560	468,174	-172,386	-26.9%	147.61	55.30
LeanPool/MetricCodes/HarmonicAnalysis.lean	+90/-156	1,381,949	1,329,616	-52,332	-3.8%	289.74	132.55
LeanPool/MetricCodes/Branching.lean	+45/-112	1,326,242	1,283,864	-42,378	-3.2%	258.64	129.16
LeanPool/MetricCodes/SpectralDecomposition.lean	+75/-49	1,654,357	1,613,531	-40,825	-2.5%	246.92	134.22
LeanPool/MetricCodes/Binary.lean	+24/-44	610,156	577,785	-32,370	-5.3%	145.13	62.81
LeanPool/MetricCodes/Interlacing.lean	+11/-49	1,099,839	1,082,054	-17,785	-1.6%	172.44	142.96
LeanPool/MetricCodes/Representation.lean	+16/-52	1,150,712	1,154,779	+4,067	+0.4%	245.98	114.84
LeanPool/MetricCodes/HighestWeights.lean	+8/-17	1,016,535	1,016,121	-414	-0.0%	139.42	130.58
LeanPool/MetricCodes/RootComplex.lean	+3/-11	630,971	630,973	+1	+0.0%	139.82	76.22
Total	+809/-1,097	11,019,346	10,301,125	-718,222	-6.5%	2076.4	1141.4

New files — absolute profile

Total heartbeats: — maxHeartbeats units across 0 valid files (91 added LOC).

Sum of lean --profile: — across 0 valid files. Import-excluded time: —.

Count-heartbeats wall-clock total: 0.00 s. Repeated import cost inside lean --profile: —.

Heartbeat values sum disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted from raw allocations to maxHeartbeats units by dividing by 1000. They include command elaboration and kernel checking, exclude imports, and include profiler overhead; they are not comparable to the deprecated linter's totals. 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)	Commands	Errors
LeanPool/MetricCodes/Conclusion.lean	57	—	—	—	—	—	1151	1
LeanPool/MetricCodes/Rigidity.lean	20	—	—	—	—	—	824	1
LeanPool/MetricCodes/Weyl.lean	14	—	—	—	—	—	596	1
Total	91	—	0.00	—	—	—	2571	3

Aggregate phase totals

Phase	Time
Unavailable	—

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

[Vilin97]

/review

Exact head: 216782909c1daee9b3659094e01b6d94d121c27f.

[Vilin97]

{
"summary": "This MetricCodes refactor replaces broad arithmetic search and duplicated proofs with explicit premises, existing named theorems, and shared adjoint and finite-sum arguments. The spanning-range helper and injective linear-map cancellation make the longer arguments easier to follow while retaining the existing written contracts. The reported 3.811% median wall-time reduction is noisy; the advisory profile has 11 valid file comparisons and does not establish a whole-project speedup.",
"assessment": {
"scope": "Proof elaboration refactor in MetricCodes",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The refactor reduces repeated proof work and unnecessary automation without an actionable maintenance regression."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

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

Reviewed head: 216782909c1daee9b3659094e01b6d94d121c27f

Verdict: ✅ approve

The refactor narrows arithmetic search, reuses existing theorems, and shares adjoint/tensor arguments while retaining readable proof structure. All 17 project modules compiled from source with pinned dependencies and repository options, without diagnostics. The 11 valid profile comparisons show no material regression. Three files failed profiling on both revisions; head also references a helper absent from the profiler’s base imports. Repository CI remains in progress.

Aspect	Value
Scope	proof elaboration optimization and helper extraction
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The refactor makes proof dependencies more explicit and removes duplicated arguments without introducing actionable maintenance debt.

---

Tokens: 10,324,684 in / 21,859 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $41.6266 (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.

CI was not green for this commit at review time; this review does not replace CI.