[SamuelSchlesinger]

Part of #4737 (lane time-space-bounds, survey items core-defs F4/F7, timespace F1).

The time and space classes now share one lemma shape for absorbing linear bounds:
X_mono_of_le_mul_add {C} (h : ∀ n, t₁ n ≤ C * t₂ n + C) : X enc t₁ ⊆ X enc t₂. X_mono and
X_mono_of_eventually_le are derived from it. The arithmetic that each class re-derived (the
eventual-to-everywhere bound, the constant-absorption step, the (n + 1) ^ k shift) now lives in
one small module, Foundations/Data/Nat/AffineBound. It imports Init and
Mathlib.Order.Filter.AtTopBot.Basic publicly, and PolynomialBound.Closure and
Mathlib.Data.Finset.Lattice.Fold for proofs only.

This is a refactor. It adds no new mathematics.

Renamed, without aliases. DTIME, TISP, SigmaTwoTIME and SharpTIME already used the
_mono_of_le_mul_add {C} shape, and #4692 calls DTIME_mono_of_le_mul_add (C := …), so the four
odd ones out were renamed to match:

old	new
DSPACE_subset_of_le_mul_add (c d)	DSPACE_mono_of_le_mul_add {C}
NSPACE_subset_of_le_mul_add (c d)	NSPACE_mono_of_le_mul_add {C}
ATIME_subset_of_le_mul_add (c d)	ATIME_mono_of_le_mul_add {C}
ASPACE_subset_of_le_mul_add (c d)	ASPACE_mono_of_le_mul_add {C}

All in-repository callers were updated. No open PR uses the old names; I checked every open PR
diff.

Added.

• NTIME_mono_of_le_mul_add, BPTIME_mono_of_le_mul_add.
• NSPACE_mono.
• ATIME_mono_of_eventually_le, ASPACE_mono_of_eventually_le.
• Nat.exists_le_add_of_eventually_le, Nat.exists_le_mul_add_of_eventually_le,
  Nat.mul_add_le_mul_add_of_le_mul_add, Nat.add_one_pow_le_two_pow_mul_add.

Removed.

• The private exists_add_of_eventually_le and exists_linear_of_eventually_le (Time).
• The private mul_add_le_mul_add (Alternation).
• The private succ_pow_le_two_pow_mul_add (Time/Polynomial).
• The inline re-derivations in Space/Basic and Space/Nondeterministic, in NTIME_succ_pow_eq, and
  in Padding/Polynomial.
• Nat.add_one_pow_le_two_pow_mul_add is derived from the existing
  Nat.mul_add_one_pow_le_two_pow (c = 1), not re-proved. It gives that bound in the
  C * g n + C shape that the class lemmas take.

PPTIME (PP/Time.lean, randomized lane) has PPTIME_mono but no _of_le_mul_add variant. I left
it alone and record it as a follow-up for that lane.

Manuals. I reviewed the Operator's Manual and the Agent Operator's Manual. No manual, the
results inventory or ROADMAP.md names any renamed or added declaration, so neither manual needs
an edit.

Validation. On e1a8624, a local scripts/check.sh fell back to the full check because the
aggregate changed. All six Lean gates passed (lake build, lake test, lake lint,
mk_all --check, lint-style, checkInitImports), as did the Python tooling tests, source
hygiene, both ratchets, documentation pins, the tidy statement ratchet, the result registry and
the changed-file lints. I stopped the run during the last step, the re-elaboration of
cache-restored files, to free a shared build slot. On the follow-up commit 6f52d3f (proof-only:
the power bound and Padding/Polynomial), AffineBound and its importers build with --wfail;
source hygiene and both ratchets pass. Hosted CI provides full validation of the head.

AI disclosure: written by a Jetski agent (worker, session 38db7bed) for Samuel Schlesinger. Agent
review is not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 130c4b0f) of 6f52d3f: approve

This is agent review, not human review. I did not write or design this change.

Reuse. I searched Mathlib for the four AffineBound lemmas and found no existing versions. There is no lemma turning ∀ᶠ n in atTop, f n ≤ g n into ∃ C, ∀ n, f n ≤ g n + C. Mathlib's add_pow_le gives (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n), which is not the C * g n + C shape. Nat.add_one_pow_le_two_pow_mul_add is correctly derived from the existing Nat.mul_add_one_pow_le_two_pow rather than re-proved. A small leaf module is the right home. Nat/Asymptotics is a hub with 25 importers, and the name says what the file contains.

(c d) → {C}. This loses no generality, since C := max c d always works. I checked every caller that passed distinct constants:

• The four space-hierarchy uses (4 0, 2 ^ (k + 1) 1) now read better: (C := 4) with Nat.le_add_right, and the (n + 1) ^ k shift is one named lemma instead of a simpa around mul_add_one_pow_le_two_pow 1 ….
• EXPSPACE/Separation keeps its simp [hG].
• Only the Tests/Alternation example (3 * n + 5) became slightly less direct, needing omega instead of le_rfl. That is an acceptable cost for one shape across DTIME/NTIME/BPTIME/TISP/SigmaTwoTIME/SharpTIME/DSPACE/NSPACE/ATIME/ASPACE.

DTIME_mono_of_le_mul_add moved out of the α : Type section with the same argument order. It is now universe-polymorphic, a harmless generalization.

Declaration preservation. No old names remain anywhere in the tree: library, tests, manual, results or ROADMAP. The same holds for the removed private helpers.

Open PRs. I grepped the diffs of all 61 other open PRs, plus the heads of the two whose diffs GitHub will not serve (#2530, #3268). None use the old names or the removed helpers. #4150 changes Alternation/Savitch.lean without calling the renamed lemmas. #4692 calls DTIME_mono_of_le_mul_add (C := …), which is unchanged. git merge-tree against main and against #4755 is clean, and the merged tree has no old names.

Manuals. I agree no edit to the Operator's Manual or the Agent Operator's Manual is needed. Neither names a changed declaration, and neither do ROADMAP.md, results/README.md or CslibFrontierResults.

CI. ci-checks passed on this head (run 43276277828). The Parallel-definition notice (0 examined), the Duplicate-statement notice (36 theorems) and the Repeated-proof-block notice (86 proofs) are all empty. I also searched by hand: the only re-derivation of the eventual-absorb step left outside this PR's scope is the first follow-up below. The description-names notice (X_mono, X_mono_of_eventually_le) only flags the PR body's placeholder pattern.

Non-blocking:

• PolynomiallyBounded.exists_le_mul_two_pow (Foundations/Data/Nat/PolynomialBound/Exponential.lean) still re-derives the eventual-to-everywhere step with a Finset.range sum. It could now use Nat.exists_le_add_of_eventually_le without an import cycle. That file is outside this PR's class-lemma scope, so it is a follow-up, like PPTIME/PromiseBPTIME.
• The PR body says AffineBound "imports only Init and two Mathlib order files". It also privately imports PolynomialBound.Closure and Mathlib.Data.Finset.Lattice.Fold.
• The Nat lemmas are general mathematics. The marker could name a Mathlib destination, as several sibling Foundations/Data/Nat files do.