RootSystem: supply interval bounds directly in the pairing proof

[Vilin97]

An.pairing_formula finishes by searching the library for premises even though the missing facts are just the two signed intervals' endpoint bounds. Supply those bounds directly in a small auxiliary proof and finish with grind only [Fin.le_def, Fin.lt_def]. The median clean project rebuild falls from 93.179 s to 27.930 s (70.03%).

This optimizes exactly one existing project, RootSystem. Available VM source captures attributed 83.313 s to its 863 lines, including 67.636 s to An.pairing_formula. Larger candidates included GrothendieckVanishing, KaltonRoberts, and MassFormula; RootSystem offered a concentrated bottleneck in one proof with a small audit scope. No mathematics is deleted, and imports, definitions, statements, instances, namespaces, the project card, and generated indexes remain unchanged.

Base: 26ce45d3871e5560a8baffa4d49a8942b1d20a24 (re-fetched and verified immediately before commit).
Head: b84ddb316ea730faa4d702db731453c5171f20c0.
The live repository pins Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e; both are unchanged.

An out-of-tree Lean environment inspector recorded the base before editing and re-imported all four project modules with importAll := true after rebuilding. It serializes fully elaborated expression graphs, including binder names/annotations and universe levels, and compares names, owning modules, universes, safety/partial flags, declaration kinds, definition bodies/reducibility hints, and inductive/constructor/recursor metadata. Only theorem proof bodies and nonsemantic expression metadata are excluded. All 435 pre-existing declarations match, including private generated proofs; no declaration is missing or changed. There is one new private auxiliary theorem proving the two interval bounds. The as_aux_lemma packaging preserves the existing generated proof declaration. The repository's textual statement comparison also finds zero changed, renamed, added, or removed named declarations.

Each controlled run deleted only the four project's local Lean/IR build outputs, kept dependency caches fixed, and timed lake build LeanPool.RootSystem.Imports with Python's monotonic perf_counter. All runs used the native repository options on the shared Azure VM.

Project rebuild	Run 1 (s)	Run 2 (s)	Run 3 (s)	Median (s)
Base	96.241	87.361	93.179	93.179
Head	31.951	27.287	27.930	27.930

Successful synchronous command profiles report 89,368.565 → 72,431.000 heartbeats for pairing_formula (18.95% fewer; raw allocation counts 89,368,565 → 72,431,000). The instrumented source-prefix wall times were 154.112 → 30.408 s. The prefix contains the original imports, definitions, and proofs through pairing_formula, followed by end An, and uses the native module setup with Elab.async=false and command heartbeat tracing. Full-file synchronous tracing reaches existing heartbeat limits in the unchanged pairing_symm and An_is_reduced; no limits were raised. The full native project builds pass. Instrumented prefix times are separate from project rebuild measurements, and shared VM load can affect wall time.

Validation:

• Three warning-free clean builds: lake build LeanPool.RootSystem.Imports.
• lake env lean --run scripts/ci/lint-project.lean LeanPool.RootSystem LeanPool.RootSystem.An LeanPool.RootSystem.BCn LeanPool.RootSystem.Imports: passed for all 436 declarations, including slow linters.
• lake exe lint-style LeanPool.RootSystem.Imports: passed.
• A project-scoped harness calls the unmodified lean_pool.quality checks for all four files and the existing YAML card: headers, forbidden code/options, file/proof sizes, metadata/declaration/card validation, axioms, and compiled option-backdoor audit all pass.
• A separate Lean axiom walk covers all 436 declarations, including private helpers, and permits only Classical.choice, propext, and Quot.sound.
• lake exe mk_all --module --check, lake shake --force --keep-public LeanPool.RootSystem.Imports, and git diff --check: passed. Shake proposes no import changes with the public dependency surface preserved; --force bypasses its unrelated whole-pool build sanity check after the selected project has been built.
• Final structural declaration manifest comparison: 435 unchanged, zero missing, one supporting private theorem added.

Full-precision measurements, manifests, inspector scripts, and validation logs are retained on the VM at /data/codex/scratch/vasilin97/optimization-20261014/, outside the content PR. Dependency fan-out is unchanged. Repository gates and configurations are unchanged. This PR is for independent review and normal protected CI; no merge or auto-merge is requested.

[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] No blocking defect was found in this proof-only change.

Summary

An.pairing_formula now supplies both intervals' endpoint bounds before finishing with grind only [Fin.le_def, Fin.lt_def].

• The interval pairing proof uses supplied bounds and a narrower search.

_{Reviews (1) · Last reviewed commit: "Optimize RootSystem interval pairing pro..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "At b84ddb3, An.pairing_formula now supplies the two endpoint-order facts directly from SignedInterval.hij, retains its existing intermediate proof, and replaces final library-suggestion search with grind only [Fin.le_def, Fin.lt_def]. Independent source and integration audits found no changed mathematical interface or new assumption. A separate audit of the author's saved measurements supports a median selected-project rebuild of 93.179 to 27.930 seconds and 18.95% fewer profiled heartbeats; these are inspected author-produced data, not fresh reviewer builds. Protected current-head CI and the existing automatic configured review2113 remain separate integration gates.",
"assessment": {
"scope": "single proof tactic rewrite",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "Explicit record bounds and a bounded final tactic improve robustness without removing the argument's structure or changing its public contract."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

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

Reviewed head: b84ddb316ea730faa4d702db731453c5171f20c0

Verdict: ✅ approve

The refactor supplies both intervals’ endpoint bounds explicitly and replaces grind +suggestions with grind only [Fin.le_def, Fin.lt_def]. It preserves the intermediate sum proofs and gives the final step explicit premises and a restricted lemma set, reducing dependence on library search. No maintainability regression was found. No project build was run because this checkout lacks dependency caches; the reported speedup was not independently reproduced.

Aspect	Value
Scope	tactic rewrite
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

Explicit endpoint bounds and a restricted final tactic make the proof easier to diagnose while preserving its existing structure.

---

Tokens: 380,687 in / 4,624 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $1.5921 (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.