Optimize GL syntax proof elaboration without changing declarations

[Vilin97]

The syntax layer of Lean4GlCoalgebras repeatedly simplified the full context for finite-set maps and substitution lemmas. This replaces five proofs with explicit induction steps and finite-sum arguments. The five affected proofs' profiled cost falls 69.82%; the syntax module's root-command heartbeat total falls 9.03%. The full clean project measurements show no clear wall-time improvement, so this PR claims a local elaboration improvement.

Changes:

• Use only the closure equations, finite-set map identities and induction hypotheses in the two split-formula closure-map lemmas.
• Replace aesop in single_neg with the negation equations and an explicit conditional split.
• Give not_in_single_voc a constructor-by-constructor argument: absent singleton membership handles atoms, absent union membership handles binary connectives, and the induction hypothesis handles modalities.
• Bound a union sum by adding its nonnegative intersection sum, then apply strict addition monotonicity and the singleton-difference sum identity. This avoids subtraction and broad simplification in Finset.sum_diff_singleton_lt.
• Retain the existing public import environment and mark the public tactic import shake: keep. No import or dependency-closure reduction is claimed. The two pre-existing arithmetic helpers remain unchanged to preserve the API.

Selection: screening considered Lean4GlCoalgebras (18 files under its project directory, 12,667 lines, 610 automation sites) and EilenbergZilber (6 files, 7,419 lines, 212 automation sites). Their initial targeted screening builds took 6.374012s for GL Syntax and 32.487126s for EilenbergZilber Bisimplicial. GL exposed several concrete repeated proof searches in a foundational module, plus duplicated game-history arguments. The latter and the larger map-based rewrites were rejected when they changed or removed generated declarations. This PR retains only changes that pass the strict invariant.

Base: 4eb7c4b2f878b7a49013e7f40215beac7d47a503, re-fetched and verified immediately before commit. Head: f148e6e7a4d479151d89ff566efe243369ae9572. Current main pins Lean/Mathlib 4.35.0-rc3; the pins are unchanged. This existing-project optimization keeps the migrated YAML card, project aggregate and fixed LeanPool.lean unchanged.

Invariant audit: import the base and optimized project environments at both private and exported visibility, enumerate every constant belonging to the project modules, and serialize exact expression DAGs using structural equality. Records include raw elaborated types, universe parameters, declaration kind, safety/partial flags, export membership, reducibility/inductive/recursor details, and complete non-theorem values. Only theorem proof values are masked. All 4,474 records, representing 4,440 unique declarations, are byte-identical: zero changed, removed or added declarations; no normalization or ignored comparison fields was needed. Both manifest files have SHA-256 95ecc03133391dd16be5bbad62cc8abe432b9baa5b24ed9a9acc8f383fd61d02. The repository's source-signature comparison also reports zero statement changes, binder renames, additions or removals across the 78 named declarations in Syntax.

Controlled measurements on the Azure VM: three alternating pairs for direct file compiles (base/head, head/base, base/head). After the scratch experiments ended, two alternating pairs of project-clean builds (base/head, head/base) ran without overlapping scratch compiles. Project runs delete only this project's Lean and IR artifacts, including its entry wrapper; both worktrees use the same cached dependency store. Direct file runs use Elab.async=false and do not write artifacts. Python time.perf_counter measures complete command wall time; all 10 reported runs exit zero without warnings.

Measurement	Base observations (s)	Optimized observations (s)	Base median (s)	Optimized median (s)
lake env lean -DElab.async=false LeanPool/Lean4GlCoalgebras/Logic/Syntax.lean	5.781897, 5.969238, 5.932955	5.580231, 5.743985, 5.642379	5.932955	5.642379
Project-clean lake build LeanPool.Lean4GlCoalgebras.Imports	92.403974, 85.453535	92.430919, 86.698241	88.928754	89.564580

The direct file median is 4.90% lower. Project observations overlap; its optimized median/mean is 0.72% higher, which does not establish a project-wide speedup. This shared VM is not an isolated benchmark host. Deterministic command heartbeats are the stronger evidence for the local improvement.

Serial profiling uses lake env lean -DElab.async=false -Dtrace.Elab.command=true -Dtrace.profiler=true -Dtrace.profiler.useHeartbeats=true -Dtrace.profiler.threshold=1000000000000000000 <source>. Following the repository's profiler convention, divide raw counters by 1000. Syntax has 235 root command traces on each side: 178,811.000 → 162,663.526 standard heartbeat units.

Changed proof	Base heartbeats	Optimized heartbeats	Reduction
FL_SplitFormula_left_eq_FL_Formula_map	2,114.870	657.878	68.89%
FL_SplitFormula_right_eq_FL_Formula_map	1,942.493	550.527	71.66%
single_neg	1,589.151	850.245	46.50%
not_in_single_voc	1,806.911	402.864	77.70%
Finset.sum_diff_singleton_lt	2,642.032	584.999	77.86%
Five-proof total	10,095.457	3,046.513	69.82%

Validation:

• lake build LeanPool.Lean4GlCoalgebras.Imports: warning-free, including two final project-clean builds per side.
• lake env lean --run scripts/ci/lint-project.lean <all 19 project modules>: the CI slow declaration linters pass (4,439 declarations in that linter environment).
• lake exe lint-style LeanPool.Lean4GlCoalgebras.Imports: passes.
• lake exe mk_all --module --check: passes; no generated-index changes required.
• Unmodified lean_pool.quality functions: repository-wide static checks and this project's card/declaration resolution, axiom audit and compiled environment/backdoor audit all pass with zero findings.
• lake shake --force --keep-public --keep-implied --explain LeanPool.Lean4GlCoalgebras.Imports: passes. --force skips the unrelated whole-pool cache sanity check; the selected project was built first. With implied imports removable, shake suggests existing redundant public imports; those are retained.
• Complete environment manifest and source-signature comparisons: pass.
• git diff --check: passes. Only the selected project's Syntax source changes; no gates, settings, waivers or unrelated sources change.

Reproducible VM evidence and scripts are preserved at /data/codex/scratch/vasilin97/optimization-20261008/evidence/ (CompactManifest.lean, compare_manifest.py, measure.py, measure_controlled_project.py, measurements.json, controlled-project-measurements.json, measurement-summary.json, validate_quality.py, and raw logs). The quality script runs with PYTHONPATH=python /data/lean-pool/python/.venv/bin/python <evidence>/validate_quality.py from the optimization worktree.

Limitations: no whole-pool or cold-Mathlib speedup is claimed; normal protected PR CI and independent review remain pending. PR610 and PR611 are merged and current-main Lean Action CI was verified successful. This PR is left 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 risk] Refactors proof tactics in a math library module.

The proof refactor appears safe to merge within its unchanged public contracts.

Summary

Rewrites five proofs in Syntax.lean with narrower simplification, explicit constructor cases, and named finite-sum facts. No actionable issue was found.

• The changed theorem statements, definitions, and import declarations remain unchanged.
• The proof steps follow the existing definitions and preserve the contracts used by callers.
• Vilin97 explicitly retains the public tactic import and two arithmetic helpers for compatibility.
• Vilin97 reports lower local heartbeat counts, not a project-wide wall-time improvement. The benchmarks and compiled-environment comparison were not independently repeated.
• This review covers the existing project's proof refactor. External source fidelity and license provenance were not independently rechecked; neither changes here.

_{Reviews (1) · Last reviewed commit: "Optimize GL syntax proof elaboration wit..." · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 78 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: 177,077 → 160,885 (-16,192, -9.1%). Commands: 235 → 235.

Per-file wall sum: 11.3 s → 15.0 s (+33.5%). 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/Lean4GlCoalgebras/Logic/Syntax.lean	+27/-17	177,077	160,885	-16,192	-9.1%	11.26	15.03
Total	+27/-17	177,077	160,885	-16,192	-9.1%	11.3	15.0

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

[Vilin97]

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

Reviewed head: f148e6e7a4d479151d89ff566efe243369ae9572

Verdict: ✅ approve

The five proof rewrites improve maintainability: restricted simplification replaces broad automation, constructor cases expose the vocabulary argument, and named finite-sum identities clarify the inequality proof. Public imports and helpers remain available. Targeted base/head compiles passed without warnings; matched local profiling reproduced reductions of 69.8% for the changed proofs and 9.0% for Syntax overall. Full-project timings and the environment-manifest audit were not independently rerun.

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

The refactor makes the proofs easier to debug and cheaper to elaborate without introducing actionable maintenance debt.

---

Tokens: 1,332,883 in / 12,871 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $5.5246 (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]

Source review at f148e6e7: five syntax proof refactors

The five rewrites preserve their written contracts and replace broad simplification/search with explicit closure-map identities, constructor cases, and finite-sum facts. The union-sum proof correctly handles overlapping sets using the nonnegative intersection sum; no disjointness premise is added. The unchanged arithmetic helpers and public imports remain available; shake: keep retains the existing tactic import.

Assessment: tactic rewrite; maintainability improved; more robust; low risk; no actionable findings. The complete source comparison is limited to five proof bodies and one import comment. No workflow, gate, or review criterion changes.

The public profile reports lower heartbeat cost. I did not reproduce the benchmarks or compiled-environment invariant audit, and no project-wide wall-time improvement is established.

The current integration review accepts this refactor: exact-head CI is green, the automated review approves it, and the five proof changes improve clarity without an actionable code finding. Proceeding through the normal protected merge queue under the standing maintainer instructions.