perf(Incompleteness): factor costly definability and frame proofs

[Vilin97]

This refactor reduces proof elaboration work in Incompleteness while preserving the existing mathematical interface. The base has 55,621 lines across 184 modules. It had the largest recorded source-profile total among four larger candidates inspected (327.9 seconds), including a roughly 26-second singleton-sequence proof.

The changes include:

• A private abstract-function definability lemma that avoids unfolding encoded sequence operations during conversion and omits the unused V ⊧ₘ* 𝐈Sg1 hypothesis from the new helper. The existing generated mkSeq₁Def.eq_1 declaration is retained.
• Direct relation, equality, membership and witness arguments in the GL and Grzegorczyk frame proofs.
• Two generic list-boxing inclusion lemmas, reused by both completeness arguments.
• Direct congruence and subformula arguments, explicit finite Peano axiom-set membership, reuse of the canonical-frame relation theorem, named formula recursion equations, a modal duality rewrite, and an explicit simplifier list for quoted derivation projections.
• Thirteen unused private imports removed following lake shake --force --keep-public. Public imports, project metadata and generated indexes are preserved.

Base: a68be5e810692e21ecd16b16759afcf019788dc6. Tested head: 967e8fa8ed450a86a87702a9d7ceeca81a6d80e0.
The repository's existing Lean 4.35.0-rc3, Mathlib c55e6e786f49471c72fbddbec5415808896aec1e, and Tau Ceti 5189e8a380bdf5740cc1fe4123cc9cbe635724c2 pins are preserved.

A Lean environment inspector imports all 184 project modules with importAll := true, extensions disabled, and trust level zero. Its manifest records every declaration's fully elaborated type, universe parameters, safety, name, reducibility hints, all non-theorem values, and inductive/recursor data as structural expression DAGs. Only theorem bodies and source-position metadata are excluded. Comparison by full kernel name preserves all 19,585 unique pre-existing declarations, with 20 new declarations (two generic lemmas and eighteen private proof helpers) and no missing or changed declaration.

The base manifest contains 19,596 module entries because deferred congruence declarations can be cached in multiple module objects. Three cache placements change for ComplementClosedConsistentFinset.congr_simp, FormulaFinset.ComplementaryClosed.congr_simp, and canonicalFrame.congr_simp. Their global declaration identities and fields are unchanged. Separate normal-import client modules compile all three names, and the realized types, universes and safety flags match the original manifest exactly. The raw module-entry comparison is retained alongside the deduplicated declaration audit; existing private auxiliary declarations are also preserved.

The benchmark uses six pairs with counterbalanced order (candidate/base, base/candidate, repeated three times), deleting all Incompleteness artifacts from the local lib/lean and ir build directories before each LEAN_NUM_THREADS=4 lake build LeanPool.Incompleteness.Imports. Dependencies stay cached at the same pinned revisions. GNU time records wall/user/system time and maximum compiler-process RSS. The predeclared primary statistic is median full-project wall time across all six runs per revision; the secondary statistic is median peak compiler RSS. Peak RSS is the maximum compiler-process measurement, not aggregate parallel-build memory.

Pair	Order	Base wall (s)	Candidate wall (s)	Base RSS (KiB)	Candidate RSS (KiB)
1	candidate → base	521.34	467.06	12,431,504	12,429,680
2	base → candidate	460.17	475.31	12,432,444	12,441,008
3	candidate → base	544.94	527.31	12,421,684	12,430,136
4	base → candidate	463.05	543.65	12,425,956	12,416,412
5	candidate → base	680.47	543.71	12,425,212	12,413,864
6	base → candidate	651.01	596.96	12,424,260	12,427,884
Median		533.140	535.480	12,425,584	12,428,782

Observed median full-project wall time: 533.140 → 535.480 seconds (0.4389% increase). Median peak compiler RSS: 12,425,584 → 12,428,782 KiB (0.0257% increase). Median user/system CPU seconds: 694.075/85.215 → 655.745/80.435. Median of the six individual paired wall reductions: 5.7689%.

The 10% full-project wall/RSS target was not reached in this measurement. Median user-CPU time was 5.5225% lower; user-CPU time was lower in all six individual pairs (2.23–7.38%). Whole-project wall and peak-RSS medians increased slightly, with substantial variation on the shared VM.

Separate module measurements isolate the source changes: two opposite-order pairs per module, original module names and Lake setup/options, fresh output directories, the same fixed candidate dependencies, and LEAN_NUM_THREADS=4. The dependencies preserve their existing types and definition values. The direct compiler command was lake env lean --root <snapshot> --setup <module.setup.json> -o <fresh output> <source>. These secondary measurements are separate from the full-project stopping metric.

Isolated module	Base wall (s)	Candidate wall (s)	Wall reduction	Base RSS (KiB)	Candidate RSS (KiB)
HFS.Seq	37.235	11.455	69.24%	5,070,484	970,920
GL.Completeness	6.340	4.665	26.42%	932,986	910,430
Grz.Completeness	11.180	5.870	47.50%	933,714	926,472

Validation on the tested source:

• Selected-project build and warning scans, including all twelve timed clean builds.
• Declaration manifest comparison and normal-import namespace/type checks.
• All slow Mathlib declaration linters through scripts/ci/lint-project.lean over the 184 owned modules; lake exe lint-style LeanPool.Incompleteness.Imports.
• Scoped repository quality checks using the unchanged checker, including the compiled option/backdoor audit; an independent all-declaration axiom audit admitting only Classical.choice, propext, and Quot.sound.
• The unchanged official generated-index checker on the project projection, source-hash checks, and git diff --check.

This VM is shared, and external CPU/memory contention is uncontrolled. The measurements are observations for the stated procedure, not a guarantee of the same percentage on every CI runner. Instrumented source profiles were used to identify proof hotspots; they are excluded from the native timing table. Protected CI and independent review remain required. No merge, auto-merge, or queue entry is requested.

Reproducibility artifacts are retained on the VM at /data/codex/scratch/vilin/optimization-20261016T1208/pass3/: base/head sources, declaration manifests and inspectors, exact commands, source hashes, raw timing data and validation logs.

[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 code issue was identified; merge remains subject to the required independent checks.

Summary

Refactors proofs in Incompleteness without changing existing written theorem statements or mathematical definitions.

• Singleton-sequence definability proofs keep encoded sequence operations abstract.
• GL and Grz completeness proofs use direct relation and list arguments.
• Supporting proofs use direct constructor, congruence, and membership arguments.
• Modules no longer import private dependencies they do not use.

Review limits: builds, declaration audits, and timings were not rerun. The external benchmark artifacts and upstream source/license evidence were not independently verified. No new source or license claim is introduced by this diff.

_{Reviews (1) · Last reviewed commit: "perf(Incompleteness): reuse congruence a..." · Reviewed by Greptile}

[Vilin97]

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

Reviewed head: 967e8fa8ed450a86a87702a9d7ceeca81a6d80e0

Verdict: ✅ approve

This refactor factors singleton-sequence definability, replaces broad automation with explicit arguments and targeted simplification, and shares list-boxing inclusion lemmas between GL and Grz. The changes make proof dependencies clearer and preserve useful structure. No actionable maintenance regression was found. The reported whole-project timings do not establish a speedup; builds and timings were not independently verified because this checkout lacks dependency artifacts.

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

The proofs become easier to trace and less dependent on ambient automation, with no maintenance debt requiring changes before merging.

---

Tokens: 917,113 in / 6,031 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $3.7589 (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": "I reviewed the complete 19-file range at 967e8fa against a68be5e. The refactor replaces broad automation with direct definability, congruence, membership and frame arguments, and shares two list-boxing inclusion lemmas between GL and Grz. The private fixed-zero helper derives unary definability from genuine binary definability without unfolding encoded sequence operations. GL retains boxed persistence and its strict witness; Grz retains the reverse-inclusion equality argument. All 823 existing written theorem/lemma headers, public imports and existing source outside 20 proof rewrites, three new named lemmas and 13 private import removals are unchanged. Independent saved-export comparison preserves all 19,585 original kernel-name records; the three deferred congruence namespace records match base, and 184 modules / 368 saved source files bind to Git. That data check excludes theorem proof values, expression metadata and unrecorded extensions; it is not a compiler rerun. All twelve raw whole-project time files and logs agree with the disclosed median wall time of 533.140 to 535.480 seconds (0.4389% higher) and peak compiler RSS of 12,425,584 to 12,428,782 KiB (0.0257% higher); median user CPU is 5.5225% lower. Isolated module improvements and the paired-wall statistic do not replace the primary metric or establish a causal whole-project speedup. The unmet 10% target is disclosed and is not a repository gate. Configured refactor review 2157 also approves this exact head without findings.",
"assessment": {
"scope": "Proof factoring and targeted tactic rewrites across 19 existing Incompleteness modules",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "Source accepted at 967e8fa: direct proof structure and reusable helpers improve maintenance without an identified mathematical or interface regression. Exact-head ordinary CI, including index/build/lint/style/quality and the canonical Build project gate, is terminal success. Native queue integration and every protected check still apply; daily documentation publishing is asynchronous. No benchmark or compiler validation was rerun for this review."
},
"verdict": "approve",
"findings": []
}