[Vilin97]

PointwiseComposition repeatedly elaborates encoded arithmetic formulas and reconstructs the same graph-definability substitutions. This refactor reduces compiler memory and proof elaboration work across five existing modules while preserving the complete declaration API.

The project was selected after recovering the interrupted cycle and checking worktrees, existing optimization PRs, source-review comments and announcement records. It is an approximately 84,000-line, 237-module completed project with a long arithmetic dependency chain. Baseline profiles identified the vector-to-set construction as a memory hotspot and LJ.Derivation.height_rewrite as an expensive proof. Existing optimization PRs and unrelated work are preserved; this PR imports no project.

Changes

• Reuse the existing graph-substitution theorem through one private value-assignment helper. Replace repeated nested finite cases and general simplification with explicit finite cases and definitional equality at twelve application sites.
• Derive the basic arithmetic laws directly from model satisfaction where the elaborated proposition already agrees; use explicit evaluation rewrites for the remaining implication laws.
• Apply named formula-construction result lemmas directly in the two induction proofs. Prove positivity from the successor bound.
• Prove rewrite-height preservation by derivation constructors using congrArg, the induction hypotheses and the cast-height lemma, replacing broad proof search.
• Make the vector blueprint locally irreducible while elaborating its construction. The scope ends immediately afterward. The existing compiled definition body and exported reducibility status remain identical.

lake shake --force --keep-public LeanPool.PointwiseComposition.Imports was inspected. Existing imports and public export coverage are preserved. There are no project-card or index changes, and the fixed LeanPool.lean is untouched.

Declaration invariant

Recorded base: 56e877945082f3dab9f43c8e3d80435118a91446.
Tested head: 25e4cbf.

Before editing, a standalone Lean environment inspector imported LeanPool.PointwiseComposition.Imports with importAll := true and enumerated the owned modules' constNames. It records public, private, generated and meta declarations, including raw elaborated Expr types, universe parameters, safety, declaration kind, reducibility hints, mutual/inductive/constructor/recursor details, and raw non-theorem values. Only theorem proof bodies are excluded. Types and values are compared without normalization or binder renaming.

PASS: all 20,649 original declarations are present and every recorded field is identical. The head has 20,650 declarations; the sole addition is the private graph-values theorem. This includes exact preservation of all 6,198 existing definitions. Source-signature checks report no changed or removed statements. A separate loaded-extension audit confirms identical exported simplifier lemma/unfold/erasure sets and unchanged reducibility for every existing declaration. The existing rewrite equation API is retained.

Raw manifest SHA-256:

• Base: 31ed4f242e3054212a1c5ed92908057e2babe2c7dd294db04c0959c1096557f0
• Head: 1632d9809c2bf13aadee5f6a760f92ad9c9d7b2760626087d6c4ac481f50cd17

Audit programs, source patches, manifests and logs are preserved at /data/lean-pool-optimization/20261102 on the Azure VM. The audit scripts and large raw manifests are outside the content PR.

Measurements

Trial	Source	Wall seconds	User CPU seconds	System CPU seconds	Peak RSS KiB	Major page faults
1	base	390.43	823.16	93.03	1,435,160	33
2	head	400.65	823.83	92.96	1,190,272	8
3	head	398.83	819.61	92.26	1,187,460	29
4	base	389.94	824.53	92.98	1,428,544	9

Median peak compiler RSS: 1,431,852 → 1,188,866 KiB (16.97% lower). This meets the 10% memory target.

Median wall time: 390.19 → 399.74 seconds (2.45% higher). Median total CPU time: 916.85 → 914.33 seconds (0.27% lower). These runs do not establish a compilation-speed improvement.

Each trial removes only this project's lib/lean/LeanPool/PointwiseComposition* and ir/LeanPool/PointwiseComposition* build artifacts, then runs:

/usr/bin/time -v lake --wfail build LeanPool.PointwiseComposition.Imports

Trials use the same VM, pinned dependencies, compiler options, default Lake scheduling and warm filesystem caches, in the predetermined order base, head, head, base. Dependencies remain built. No other profiling or validation from this cycle runs during these trials. Peak RSS is GNU time's maximum individual compiler/child-process high-water mark, not the sum of simultaneous processes. The shared VM has unrelated load, so the wall-time results have that limitation.

Earlier exploratory measurements are retained separately. A pre-vector-optimization pair took 465.24 s / 1,438,256 KiB at base and 468.91 s / 1,442,036 KiB at its intermediate head; it established no project-level gain. An interrupted later series produced a head build with heavy paging (4,878 s wall, 92,115 major page faults). It is excluded from the final comparison. No end-to-end compilation-speed claim is based on that interrupted trial.

Validation

• Four project-clean warning-fatal builds using the command above.
• Mathlib's existing slow declaration linters: lake env lean --run scripts/ci/lint-project.lean with all 237 project modules: 20,650 declarations passed.
• lake exe lint-style LeanPool.PointwiseComposition.Imports
• lake exe mk_all --module --check
• uv run --project python --locked python -m lean_pool.quality --repo . --static-only
• The existing repository quality functions for project-card declaration resolution, public axiom closure (7,515 source declarations), and the compiled option/backdoor audit across all 237 modules: zero errors.
• Full compiled-manifest comparison, source signatures, exported simplifier/reducibility comparison and git diff --check.

The fetched repository already pins Lean/Mathlib 4.35.0-rc3 (Mathlib c55e6e786f49471c72fbddbec5415808896aec1e); those pins are unchanged. Before commit, the recorded base and the selected project's equality with current main were verified. Current main was 112f0c6d57d1e444ef260764f5049760112a2a86 at that check; the selected project, card, toolchain/dependencies and applicable contribution/review rules are identical to the recorded base. The isolated author branch was preserved without rebasing to chase unrelated main changes.

Full repository CI and independent review remain required. This PR is open for review with no auto-merge, queue entry or merge action. The infrastructure priority hold is preserved, and daily documentation publishing is assessed separately from applicable protected validation.

[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 blocking issue was found in this proof-only refactor.

Summary

This refactor reduces repeated proof work across five existing PointwiseComposition modules.

• History evaluation reuses one proof to substitute values into code graphs.
• Formula construction proves its cases with direct result rewrites.
• Peano-minus arithmetic laws use direct model conversions.
• Vector-to-set construction avoids expanding its blueprint during elaboration.
• Term rewrites preserve derivation height through explicit constructor cases.

No actionable issue was found. Existing statements, imports, project metadata, and computation fields are unchanged. This is maintenance of an accepted project, not a new formalization.

Vilin97 explicitly reports the higher wall time and makes no compilation-speed claim. The supplied measurements show lower peak memory, with nearly unchanged CPU time.

The reported memory reduction and raw declaration audits were not independently reproduced. No builds were run during this review, and external source claims were not reverified.

_{Reviews (1) · Last reviewed commit: "Reduce PointwiseComposition compiler mem..." · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

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

Also: 1 declaration 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 (1)

• PointwiseComposition.CategoricalRiceShapiro.Evaluator.definable_code_graph_values — LeanPool/PointwiseComposition/CategoricalRiceShapiro/Evaluator/HistoryEvaluation.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: 3,135,194 → 3,067,622 (-67,572, -2.2%). Commands: 1,399 → 1,406.

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

Files: 5 compared — 3 cheaper, 0 costlier, 2 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/PointwiseComposition/Foundation/FirstOrder/Arithmetic/PeanoMinus/Basic.lean	+29/-15	491,948	454,700	-37,248	-7.6%	28.83	54.03
LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/HFS/Vec.lean	+7/-0	858,220	839,794	-18,426	-2.1%	52.73	109.84
LeanPool/PointwiseComposition/Foundation/FirstOrder/LJ/Basic.lean	+56/-3	134,756	119,246	-15,510	-11.5%	21.17	38.91
LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/Bootstrapping/Syntax/Formula/Basic.lean	+33/-17	1,200,713	1,202,774	+2,061	+0.2%	68.80	127.61
LeanPool/PointwiseComposition/CategoricalRiceShapiro/Evaluator/HistoryEvaluation.lean	+60/-197	449,556	451,108	+1,552	+0.3%	50.49	88.62
Total	+185/-232	3,135,194	3,067,622	-67,572	-2.2%	222.0	419.0

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

[Vilin97]

{
"summary": "Across five existing PointwiseComposition modules, this refactor shares graph-substitution proofs, uses named evaluation results and explicit derivation-constructor arguments, and limits blueprint opacity to one construction. These changes make the proof dependencies clearer and reduce broad proof search. The hosted profile reports five valid comparisons and 2.2% fewer heartbeats; its parallel wall times do not establish a project-wide speed change, and the reported memory reduction was not independently reproduced. This source approval leaves normal CI, current-main validation and protected integration requirements in force.",
"assessment": {
"scope": "proof refactor and local elaboration control",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "The shared valuation helper and explicit evaluation and constructor proofs improve maintenance without an actionable regression in the reviewed source."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

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

Reviewed head: 25e4cbfc8f3382d91bf86e2c95404faad2942d3c

Verdict: ✅ approve

The refactor centralizes graph-value substitution and replaces broad simplification and proof search with named rewrites and explicit constructor cases. Proof dependencies are clearer, and blueprint irreducibility is confined to one construction. The supplied /profile reports 2.2% fewer heartbeats overall; wall-time evidence is inconclusive. A standalone attribute-scoping probe passed on the pinned compiler. Project compilation stopped at missing dependency artifacts, so the memory measurements and declaration audit were not independently reproduced.

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

Explicit proof dependencies and constructor cases make failures easier to localize, with no actionable maintenance regression found.

---

Tokens: 1,788,020 in / 9,537 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $7.2951 (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.