[Vilin97]

Incompleteness's term constructions spend 52 s and 56.6 s in two kernel type-checking events around the encoded listMaxDef and nthDef substitutions. This changes only the corresponding proof bodies: unfold the blueprint, explicitly rewrite HierarchySymbol.Semiformula.val_mkSigma and Semiformula.eval_substs, then simplify the resulting evaluation. The explicit equality steps avoid the expensive conversion observed with the original single simp [blueprint].

Selected project: Incompleteness, 184 modules. These two hotspots dominated its declaration profiles and each required about 12 GiB in the original build. No imports, statements, definitions, instances, exported names, project metadata, indexes, toolchain pins, or gates change.

Base: edbe5bd56f476cc2965564676b66199f281ab714
Head: d2be42e0a03f8ebbd081fc388f62e1b224f138f3

The base was fetched again and verified immediately before committing. This uses current main's existing Lean/Mathlib 4.35.0-rc3 pins.

Invariant audit. Before editing, a Lean environment inspector recorded private module data, fully elaborated expression DAGs for every constant's type and every non-theorem value, universe parameters, declaration kind, safety/partial flags, reducibility hints, and inductive/constructor/recursor metadata. Only theorem proof values and expression source metadata are omitted. The rebuilt head manifest is byte-identical to base: SHA-256 22a3fbdb780054b2a8235bf823640dc08042cc4f388f2fbdcd6435af6c6d8576. Both contain 19,614 inventory rows for 19,605 distinct names; repeated module memberships were checked explicitly. A separate ownership audit confirms coverage of all 19,604 project-owned constants (the inventory also includes one generated imported congruence helper). Zero additions, removals, or differences. A source audit checks all 184 files and permits exactly the two proof-body replacements and explanatory comments.

Controlled measurements. Four sequential clean-project builds in base/head/head/base order, with identical cached dependencies, LEAN_NUM_THREADS=2, and /usr/bin/time -v lake --no-cache build --wfail LeanPool.Incompleteness.Imports. Each run deletes only the selected project's Lean/IR artifacts, verifies its source hashes before/after, and compiles all 184 project modules. No other Lean jobs from this task ran concurrently.

Run	Wall seconds	Maximum child RSS, KiB
Base 1	349.16	12,435,412
Head 1	234.81	1,363,048
Head 2	233.95	1,366,284
Base 2	333.57	12,438,640
Base median	341.365	12,437,026
Head median	234.38	1,364,666

Observed median reductions: 31.34% wall time, 89.03% maximum child RSS. This is a shared Azure VM without CPU isolation or OS cache flushing; RSS is the largest child's peak, not aggregate simultaneous-process memory. These are project compilation measurements, not a whole-pool benchmark.

Validation.

• Four warning-failing clean builds, plus a final coherent head build with +LeanPool.
• Full declaration manifest comparison and source/ownership audits.
• lake env lean --run scripts/ci/lint-project.lean <all 184 project modules>: passed, 19,604 declarations, including slow Mathlib/Batteries checks.
• lake exe lint-style LeanPool.Incompleteness.Imports: passed.
• Unmodified python -m lean_pool.quality --repo <project-scoped validation view>: passed, including axiom, compiled option/soundness, card, reachability, header and size checks. The view contains all selected sources, its existing card, unchanged pinned configuration and root, and the built artifacts.
• Unmodified generated-index checker on the same view and git diff --check: passed. No generated changes required.
• lake shake --force --keep-public LeanPool.Incompleteness.Imports returns 1 with five pre-existing import advisories. Its output is byte-identical to the recorded base output; those public imports are retained to preserve the API invariant.

Whole-pool CI and independent PR review remain pending. Open for review only; do not enqueue, enable auto-merge, or merge as part of this optimization 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] This proof-only change appears safe to merge.

Summary

Replaces two single-step proofs with explicit rewrites through HierarchySymbol.Semiformula.val_mkSigma and Semiformula.eval_substs, followed by simp.

• Term-construction proofs avoid large kernel reductions.

_{Reviews (1) · Last reviewed commit: "perf(Incompleteness): avoid kernel reduc..." · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

A base→head comparison was attempted but its measurements are unavailable (see the run log); modified files are omitted from the tables below.

Statement changes

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

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.

Total heartbeats: 588,008 maxHeartbeats units across 2 valid files (14 added LOC).

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

Count-heartbeats wall-clock total: 55.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/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Basic.lean	7	326,825	31.70	—	—	—	358	0
LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean	7	261,183	23.30	—	—	—	325	0
Total	14	588,008	55.00	—	—	—	683	0

Aggregate phase totals

Phase	Time
Unavailable	—

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