[Vilin97]

Several EhrhartVolumeInequality proofs invoke nonlinear normalization or construct a continuous linear equivalence to solve linear arithmetic and injectivity goals. This pass replaces those steps with lighter arithmetic, direct order/cancellation lemmas, and WithLp.ofLp_injective. It changes 42 existing proof blocks across the seven source modules. FourierAnalysis also replaces its private Matrix.Order import with two narrower Mathlib modules and drops two unused local scopes.

The three paired clean-project builds all improved (3.0–4.7% per pair). The median wall time fell 234.42 → 223.40 seconds (4.70%). Median user CPU fell 327.52 → 321.06 seconds (1.97%); maximum RSS was effectively flat (2,005,864 → 2,001,264 KiB, 0.23% lower). The six-hour optimization budget ended without reaching the requested 10% time/RAM target; this PR retains the smaller measured pass. Larger closed-span/L² proof refactors regressed measured builds and are excluded.

Base: edbe5bd56f476cc2965564676b66199f281ab714. Head: 646d9323ad8fed2322617c34904cc9e0cd324c7c. Existing live-main pins are unchanged: Lean v4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e.

Exact invariant audit

Before editing, Lean environment inspection exported all owned constants, including private/compiler-generated declarations. The manifest records names, kind/safety, unfolding hints, universe parameters, exact expression DAGs for types, and exact non-theorem values; only theorem proof bodies are omitted. All 3,578 pre-existing declarations match byte-for-byte, with zero additions, removals, or changed fields. Both manifest SHA-256 values are c0f6fc1715687fb988e9d372b36c6bde31c003bec6502d020042a8dd9118293d. An independent source audit also confirms unchanged signatures/binders and all 499 non-theorem declaration blocks. No definition, instance, statement, public name, metadata card, generated index, or repository gate was changed.

An expanded export additionally compares complete inductive/constructor/recursor metadata, recursor reduction-rule expression DAGs, and mutual-declaration lists. Its base/head manifests are also byte-identical (SHA-256 3cbf556ba21e638e1b594dd54d0c50570267e5821ec5cee0910d2602ae933b02).

Measurement method

Each run removes only this project's compiled facets from .lake/build/lib/lean and .lake/build/ir, retaining the pinned dependency caches. All nine selected modules rebuild. Source hashes are checked before every candidate run. Exact timed command:

/usr/bin/time -v taskset -c 12-15 lake --wfail build LeanPool.EhrhartVolumeInequality.Imports

Alternating pair	Base wall (s)	Head wall (s)	Base max RSS (KiB)	Head max RSS (KiB)
1: base → head	234.42	223.40	2,005,864	1,997,816
2: head → base	222.00	215.25	2,007,792	2,001,264
3: base → head	239.14	230.70	2,004,948	2,001,964

Four-core affinity and alternating order control part of the variation; the VM is shared and cores are not exclusive. GNU time maximum RSS is a process-tree maximum, not summed concurrent memory. These are warm-dependency, cold-project measurements, not a cold Mathlib build or whole-pool timing.

The final synchronous command-profile counter fell 4,691,501.017 → 4,614,251.624 (1.65%). The fixed-point proof fell 20,900.735 → 10,025.365; the uniform inner-ball proof fell 21,366.195 → 11,237.221. Profiles use -DElab.async=false -Dtrace.Elab.command=true -Dtrace.profiler=true -Dtrace.profiler.useHeartbeats=true, with nested trace output suppressed by its diagnostic threshold. Normal timed builds use repository defaults. Profile counters are diagnostic and are not substituted for wall time/RSS.

Validation

• lake --wfail build LeanPool.EhrhartVolumeInequality.Imports passed in all candidate samples.
• Mathlib/Batteries slow declaration linters passed via lake env lean --run scripts/ci/lint-project.lean over all nine project modules.
• lake exe lint-style LeanPool.EhrhartVolumeInequality.Imports passed.
• python3 -m lean_pool.quality --repo <project-only mirror> passed, including compiled trust/backdoor checks; the mirror has the real selected sources, unchanged card and current configuration.
• Independent recursive Lean axiom audit passed for every owned declaration and reachable type/value dependency, allowing only Classical.choice, propext and Quot.sound.
• python3 scripts/project-indexes.py --repo <project-only mirror> --module --check and git diff --check passed.
• lake shake --force --keep-public restricted with --only to all nine project modules passed. Force bypasses the unrelated whole-pool build preflight for this local analysis; no source/configuration waiver was added.

Whole-pool CI and the independent refactor review remain required. Python source was not changed. Raw paired samples, full logs, source hashes, base/head manifests and audit tools are retained on the VM at /data/codex/scratch/researcher/optimization-20261102. No merge, auto-merge or native queue action has been requested; the infrastructure priority hold is preserved.

[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 the proof-only changes; external source fidelity and the reported performance gains remain independently unverified.

Summary

Replaces heavier arithmetic and cancellation proofs across seven existing modules.

• Lean builds the Ehrhart volume inequality modules faster with simpler proof steps.
• FourierAnalysis uses narrower imports and fewer local scopes.

_{Reviews (2) · Last reviewed commit: "Merge current main for EhrhartVolumeIneq..." · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 2,372 tracked declarations across 7 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: 4,013,747 → 3,948,819 (-64,928, -1.6%). Commands: 3,183 → 3,183.

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

Files: 6 compared — 4 cheaper, 0 costlier, 2 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/EhrhartVolumeInequality/Foundations.lean	+15/-15	504,866	479,451	-25,415	-5.0%	112.46	95.56
LeanPool/EhrhartVolumeInequality/Regularization.lean	+12/-14	1,012,868	993,790	-19,078	-1.9%	164.27	203.10
LeanPool/EhrhartVolumeInequality/FourierAnalysis.lean	+11/-10	697,253	689,955	-7,298	-1.0%	135.97	139.76
LeanPool/EhrhartVolumeInequality/Resolvent.lean	+5/-5	1,045,657	1,039,782	-5,875	-0.6%	193.96	171.20
LeanPool/EhrhartVolumeInequality/Convexity.lean	+5/-5	612,288	606,966	-5,322	-0.9%	101.52	114.92
LeanPool/EhrhartVolumeInequality/Convergence.lean	+2/-2	140,815	138,874	-1,941	-1.4%	34.96	33.54
Total	+50/-51	4,013,747	3,948,819	-64,928	-1.6%	743.1	758.1

New files — absolute profile

Total heartbeats: — maxHeartbeats units across 0 valid files (8 added LOC).

Sum of lean --profile: — across 0 valid files. Import-excluded time: —.

Count-heartbeats wall-clock total: 0.00 s. Repeated import cost inside lean --profile: —.

Heartbeat values sum disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted from raw allocations to maxHeartbeats units by dividing by 1000. They include command elaboration and kernel checking, exclude imports, and include profiler overhead; they are not comparable to the deprecated linter's totals. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Commands	Errors
LeanPool/EhrhartVolumeInequality/Variation.lean	8	—	—	—	—	—	629	1
Total	8	—	0.00	—	—	—	629	1

Aggregate phase totals

Phase	Time
Unavailable	—

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

[Vilin97]

Static source assessment: approve the refactor at 646d9323ad8fed2322617c34904cc9e0cd324c7c; full current-head CI remains pending.

The review covered all seven complete file pairs and native patches, with independent reviews of all 42 changed proof commands. Written declaration headers and non-proof definitions retain their scope, apart from the disclosed private-import and local-scope cleanup. The direct arithmetic, cast and injectivity arguments preserve their hypotheses and cases. The removed matrix scopes surround only an unchanged, explicitly typed alias. No mathematical statement is weakened, and project registration, other projects, dependencies and repository controls are unchanged.

The simplifications are reasonable maintenance changes without relying on the author's private benchmark or compiled-manifest claims. The public profile measures six paired files at about 1.6% fewer heartbeats; it does not provide a complete seven-file result. Its Variation.lean measurement reports two Lean diagnostics, at lines 2965 and 3954, in theorem commands that are byte-identical on base and head. Both diagnostics also occur in the same run's base measurement, so this does not establish a refactor regression. The discrepancy with normal compilation remains unresolved.

No change-specific static source finding remains. The advisory profile supplies no required-CI credit. The existing configured review, complete current-head hosted validation and protected native-queue checks must still be reconciled independently; no duplicate review request or queue entry was made.

[Vilin97]

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

Reviewed head: 3f6b4ad33fa31bea7f933e46f3592cc6d36caa25

Verdict: ✅ approve

The refactor replaces heavier arithmetic and normalization tactics with linear arithmetic, direct cancellation lemmas, and WithLp injectivity, preserving intermediate bounds and reusable helpers. Private imports are narrowed without disrupting callers. The refreshed profile reports 1.6% fewer heartbeats across six files; Variation’s measurement failed and detailed logs required authentication. Current-head CI completed its build step successfully, but lint and quality checks remain unfinished. Local compilation was blocked by an HTTP 403 fetching Mathlib.

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

The changes reduce automation dependencies while retaining proof structure and reuse, with no actionable maintenance regression found.

---

Tokens: 1,591,160 in / 11,414 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $6.5358 (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.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Static source continuation at 3f6b4ad33fa31bea7f933e46f3592cc6d36caa25: the reviewed EhrhartVolumeInequality refactor is preserved in the normal merge with current main c1dd32a. I checked all seven complete resulting file bodies against the accepted source and current-main compatibility edits. The import resolution keeps both Complex.LogDeriv and import-all LpSpace.Basic, and retains main’s typed contDiff_apply update. All other projects, registration, toolchain and gate inputs are literal current main. No mathematical statement was weakened. Source assessment remains approve; complete validation and configured review must now be checked on this new head, followed by the protected native queue. The old head’s CI is not credit for this revision. The previous unmergeable queue entry was removed solely to permit this branch repair.

[Vilin97]

/review