Reduce Eilenberg–Zilber shuffle proof elaboration work

[Vilin97]

Eight Eilenberg–Zilber shuffle proofs repeatedly invoke conversion or automation for goals already settled by existing lemmas or definitional equality. This change reduces their elaboration work while retaining every pre-existing declaration, including generated auxiliaries.

The selected project is LeanPool.EilenbergZilber. Its central 3,057-line shuffle module took 26s in the initial isolated project build (57.61s total, dependencies cached). I also considered FriezePatterns, KaltonRoberts, and QuasiBorelSpaces from source size/import/tactic evidence; the shuffle module offered a focused set of measurable proof costs shared by the entire project.

Changes:

• Use reflexivity and direct Fin.succAbove_lt_succAbove_iff applications in the inversion-count step comparison.
• Restrict the right/left insertion comparison to simp_all only [Fin.cast].
• Replace eight linear natural-number bound proofs with omega in the vertex-swap and adjacent-step theorems.
• Derive diagonal-swap injectivity directly from the existing coordinate-sum identity and reduce unchanged-vertex evaluation to ite_eq_right.
• Use the existing coordinate positivity lemmas directly in the involution's subtraction cancellation, with an explicit simp list.

The base is 5796b7f6962b59cd891545969a2fa8c0066d1800. Current main pins Lean/Mathlib 4.35.0-rc3; those pins are retained. This PR only changes LeanPool/EilenbergZilber/Shuffle.lean.

Invariant audit:

• Before editing, an out-of-tree Lean inspector imported every project module with importAll := true and extensions disabled. It enumerated module-owned constants, including private/generated declarations, and serialized complete expression DAGs, universe parameters, declaration kinds, safety, reducibility hints, mutual/inductive/recursor metadata, and every non-theorem value.
• The same inspector ran after rebuilding. All 1,553 existing declarations survive. All 166 non-theorem declarations compare exactly, including values. No public name, source signature, universe parameter, or safety level changed. The source-signature checker independently reports 115 unchanged named declarations in the edited module.
• Twenty existing generated theorem types differ only in compiler-generated hygienic bound-variable names; their complete expression DAGs agree after alpha-normalizing those binders. No other type normalization is used. Two generated theorem helpers were added.
• Candidate changes that removed or changed generated helper interfaces were discarded.

Measurements:
Project-clean builds alternate base→head three times in the same isolated checkout. Before each run, only the selected project's .lake/build/lib/lean/LeanPool/EilenbergZilber* and .lake/build/ir/LeanPool/EilenbergZilber* artifacts are removed; pinned dependency artifacts stay cached. Every run uses lake --wfail build LeanPool.EilenbergZilber.Imports and succeeds without warnings.

Wall time (seconds)	Base	Optimized
Pair 1	54.544571	53.415417
Pair 2	52.057287	52.654912
Pair 3	55.283715	50.316823
Median	54.544571	52.654912

The observed median falls 3.46%. The distributions overlap and one pair regresses, so these shared-VM observations do not establish a reliable aggregate wall-time gain. Preliminary standalone base builds were 97.440689s, 78.197403s, and 55.156662s; the paired series addresses that substantial host/time variation.

Declaration profiling uses lake env lean -DElab.async=false -Dtrace.Elab.command=true -Dtrace.profiler=true -Dtrace.profiler.useHeartbeats=true -Dtrace.profiler.threshold=1000000000000000000 LeanPool/EilenbergZilber/Shuffle.lean. Macro expansion can print a declaration twice; aggregate counts retain the largest command trace for each named declaration to avoid counting those traces twice. Values below are raw heartbeat allocations (divide by 1,000 for Lean heartbeat-budget units).

Proof	Base allocations	Optimized allocations	Reduction
insertLeftStep_invCount_term_skip	82,196,365	80,069,832	2.59%
insertRightStep_eq_swap	7,846,963	6,583,051	16.11%
isRightVertex_swap	40,328,437	34,012,281	15.66%
swapDiagonalStepsFun_injective	1,702,355	337,741	80.16%
swapDiagonalSteps_apply_ne	347,436	172,031	50.49%
swapDiagonalSteps_flip_prev	20,507,553	14,981,102	26.95%
swapDiagonalSteps_flip_curr	46,188,994	39,790,663	13.85%
swapDiagonalSteps_involutive	35,427,743	3,467,640	90.21%

Edited proofs: 234,545,846 → 179,414,341 (−23.51%). All named declarations in the module: 1,192,863,316 → 1,137,758,177 (−4.62%). Profile-process wall time was 147.33s → 128.64s; tracing and shared-host load make that secondary evidence.

Validation:

• lake --wfail build LeanPool.EilenbergZilber.Imports with project artifacts cleared for each measured run.
• lake env lean --run <Manifest.lean> <all seven project modules> and complete before/after comparison.
• lake exe runLinter --no-build LeanPool.EilenbergZilber.Imports.
• lake exe lint-style LeanPool.EilenbergZilber.Imports.
• lake exe mk_all --module --check on the full checkout.
• Current main's unmodified python -m lean_pool.quality against a project-scoped validation checkout containing the original Lake config, registry card, entry module, aggregate, all selected sources, and built artifacts. This covers size/header/statement-source rules, metadata, declaration resolution, allowed axioms, and the environment-level option/axiom-injection audit.
• lake shake --force --keep-public --explain LeanPool.EilenbergZilber.Imports; the selected target was already built. The force flag only bypasses shake's whole-library build preflight. Public imports and the existing Mathlib.Tactic -- shake: keep export are retained, so dependency closure is unchanged.
• git diff --check.

The whole pool was not rebuilt locally; full CI and independent refactor review remain required. Wall time on this shared VM is noisy. 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 issue was found in this proof-only refactor.

Summary

Changes eight proofs in Shuffle.lean without changing their statements or the shuffle definitions.

• Shuffle proofs use less elaboration work for the same results.

Review covered the complete diff, supporting definitions, downstream uses, project card, and import boundaries. Builds, profiling, and the generated-declaration audit were not independently repeated. External source and license evidence were not independently verified; this PR leaves those records unchanged.

_{Reviews (1) · Last reviewed commit: "Optimize Eilenberg-Zilber shuffle proof ..." · Reviewed by Greptile}

[Vilin97]

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

Reviewed head: fcb6bc9df22f5ba91f08584a57b4219e5ee6ed0b

Verdict: ✅ approve

The eight proof rewrites replace redundant conversions and search with reflexivity, direct lemma applications, an explicit coordinate-sum calculation, and restricted simp lists. The new omega calls discharge local natural-number bounds while preserving the surrounding case structure. Inspection of the full diff, Shuffle module, and callers found no actionable maintainability regression. The contributor reports lower allocations; I could not independently validate compilation or profiling because fetching pinned Mathlib failed with HTTP 403.

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

The refactor makes proof dependencies more explicit and reduces reliance on automation without sacrificing useful structure or reusable helpers.

---

Tokens: 688,698 in / 4,309 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $2.8194 (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]

{
"review": "Permanent reviewer: independent refactor review",
"reviewed_head": "fcb6bc9df22f5ba91f08584a57b4219e5ee6ed0b",
"summary": "The eight proof changes replace redundant conversion and broad automation with reflexivity, direct coordinate-sum and positivity lemmas, and targeted simplification. The existing case structure remains intact, while the injectivity and involution arguments become easier to follow.",
"assessment": {
"scope": "Targeted proof and tactic refactor",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The explicit replacements reduce dependence on broad automation without removing reusable results or weakening a theorem."
},
"verdict": "approve",
"findings": [],
"coverage": {
"complete_PR_diff": true,
"changed_files": 1,
"patch_hunks": 10,
"root": "Complete one-commit comparison and the affected proof contexts under the current refactor rules.",
"peer": "Independently read the complete 159,695-byte changed module, checked local invariant and positivity providers, and verified that reversing all ten hunks gives the independently pinned 159,915-byte baseline; the forward roundtrip returns the exact current body.",
"generated_environment_audit_repeated": false
},
"evidence": [
"The Fin inversion-count cases use proof irrelevance via rfl and apply succAbove order equivalence directly; their cases and premises are preserved.",
"swapDiagonalStepsFun_injective identifies both indices through the existing coordinate-sum theorem. swapDiagonalSteps_apply_ne applies the definition's unchanged else branch directly.",
"The involution uses proved coordinate positivity to justify natural-number subtraction cancellation. simp_all only [Fin.cast] and simpa only [rm1] restrict simplification; omega replaces only the small natural-number index-bound subproofs.",
"The complete diff changes only the eight lemma proof bodies. No named signature, import, attribute, non-theorem source text, project card, dependency pin or gate is changed."
],
"validation": {
"current_head_LeanCI": {
"run": 38280162448,
"status": "completed",
"conclusion": "success",
"updated_at": "2026-10-12T17:08:53Z"
},
"local_build_or_private_validation_replay": false,
"author_measurements": "The PR reports lower heartbeat allocation and overlapping paired wall times, with one slower pair. Those measurements and the 1,553-declaration compiled manifest were not independently rerun or adopted as this review's evidence.",
"configured_refactor_review": {
"id": 6129037641,
"head": "fcb6bc9df22f5ba91f08584a57b4219e5ee6ed0b",
"verdict": "approve",
"updated_at": "2026-10-12T17:13:50Z",
"body_sha256": "a4b6d2a8247594805afcc96b62614a1951268c4847f03fe0a20d922b13d52113",
"scope": "Independent maintainability review; its unsuccessful dependency download is not adopted as build/profile evidence."
},
"current_main_before_native_enqueue": {
"head": "f482bd7ae78816404abd4ec7d2dff4935c65fdab",
"CI": "SUCCESS",
"at": "2026-10-12T17:37:03.530507+00:00",
"required_checks_refreshed": true,
"rollout610611": "MERGED"
}
},
"disposition": {
"state": "MERGED through the protected native queue",
"configured_review": {
"id": 6129037641,
"head": "fcb6bc9df22f5ba91f08584a57b4219e5ee6ed0b",
"verdict": "approve"
},
"permanent_reviewer_enqueued": true,
"next_action": "No further action for this unchanged reviewed head. Preserve the accepted source and configured review evidence.",
"previous_native_queue": {
"id": "MQE_lQDOSY3yXM8AAAABIAkxI84ABJD4zgM5FaE",
"position": 2,
"state": "AWAITING_CHECKS",
"enqueuedAt": "2026-10-12T17:37:03Z"
},
"merged_at": "2026-10-12T17:53:40Z",
"merge_commit": "b1dbef68836834ad4dc3f6eb9434c87f405f3bf0",
"merge_queue_entry": null,
"merge_group_CI": {
"run": 38285430532,
"head": "b1dbef68836834ad4dc3f6eb9434c87f405f3bf0",
"status": "completed",
"conclusion": "success",
"completed_updated_at": "2026-10-12T17:53:15Z"
}
}
}