[Vilin97]

MisereGames has 50 source modules below its project directory (about 18,400 lines), plus its entry module. Existing profiling identified recursive stride and subposition proofs as expensive; there is no competing open MisereGames optimization PR.

Replace depth-eight form_wf search with explicit option/subposition and lexicographic decrease witnesses in the solved-game, stride-addition, birthday and shortness proofs. Replace three aesop proofs with direct move-set identities or option witnesses. The recursive arguments and existing declarations stay in place.

Base: ededf2dc890654488765f9f22dac63af8c047dab. Head: 8db2065187ebe2e82764587cd7ca590ed98b1945. The checkout uses current main's existing Lean/Mathlib 4.35.0-rc3 pins; no toolchain, dependency, CI, gate, waiver, project card or shared index changes.

Before editing, imported LeanPool.MisereGames.Imports with Lean environment inspection at private visibility and serialized every owned constant's full expression graph for its type, universe parameters, declaration kind and safety metadata. Definitions/opaques additionally include their complete values; inductives, constructors and recursors include their structural metadata. Theorems exclude only their proof values. A separate exported-visibility manifest checks the public surface. After rebuilding, sorted records are byte-identical for all 3,918 declarations and all 2,514 exported declarations: no additions, removals or differences. This includes generated/private declarations. Source edits are confined to theorem proofs and their termination proofs.

Manifest SHA-256 digests (identical before/after):

• Private: 23106effc1bb58e197c27dccc41ffb40515032acb9b5ada4afa6534cf385eda2
• Exported: 337148454b6b3ca3895ad2775ba67820d1d966e04ccba36c88ee1364d360399c

Measurements use separate base/head worktrees on the Azure VM, the same pinned prebuilt dependencies and native options, warm dependency/page caches, and deletion of each worktree's private .lake/build before every trial. Each lake build LeanPool.MisereGames.Imports recompiles all 51 owned modules. Trials alternate base/head; wall time uses Python's monotonic clock around /usr/bin/time -v, whose CPU and RSS results are also retained.

Trial	Base wall seconds	Head wall seconds
1	84.333259	81.998285
2	86.765763	73.129397
3	73.813205	70.932946
Median	84.333259	73.129397

Observed median wall time improves 13.2852%. Median user CPU time improves from 132.33 s to 121.65 s (8.0707%). Median maximum child-process RSS is 1,037,236 → 1,033,492 KiB, essentially unchanged; this is not aggregate concurrent memory. The shared VM has scheduling noise, visible in the trial spread; the wall-time percentage is an observation from these trials, not a guaranteed CI speedup.

With lake env lean -DElab.async=false -Dtrace.profiler=true -Dtrace.Elab.command=true -Dtrace.profiler.threshold=100 LeanPool/MisereGames/Misere/Stride.lean, command profiling gives:

Declaration	Base seconds	Head seconds
hasStride_add	6.039500	1.437360
isSolved_of_subposition	1.102066	0.017240
isSolved_add	0.502846	0.068576
isSolved_deadEnd	0.546215	0.011682

Validation:

• Six clean targeted builds succeeded; build logs contain no warnings.
• lake env lean --run scripts/ci/lint-project.lean with all 51 owned modules: passed, 3,917 linted declarations.
• lake exe lint-style LeanPool.MisereGames: passed.
• lake exe mk_all --module --check: passed; no generated changes needed.
• Repository static quality/metadata, project declaration resolution, allowed-axiom and compiled environment backdoor audits: passed.
• Both complete environment-manifest comparisons and git diff --check: passed.
• lake shake --force --keep-public LeanPool.MisereGames.Imports on base and head reports the same two existing suggestions (one public metaprogram import and one private import). Imports are unchanged to keep this PR focused and preserve the exported environment.

Raw manifests, measurement scripts, six build logs, timing files, profiles and validation logs are retained on the VM at /data/codex/scratch/researcher/optimization-20261103T0515/. Full pool builds and protected CI remain the repository's responsibility. Leave this PR open for the independent review and protected validation workflow; auto-merge is disabled.

[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 refactor appears safe to merge, subject to the repository's required validation.

Summary

This PR replaces broad proof search with direct move identities and explicit termination witnesses in five existing MisereGames modules.

• Selected game proofs give Lean direct witnesses instead of searching.

_{Reviews (1) · Last reviewed commit: "Optimize MisereGames recursive proof ela..." · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 293 tracked declarations across 5 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.

Compile cost of modified files — base → head

Heartbeats: 815,687 → 397,181 (-418,506, -51.3%). Commands: 552 → 552.

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

Files: 5 compared — 5 cheaper, 0 costlier, 0 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/MisereGames/Misere/Stride.lean	+14/-4	291,097	92,995	-198,102	-68.1%	37.98	15.16
LeanPool/MisereGames/Form/Birthday.lean	+8/-2	177,901	82,487	-95,413	-53.6%	28.19	12.81
LeanPool/MisereGames/GameForm.lean	+8/-2	151,948	105,616	-46,332	-30.5%	21.19	15.57
LeanPool/MisereGames/Form/Short.lean	+3/-1	109,203	62,925	-46,278	-42.4%	18.31	15.76
LeanPool/MisereGames/Form.lean	+1/-1	85,539	53,158	-32,381	-37.9%	24.76	11.21
Total	+34/-10	815,687	397,181	-418,506	-51.3%	130.4	70.5

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

[Vilin97]

{"summary":"Source review at 8db2065: the nine hunks in five files replace broad proof search with direct move-union/image witnesses and explicit proper-subposition or lexicographic decrease proofs. I checked all ten affected proofs against the unchanged option/subposition and well-foundedness definitions. All 324 written declaration headers, seven termination measures, imports and nonproof commands are retained; no mathematical premise or conclusion was weakened. This improves clarity and reduces dependence on proof search. Source assessment: approve, no findings. Hosted current-head build/lint/style/quality and applicable protected validation remain pending. The private manifest and timing claims were not used as evidence. Preserve NOAUTO and leave the PR open for protected validation; Main's CI hold still applies.","assessment":{"scope":"Existing MisereGames proof and termination refactor","introduces_tech_debt":false,"maintainability":"improved","brittleness":"more_robust","risk":"low","assessment_one_sentence":"Direct relation constructors and move witnesses make the same proofs easier to follow while preserving the original statements and recursion measures."},"verdict":"approve","findings":[]}

[Vilin97]

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

Reviewed head: 8db2065187ebe2e82764587cd7ca590ed98b1945

Verdict: ✅ approve

This replaces selected form_wf and aesop searches with explicit subposition witnesses, lexicographic decreases, and move-set rewrites. The recursive arguments and intermediate proof structure remain readable, and no reusable helpers are removed. The /profile comment reports fewer heartbeats in every changed file, down 51.3% overall. Local elaboration was blocked by missing compiled project imports.

Aspect	Value
Scope	proof-search and termination-proof rewrite
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The explicit witnesses reduce proof-search dependence and make termination arguments easier to inspect without sacrificing proof structure or reuse.

---

Tokens: 603,197 in / 5,661 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $2.4977 (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.