[Vilin97]

KaltonRoberts' epsilon case-two spine proof asks library suggestions to rediscover that a certificate's negative mass is nonnegative. Supply the existing DualCertificate.negMass_nonneg lemma to grind explicitly. Retain grind so the original generated proof helpers remain present. This changes one proof-body line in PipelineEps.lean.

Selected from the exact-source historical profile: this 19-module project used about 317.33 seconds of source elaboration, including 102.216 seconds in this epsilon proof's grind +suggestions call. The profiled file's SHA-256 matches the base source.

Base: edbe5bd56f476cc2965564676b66199f281ab714 (fetched and reverified immediately before commit).
Head: 6cb7fcdb2462b6e317581bac789573355e55eaa7.
The live repository pins Lean/Mathlib v4.35.0-rc3; those pins and all build settings are unchanged.

Invariant audit. Before editing, import LeanPool.KaltonRoberts.Imports with trustLevel := 0, extensions disabled, and private declarations loaded. Enumerate constants by their defining project modules and record raw elaborated Expr representations, universe parameter lists, names, declaration kinds, safety/partial flags, reducibility and inductive/recursor details, and full non-theorem values. Compare the rebuilt head without hashing or pretty-print normalization; only theorem proof bodies are omitted. Repeated export records must agree and their module ownership sets are retained.

Result: 807 unique base declarations → 807 head declarations; zero missing, added, or differing declarations, including private/generated helpers. All non-theorem values and all elaborated types are identical. There are 814 export records before deduplication. No statement, definition, import, card, or generated index changes.

Clean project measurement. One measured pair, fresh project outputs at each revision, dependency oleans retained, identical CPU affinity and command:

taskset -c 12-15 /usr/bin/time -v -o measurement.time \
  lake --wfail build LeanPool.KaltonRoberts.Imports

Measurement	Base	Head
Wall time	855.89 s	417.05 s
User + system CPU	480.47 s	343.65 s
Peak compiler RSS	2,899,236 KiB	2,925,852 KiB

Observed wall time decreased 51.27% and CPU time 28.48%; RSS increased 0.92%. GNU time reports the largest descendant-process RSS, not summed concurrent memory. Both builds compiled all 19 project modules with dependencies cached. The changed epsilon module took 338 → 21 seconds in the build logs.

The VM is shared and heavily loaded, so the wall-time difference includes scheduling variation: the unchanged Pipeline module also varied, 274 → 188 seconds. The CPU reduction corroborates the optimization; this is not an isolated-host or statistical benchmark. The ordinary spine's search remains and continues to dominate peak RSS.

Validation at the final source:

• Warning-free clean lake --wfail build LeanPool.KaltonRoberts.Imports.
• lake exe runLinter --no-build LeanPool.KaltonRoberts.Imports.
• lake exe lint-style LeanPool.KaltonRoberts.Imports.
• lake exe mk_all --module --check.
• Full repository static quality checker: PYTHONPATH=python python3 -m lean_pool.quality --repo . --static-only.
• Existing quality-checker card-resolution, allowed-axiom, and environment-backdoor audits scoped to all 19 project modules: zero findings.
• Full raw declaration-manifest comparison and an additional Lean --profile run of PipelineEps.lean.
• git diff --check; only this project's proof file is committed.

lake shake --keep-public was attempted read-only; its initial workspace sanity check required unrelated, unbuilt pool modules. No import edits were made. Whole-pool compilation and remote protected checks/review remain CI responsibilities. This PR does not merge, enqueue, or enable auto-merge; current-main validation has not been certified green, so the infrastructure hold is preserved.

The manifest generator/comparator, raw manifests, benchmark harness, exact commands, logs, and measurements are retained on the VM under /data/codex/scratch/researcher/optimization-kalton-roberts-20261102/.

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 3 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: 446,046 → 441,008 (-5,038, -1.1%). Commands: 20 → 20.

Per-file wall sum: 140.7 s → 37.1 s (-73.6%). 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/KaltonRoberts/PipelineEps.lean	+1/-1	446,046	441,008	-5,038	-1.1%	140.68	37.15
Total	+1/-1	446,046	441,008	-5,038	-1.1%	140.7	37.1

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

[Vilin97]

Source assessment at 6cb7fcd: approve.

The complete diff changes one proof-body line. It supplies the existing DualCertificate.negMass_nonneg theorem to grind in the precise 0 ≤ cert.negMass goal, replacing broad suggestion search. That theorem proves nonnegativity directly from the sum of nonnegative negative parts. Statements, assumptions, computational definitions, imports and other files remain unchanged; retaining grind also avoids an unnecessary generated-proof-helper change.

The public profile reports a small deterministic heartbeat reduction (446,046 → 441,008) and lower measured wall time. The author's larger whole-project timings and declaration-manifest checks remain attributed evidence; I have not inspected private artifacts or reproduced those measurements.

This is a clear, bounded maintenance improvement. Current-head configured review and authored CI are still pending, and current-main qualification plus normal protected native-queue validation remain required.

[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 one-line proof optimization appears safe to merge, subject to the existing required checks.

Summary

Replaces library suggestion search in spine_case2_eps with the existing DualCertificate.negMass_nonneg lemma.

• The epsilon case-two proof gives grind the nonnegativity fact directly.

_{Reviews (1) · Last reviewed commit: "perf(KaltonRoberts): avoid library searc..." · Reviewed by Greptile}

[Vilin97]

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

Reviewed head: 6cb7fcdb2462b6e317581bac789573355e55eaa7

Verdict: ✅ approve

The one-line rewrite supplies the existing nonnegativity lemma explicitly to grind, removing library suggestion search while preserving the surrounding proof structure and callers. This makes the dependency clearer and reduces search brittleness. The supplied /profile report shows 1.1% fewer heartbeats and lower wall time. Independent elaboration was blocked by missing project/dependency oleans in this checkout.

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

Making the required lemma explicit improves maintainability without introducing actionable technical debt.

---

Tokens: 300,454 in / 2,083 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $1.2331 (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.