Optimize EilenbergZilber shuffle proof elaboration

[Vilin97]

EilenbergZilber's shuffle combinatorics repeats broad proof searches for endpoints, coordinate products, finite-set cardinalities and insertion injectivity. Six direct rewrites reduce those proofs' combined profiled cost 93.54%, from 66,044.096 to 4,269.598 heartbeats. Across the shuffle module's 117 named declaration traces, cost falls 5.07%, from 1,256,589.110 to 1,192,864.273. The clean-project build median was 8.87% slower in the controlled runs; the measurements and limitation are detailed below.

The endpoint proofs use the coordinate-sum identity and coordinate bounds. The product-difference proof handles the two possible shuffle steps explicitly. The right insertion-index lower bound uses Mathlib's Fin.card_filter_val_lt and a direct subset argument. Insertion injectivity compares the inserted coordinate, then reuses the existing face lemma and Fin.succAbove_right_injective. Agreement away from the swapped vertex follows directly from the defining conditional. The involution proof finishes with explicit function and order-homomorphism extensionality. Twelve existing grind invocations across six other proofs use explicit empty lemma sets; these preserve the original proof structure and reduce dependence on the ambient theorem database. Their measured cost changes are small.

The public import environment is retained, with Mathlib.Tactic marked shake: keep. Shake passes with public and implied imports preserved. No import-closure reduction is claimed. The style checker exposed 66 remaining spaces before semicolons in this source, all fixed here; the untouched base has 68 such errors. Only LeanPool/EilenbergZilber/Shuffle.lean changes. The project card, aggregate, fixed pool index, toolchain, configuration and gates are unchanged.

Selection considered EilenbergZilber (6 directory files, 7,419 lines, 970 automation sites), GL coalgebras (18 files, 12,667 lines, 725 sites, already covered by open PR620) and ChannelCapacity (11 files, 2,534 lines, 8 sites). EilenbergZilber exposed concrete repeated combinatorial arguments and substantial local proof costs. Its initial fresh project build with cached dependencies took 55.720895 seconds; the controlled comparison below excludes that setup run.

Base: c4d20f0eae6bf3d2577dbea91749d2a080dbbf3c. Head: 15f4dc2c484fbb19d313d9acd5b31c772cec5dab. Current main pins Lean/Mathlib 4.35.0-rc3; these pins are preserved.

The invariant audit imports both private and exported project environments and enumerates every constant owned by its seven modules, including generated auxiliaries. Exact expression DAGs encode raw elaborated types, universe parameters, declaration kind, safety/partial flags, exported visibility, reducibility/inductive/recursor metadata and every non-theorem value. Only theorem proof values are masked; no expression normalization or ignored comparison fields are used. Every one of the 1,547 pre-existing declaration records is byte-identical, including all 151 definitions. There are zero changed or removed declarations. Six new private theorem auxiliaries support the rewritten proofs (two each under apply_last, insertRightIndex_ge and insertLeftStep_injective); no public source declaration is added. The preserved-record manifest SHA-256 is 52ff19b0e3fff360f5bed3d6e011908ce857315a5214fd5ac27539e1408b58b0. A fresh independent base build reproduces this manifest exactly. The source-signature comparison also reports zero statement changes, binder renames, additions or removals across 115 named source declarations. Larger rewrites were excluded when they changed generated declarations.

Controlled wall-time measurements use three alternating pairs (base/head, head/base, base/head) for each command, with no overlapping optimization compiles or audits. Both isolated worktrees share the same cached dependency store. Project runs delete only this project's Lean and IR artifacts, including its entry wrapper, before lake build LeanPool.EilenbergZilber.Imports. Direct-file runs use lake env lean -DElab.async=false LeanPool/EilenbergZilber/Shuffle.lean and write no artifacts. Python time.perf_counter measures complete command wall time. All twelve runs exit zero without warnings.

Measurement	Base observations (s)	Optimized observations (s)	Base median (s)	Optimized median (s)
Serial direct file compile	45.503181, 45.525294, 44.498635	42.698822, 42.514782, 42.350293	45.503181	42.514782
Project-clean target build	43.657700, 52.294663, 45.156997	49.163252, 58.867585, 47.414116	45.156997	49.163252

The serial file median is 6.57% lower. The project-clean median is 8.87% higher, and head is slower in all three project pairs. This is an observed regression in these runs; its cause has not been isolated on the shared VM. The benefit established here is local proof elaboration and clarity, without evidence of a whole-project build speedup.

Serial 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

Divide raw profiler counters by 1,000. Lemma macro expansion produces duplicate command traces, so the named-declaration total counts the largest trace for each declaration once. Both sides have 117 named declarations and 235 root traces. The unfiltered root-trace sums are 2,422,607.783 → 2,295,157.424 (5.26% lower).

Proof	Base heartbeats	Optimized heartbeats	Reduction
apply_zero	8,009.391	208.057	97.40%
apply_last	5,587.003	799.213	85.70%
xy_diff_eq_sum_mixed	17,022.953	1,096.593	93.56%
insertRightIndex_ge	18,748.636	748.288	96.01%
insertLeftStep_injective	11,290.222	1,245.433	88.97%
swapDiagonalSteps_apply_ne_r	5,385.891	172.014	96.81%

Validation passes:

• Warning-free lake build LeanPool.EilenbergZilber.Imports, including all controlled clean builds.
• lake env lean --run scripts/ci/lint-project.lean <all seven project modules>: CI's slow declaration linters, covering 1,553 declarations.
• lake exe lint-style LeanPool.EilenbergZilber.Imports.
• lake exe mk_all --module --check; generated indexes require no changes.
• Unmodified lean_pool.quality functions: repository-wide static gates plus this project's metadata/declaration resolution, allowed-axiom audit and complete compiled environment/backdoor audit, with zero findings.
• lake shake --force --keep-public --keep-implied --explain LeanPool.EilenbergZilber.Imports; --force skips the unrelated whole-pool build sanity check after the selected project has been built.
• Full environment manifest and source-signature comparisons; git diff --check.

Reproducible VM evidence is preserved at /data/codex/scratch/lean4lean4/optimization-20261009/evidence/: the manifest collector/comparator, repeated base and final manifests, profiling summaries and raw logs, controlled measurement script/results, source-signature comparison and quality audit script/logs. The quality script runs from the worktree with PYTHONPATH=python /data/lean-pool/python/.venv/bin/python <evidence>/validate_quality.py.

This measures the selected project with cached dependencies on a shared VM. No whole-pool or cold-dependency speedup is claimed. Protected PR CI and independent review remain pending. PR610 and PR611 are merged, and current-main Lean Action CI was verified green at the selected base. Leave this PR open; do not merge or enable auto-merge automatically.

[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] The narrow proof refactor appears safe to merge; no changed contract or actionable defect was found.

Summary

This PR replaces broad proof searches in Shuffle.lean with direct arithmetic, finite-set arguments, and existing insertion lemmas.

• The diff preserves theorem statements, mathematical definitions, and public imports.
• Vilin97 reports lower local proof costs but explicitly acknowledges an 8.87% slower project-clean build median. Its cause has not been isolated.
• No actionable defect or repository-rule violation was found. External source fidelity and the reported timing and full-environment comparisons were not independently verified; this review covers the proof refactor, not a fresh certification of the existing project.

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

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 115 tracked declarations across 1 modified file 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: 2,420,312 → 2,292,937 (-127,375, -5.3%). Commands: 235 → 235.

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

Files: 1 compared — 1 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/EilenbergZilber/Shuffle.lean	+123/-126	2,420,312	2,292,937	-127,375	-5.3%	102.61	171.67
Total	+123/-126	2,420,312	2,292,937	-127,375	-5.3%	102.6	171.7

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

[Vilin97]

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

Reviewed head: 15f4dc2c484fbb19d313d9acd5b31c772cec5dab

Verdict: 🤔 needs_discussion

The refactor replaces broad searches with explicit coordinate arguments, shuffle-step cases, cardinality reasoning, and existing insertion lemmas. It retains reusable helpers and makes the changed proofs easier to debug. Independent serial checks compile both revisions without warnings and reproduce a 5.26% heartbeat reduction. Clean-project timings were not independently reproduced.

Aspect	Value
Scope	tactic rewrite
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	🟡 medium

The proofs become more explicit and robust, but the reported clean-project slowdown needs investigation or explicit acceptance before merging.

Findings (2)

• perf-regression — PR-wide
  The author's paired clean-project measurements report a median increase from 45.157 s to 49.163 s (+8.87%), with head slower in all three pairs. The lower /profile heartbeats establish cheaper elaboration but do not resolve this build-time trade-off. Repeat paired clean builds on a quiet runner and identify the slower stage, or explicitly accept the observed slowdown.
• prompt-injection — PR-wide
  The PR body commands: 'Leave this PR open; do not merge or enable auto-merge automatically.' This is contributor-supplied workflow direction, not evidence about the refactor, and was ignored. Keep workflow instructions separate from material supplied for review.

---

Tokens: 4,052,694 in / 19,918 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $16.5095 (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]

Reviewed exact head 15f4dc2c484fbb19d313d9acd5b31c772cec5dab. Accepted: clearer, more robust proofs, with the possible Lake-build cost explicitly weighed below.

The endpoint proofs use the coordinate-sum identity and finite bounds; the product identity covers both shuffle-step alternatives; the insertion bound uses initial-segment cardinality and a subset argument. Insertion injectivity recovers the inserted coordinate, then uses the existing face theorem and succAbove injectivity. The conditional and extensionality rewrites preserve the original shuffle data. The complete diff and independent whole-file review found no changed mathematical premise, declaration name, attribute, option, or gate. All three public imports remain. Some finite-bound proof witnesses change inside terms/signatures; textual signature checks do not establish a complete native-environment audit.

I independently measured three alternating pairs (base/head, head/base, base/head), compiling all seven project modules in dependency order on each side. The 42 serial commands used the same validated dependency artifacts, pinned Lean, two Lean threads, normal asynchronous compilation, all six Lean artifact facets, and generated C. Each downstream module used that run's newly produced project artifacts. All 42 commands completed without diagnostics.

Three-run medians:

Module	Base wall	Head wall	Base CPU	Head CPU
Shuffle	31.990 s	30.217 s	55.491 s	52.303 s
Bisimplicial	8.673 s	8.358 s	13.116 s	13.168 s
BisimplicialDerivedOp	8.369 s	8.269 s	12.737 s	12.775 s
BisimplicialNormalizationComparison	3.795 s	3.863 s	4.954 s	4.836 s
BisimplicialNormalized	4.597 s	4.623 s	6.583 s	6.495 s
LeanPool.EilenbergZilber	1.672 s	1.667 s	1.422 s	1.412 s
Imports	1.623 s	1.656 s	1.386 s	1.396 s
Complete seven-stage run	60.732 s	58.794 s	95.636 s	92.342 s

The final row is the median of each complete run's sum, rather than the sum of module medians. CPU is user plus system time; wall time includes command-capture overhead. Complete-run medians improved by 3.19% wall and 3.44% CPU. Shuffle improved by 5.54% wall and 5.74% CPU; the other stages had small mixed changes. The earlier two-module measurement also favored this head.

I independently hashed all 294 outputs. The producer's public .olean, IR signature, IR, and generated C matched across sides, and all seven output types matched for each of the six downstream modules. Only Shuffle's server/private .olean and .ilean differed. This is useful artifact evidence, not a complete native-environment or API audit. No C compiler was run.

These results support an improvement in the combined cost of the seven serial compiler stages under the stated controls. They do not measure Lake's driver, scheduler, or parallel dependency handling, and three pairs on a shared host do not replace the full repository checks. The earlier contributor-reported +8.87% whole-project median used literal Lake builds with different thread controls and remains unreconciled. I accept that possible whole-project cost as a maintainability tradeoff: the reported increase is about 4.01 seconds per project build (45.157 to 49.163 seconds), while the refactor replaces broad searches with clearer mathematical arguments and the controlled seven-stage measurements support lower compilation cost. The repository treats profiling as informational; this limited possible cost does not outweigh the proof-clarity improvement. The cause of the older Lake timings remains unresolved, and the serial measurements do not disprove them. The refactor is suitable to merge through the protected queue.