[SamuelSchlesinger]

Part of #4737 (lane time-space-bounds). This is a follow-up to #4754, suggested in its review.

Change. PolynomiallyBounded.exists_le_mul_two_pow re-derived the eventual-absorption step by hand: a threshold from Filter.eventually_atTop, a sum over the finitely many exceptions, and a case split. It now applies Nat.exists_le_add_of_eventually_le from #4754 to eventually_lt_two_pow and absorbs the additive constant into the multiplier. The statement is unchanged, and the proof-only import Mathlib.Algebra.Order.BigOperators.Group.Finset is replaced by AffineBound, so the change is +10/−10 lines in one file. It is a refactor, with no new mathematics. I found no other proof among the time/space classes that re-derives this absorption step. The other eventually_atTop.mp uses in Classes/ use the threshold itself.

Manual impact. I checked both manuals: neither the Operator's Manual nor the Agent Operator's Manual names this proof, and check_operator_manual.py passes, so no edit is needed.

Validation. On 440ff6e:

• lake build --wfail --iofail passes for the module and all 45 of its direct importers, including the hierarchy, circuit and BigO clients and the tests that import it, with no warnings.
• lake exe lint-style, check_hygiene.py --check-simp, proof_copies.py --base origin/main and check_operator_manual.py pass.

Following the fleet's build-slot policy, I did not run a full local check; hosted CI covers the full validation.

AI assistance. Jetski worker session 38db7bed, plan #4737, for Samuel Schlesinger. Agent review is not human review.

[SamuelSchlesinger]

APPROVE exact 440ff6ee51afd01f0ba392bf0c710427a750aca8 — independent non-author/non-design agent review by coordinator codex-coord-20261111-1634; this is not human review.

The proof now uses the existing eventual-bound lemma instead of rebuilding its finite-exception argument. From p n ≤ 2^n + C and C ≤ C · 2^n, it obtains the unchanged global multiplier C + 1, including n = 0. Names, statements and attributes are unchanged; the replacement import is proof-only and acyclic. I read the resource-bound wrapper and the unary-exponential caller: both retain their API and independent time/space absorption. No additional abstraction or test is needed for this bounded proof refactor.

Current hosted validation passes all six gates, stock lint, tidy/registry and tooling checks. I read the actual notices: 0 definitions, 1 statement and 2 proofs examined, no candidates; these scoped reports supplement source review. The changed file is byte-identical in tested merge 0e17e600. Guide examples pass; HTML is intentionally skipped. Both-manual no-edit assessment is valid: no statement, procedure, excerpt or manual input changes, so no affected rendered page or new PDF artifact is required. No local Lean build was run. All review/dependency holds cleared, and the guarded helper newly queued the exact head.

Landed as d3c8831f at 20:40:12 UTC from the exact approved head. Successful merge-group validation passes all six gates and stock/tidy/registry checks; root verified actual integration. Landing watch for this PR is complete.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 130c4b0f) of 440ff6e: approve

This is agent review, not human review. It covers the one-file change to Foundations/Data/Nat/PolynomialBound/Exponential.lean.

• Proof. It now reads better. The threshold, the Finset sum over the exceptions and the case split are exactly what Nat.exists_le_add_of_eventually_le packages. What remains is the content specific to this lemma: eventually_lt_two_pow, weakened to ≤, then absorbing the additive constant using 1 ≤ 2 ^ n. The line count is unchanged, but the reader no longer has to re-check a finite-exceptions argument. The statement is unchanged. The new module docstring wording matches the proof.
• Import. AffineBound is a plain (proof-only) import, so Exponential's public interface and its importers' interfaces are unchanged.
  • There is no cycle: AffineBound imports PolynomialBound.Closure, Mathlib and Init, and nothing there reaches Exponential.
  • The build-order cost is small. Exponential now builds after Closure and AffineBound, two small modules over Mathlib. Many of its 45 importers, the complexity-class modules among them, already depend on Closure.
  • Dropping Mathlib.Algebra.Order.BigOperators.Group.Finset removes the file's only use of it.
• Reuse. No other copy of this absorption step remains among the class files I checked. The other eventually_atTop.mp uses need the threshold itself.
• Manuals. Neither the Operator's Manual, the Agent Operator's Manual nor results/ names this lemma or module, so I agree that no edit is needed.
• Conflicts. git merge-tree is clean against current main and against refactor(Complexity/Classes): sibling API for time and space classes; reuse existing lemmas #4755, which has since merged. No other open PR touches this file or AffineBound.
• CI and other reviews. ci-checks passed on this head (run 43292463088). The advisory notices found no parallel definitions (0 examined), no duplicate statements (1 examined) and no repeated proof blocks (2 examined). The PR has no inline threads or formal reviews. The one other review comment is the codex-coord-20261111-1634 approval of this same head, and it raises no findings.

Non-blocking (upstream record): the marker still says candidate (addition to Cslib/Foundations/Data/Nat/PolynomialBound.lean). After this change the file depends on AffineBound → PolynomialBound.Closure, which imports PolynomialBound, so upstreaming it literally as an addition to that file would need AffineBound's Closure dependency split off first. The same already holds for the sibling Choose and Log files, which import Closure under the same marker. Read as "belongs with PolynomialBound", the marker is fine. Whoever upstreams this family should either land AffineBound first or keep these as PolynomialBound/* submodules.