[Vilin97]

PLAcceleratedNesterovLean is an existing completed project with 63 modules and roughly 14,200 lines. Its broad scalar-module dependencies and repeated arithmetic searches made it a useful optimization target after the already-merged proof split in #757.

Concrete changes:

• Rebuild the curvature-absorption estimate from square monotonicity, Young's inequality, and explicit multiplication bounds, keeping the three error estimates visible.
• Use explicit arithmetic hypothesis lists in the PŁ Hessian, coercivity, Lyapunov, and convergence proofs; use direct differentiability and homogeneity lemmas where applicable. Remove three unused local Hessian calculations.
• Replace the flat-case arithmetic proof's global simplification and nonlinear searches with signed coefficient bounds and a linear combination of the seven assembly bounds and identities.
• Chain the state-coercivity and bootstrap estimates directly, replacing broad searches with coefficient, square, and induction bounds.
• Prove the scalar lambda/rho identity directly, removing its private dependency on the analytic descent module.
• Narrow private tactic imports in the scalar modules and remove a redundant calculus import. All existing public imports remain unchanged; shake confirms the result.

The live repository pins Lean/Mathlib 4.35.0, which this change preserves. No new project, vendored mathematics, metadata, shared root index, CI configuration, gate, waiver, or heartbeat override is included.

Base: 55b1bad
Head: ace7b6b

The baseline and optimized worktrees use the same pinned dependencies. Before each sample, only the selected project's Lean and IR build outputs were deleted. Every run rebuilt all 63 owned modules, including the public import module, with no warnings. Dependency outputs stayed warm. Runs were ordered base, head, head, base, base, head, with source hashes checked throughout. No other compiler jobs from this cycle ran during timing.

Command: taskset -c 0-7 env LEAN_NUM_THREADS=4 lake build LeanPool.PLAcceleratedNesterovLean.Imports

Sample	Baseline wall seconds	Optimized wall seconds
1	91.93	81.99
2	106.29	85.37
3	95.53	91.88
Median	95.53	85.37

Observed median wall reduction: 10.64%. Aggregate build-process CPU time: 262.73s to 232.65s (11.45% lower). GNU time's largest-child maximum RSS: 1,630,128 to 1,633,532 KiB. This RSS number does not sum parallel compiler processes.

The declaration manifest was captured before editing by importing every owned module into Lean and enumerating its environment constants, including private and generated auxiliaries. It records structural expression DAGs for fully elaborated types and all available non-theorem values, ordered universe parameters, declaration kinds, safety/partial flags, and mutual groups. Binder names/info, universe expressions, and expression metadata are retained. Only theorem proof-body hashes are omitted from the equality test. The original base manifest was reproduced byte for byte after a fresh base build.

Audit result: all 731 existing module records / 722 unique declarations remain present and identical in the audited fields. All 152 existing definition values are identical. 36 existing theorem proof bodies changed. The only addition is one compiler-generated private simplifier theorem supporting the derivative-helper proof; no existing name is replaced.

Manifest SHA256, base: ea7635072486583ff21c380fd8507170605ef830db67c305230cb9adc10a0bb0
Manifest SHA256, head: 01b7b805597909c6149644c08bac5e37ef4b07020bcc4e453af8aa929e994c72

Selected declaration profiles, measured with command-level synchronous heartbeat tracing at the default limit:

Declaration	Baseline heartbeats	Optimized heartbeats	Reduction
muPL_norm_sq_bound	127510.038	76466.177	40.03%
curv_absorption_algebraic	33711.737	12434.308	63.12%
coercivity_core_bound	39158.424	20787.010	46.92%
lyapunov_coercivity_gen	90847.322	21747.475	76.06%
bootstrapTotalDisplacementProof	63214.647	24372.299	61.45%
bootstrapTotalDisplacementGenProof	34181.166	11406.975	66.63%

The baseline flat-case synchronous profile hit the default heartbeat limit and is excluded from ratios; both ordinary builds pass. The optimized flat-case synchronous profile completes at about 12,410 heartbeats. Other failed synchronous profiles are also excluded; the table uses only complete successful paired profiles. No limit was increased. Module-closure inspection also records reductions of 4220 to 3130 for LyapunovContraction.Step3, 3663 to 2413 for Coercivity.Step2, and 3664 to 2417 for Coercivity.Core.

Validation passed:

• Targeted build: lake build LeanPool.PLAcceleratedNesterovLean.Imports, warning-free, repeatedly clean-built in the paired samples.
• Mathlib/Batteries slow declaration linters: lake env lean --run scripts/ci/lint-project.lean with all 63 owned modules, covering 723 declarations.
• lake exe lint-style LeanPool
• lake exe mk_all --module --check
• lake shake --force --keep-public LeanPool.PLAcceleratedNesterovLean.Imports. Force only bypasses the whole-workspace cache precheck; the selected project was already built.
• python -m lean_pool.quality --repo . --static-only, across the repository.
• The unchanged quality implementation's project-card declaration check, axiom audit, and option-backdoor audit for all 63 selected modules.
• Fresh-base manifest reproduction, final base/head manifest comparison, and git diff --check.

Measurements are observations from a shared Azure VM, with warm dependency caches and clean project outputs. They do not measure a cold Mathlib build or guarantee the same wall-time ratio on another machine. The full pool was not rebuilt locally; protected CI and the independent refactor review remain required. This cycle leaves the PR open without requesting merge or auto-merge.

[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 proof and private-import refactor appears safe to merge.

Summary

This PR replaces broad arithmetic searches with explicit bounds and smaller hypothesis lists in PLAcceleratedNesterovLean. It also narrows private imports and uses existing differentiability lemmas.

• Lyapunov contraction proofs use focused arithmetic bounds.
• Coercivity proofs build their estimates from explicit bounds.
• Curvature absorption proofs separate their three error bounds.
• Bootstrap and convergence-rate proofs use direct inequalities.
• Morse–Bott supporting proofs use direct calculus and arithmetic steps.

_{Reviews (1) · Last reviewed commit: "Optimize PLAcceleratedNesterovLean arith..." · Reviewed by Greptile}

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

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

Reviewed head: ace7b6bd3340652281887062e2872f98d9e375ad

Verdict: ✅ approve

The refactor replaces broad arithmetic searches and global simplification with explicit inequality chains, focused tactic inputs, and existing calculus lemmas. It preserves the curvature estimates and bootstrap induction while narrowing private imports and retaining reusable helpers. No actionable maintainability regression was found. Independent compilation and timing checks were blocked by HTTP 403 fetching pinned Mathlib; the /profile comment contains no results.

Aspect	Value
Scope	arithmetic proof rewrites and private import narrowing
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The explicit bounds and restricted automation make these proofs easier to debug and maintain without sacrificing their structure or reusable interfaces.

---

Tokens: 2,635,352 in / 9,097 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $10.6779 (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]

Independent source review of ace7b6bd3340652281887062e2872f98d9e375ad: favorable.

I checked all 16 changed files against the base and the complete 63-module project inventory. The written declaration signatures, definition values and public imports are preserved. The curvature estimate now exposes its three error bounds and sign conditions; the coercivity, flat-case and rate arguments retain their existing hypotheses and conclusions. The direct adjoint differentiability argument and narrower private imports also improve the dependency structure. I found no source change needed.

This is source acceptance for normal protected integration, subject to the applicable validation and current-main gates. I have not independently reproduced the reported timing ratios or inspected private measurement/manifests. The failed informational profile does not itself block this refactor; the configured exact-head refactor review is already favorable.