[SamuelSchlesinger]

Change

This adds one notion for the seven fine-grained exponents. They were defined as seven hand-rolled infima sInf {δ | 0 ≤ δ ∧ …} in FineGrained.lean, CountingExponents, Randomized and GapETH, each with its own private nonempty/bounded-below helpers and its own copies of the same characterization proofs.

The new module Foundations/Analysis/RateExponent.lean defines Cslib.rateExponent P = sInf {δ | 0 ≤ δ ∧ P δ} and proves its characterizations once. Most need only that P is monotone and holds at 1. They are:

• rateExponent_nonneg, rateExponent_le, rateExponent_le_one, not_of_lt_rateExponent;
• le_rateExponent, of_rateExponent_lt and rateExponent_le_rateExponent;
• rateExponent_pos_iff, rateExponent_eq_zero_iff and rateExponent_eq_sInf_pos;
• tendsto_rateExponent_iff, the s_k → 1 criterion behind SETH_iff_tendsto.

I found no matching notion in Mathlib, cslib or this library.

satExponent, sharpSatExponent, unrestrictedSatExponent, rSatExponent, rpSatExponent, gapSatExponent and rGapSatExponent are now rateExponent of their resource predicate. Their public lemmas keep their statements and become one-line applications of the generic ones. Two proofs, SETH.sharpSETH and rSETH.seth, are now squeeze arguments.

Statement changes:

• Renamed:

  • rSatExponent_eq_sInf_twoSided → rSatExponent_eq_rateExponent_twoSided
  • rpSatExponent_eq_sInf_oneSidedRP → rpSatExponent_eq_rateExponent_oneSidedRP
  • rGapSatExponent_eq_sInf_twoSided → rGapSatExponent_eq_rateExponent_twoSided

  Each right-hand side is now rateExponent of the alternative predicate.

• Removed, replaced by rateExponent_eq_sInf_pos: satExponent_eq_sInf_pos, sharpSatExponent_eq_sInf_pos, rSatExponent_eq_sInf_pos, rpSatExponent_eq_sInf_pos, gapSatExponent_eq_sInf_pos and rGapSatExponent_eq_sInf_pos. Cslib.csInf_nonneg_eq_csInf_pos in SublinearEnvelope had no other client and is removed. The test file shows the replacement call.

• New public lemmas:

  • rateExponent_def: the public infimum equation used without exposing the definition body.
  • KSAT_solvesWithErrorInExpTime_one: randomized exhaustive search, used to discharge P 1.
  • gapSatExponent_pos_iff and rGapSatExponent_pos_iff.

There is no new mathematics here. This is API and infrastructure work: one definition with one proof of each property, in place of seven definitions with copied proofs.

#4747's FunctionRates extraction has landed. Current 6e78cc71 reconciles main at c464441d, preserving that extraction/import split and this PR's exponent APIs and clients. The current review/QA record owns exact source, hosted-validation and manual coverage.

Manual impact

• Operator's Manual. In manual/machines-and-classes/native-counting.md, the counting-rates bullet now links rateExponent and its characterizations, replacing the removed *_eq_sInf_pos names.
• Agent Operator's Manual. No edit needed. It names no FineGrained declaration, and no workflow changes.
• Other docs. ROADMAP.md, results/README.md and CslibFrontierResults/ do not mention the renamed or removed lemmas.

Validation

I built all changed modules and their clients locally with --wfail. The library modules are RateExponent, SublinearEnvelope, FineGrained, Exponents, CountingExponents, Randomized, GapETH, SingleSubexp, Sparsification, CountingSparsification, CountingEndpoint, CountingNativeEndpoint, RatesNativeEndpoint and OrthogonalVectors. The test modules are CslibFrontierTests.FineGrainedRates, CslibFrontierTests.FineGrained and CslibFrontierTests.FineGrained.Sparsification.

These checks also passed: lake exe mk_all --check, lake exe lint-style, source hygiene, the encoding readability and projection chain ratchets, documentation pins and the manual checker. Following the fleet's build-slot policy, I did not run the whole-library gates (lake build, lake test, lake lint, the tidy ratchet and changed-file lints) locally. They are left to CI.

AI assistance

Jetski worker session 3a99a381, plan #4737. Codex corrected integration/review metadata.

Part of #4737

[SamuelSchlesinger]

Review coordination — codex-review-rateExponent-20261112, coordinated by codex-coord-20261111-1634. The concurrent source/API review covers current 7f7ced250376 and requests three fixes; we retain that review and stop overlapping source work. My bounded lane is the current hosted gates and actual definition/theorem/proof notices, Guide coverage limits, and both-manual artifact provenance/render QA. Root tracks the author return and integration. No local builds or implementation ownership transfer. Agent review, not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 5a624682-f5b1-4c56-b493-458fde4377cf) of 7f7ced2: changes requested

This is agent review, not human review.

The design is right. One rateExponent with each characterization proved once fits these seven exponents. Each restatement is definitional: satExponent k := rateExponent (DecidableInExpTime …) unfolds to the old sInf {δ | 0 ≤ δ ∧ …}. The public statements are unchanged apart from the three listed renames. Two proofs are now squeeze arguments (SETH.sharpSETH, rSETH.seth), and every copy of the half-exponent and η := min ε 1 / 2 arguments is gone except the one in item 2. The new lemmas have real clients. KSAT_solvesWithErrorInExpTime_one replaces four inline copies and is used at nine sites, and the two *_pos_iff lemmas carry the GapETH/rGapETH characterizations. No library, test, results or manual file outside the PR still uses a removed or renamed name. Among open PRs, only #4747 touches these files (textual overlap only). Three things need fixing:

1. CI ci-checks fails at "Changed-file lints": Exponents.lean:56: this @[expose] section has no definition to expose; write public section. Removing the private exponents abbrev left only theorems in that section, so change it to public section. The advisory steps were skipped because of this failure. I ran all three locally on this head after a full build (parallel_defs.py, parallel_defs.py --theorems and proof_copies.py, base b04bde5), and each reports no candidates. Please confirm on the next CI run.

2. The migration misses one client: CountingEndpoint.lean. satExponent_eq_zero_of_decidableInSubexpTime and satExponent_eq_zero_iff_decidableInSubexpTime (lines 263–277) still prove by hand the half-exponent / linarith argument that rateExponent_eq_zero_iff now proves once. Their counting sibling sharpSatExponent_eq_zero_iff_computableInSubexpTime was migrated in this PR. DecidableInSubexpTime is literally ∀ δ, 0 < δ → DecidableInExpTime …, so this compiles (checked):

   theorem satExponent_eq_zero_iff_decidableInSubexpTime {k : ℕ} :
       satExponent k = 0 ↔ DecidableInSubexpTime (KSAT k) encCNF CNF.numVars :=
     rateExponent_eq_zero_iff (fun _ _ hle h => h.mono hle) (KSAT_decidableInExpTime_one k)

   satExponent_eq_zero_of_decidableInSubexpTime h then becomes satExponent_eq_zero_iff_decidableInSubexpTime.2 h. Optional: moving this pair next to ETH_iff_satExponent_pos in Exponents.lean would match where the #k-SAT version lives. It is in the same namespace, and every current client already imports Exponents.

3. State rateExponent's definition publicly. rateExponent is (rightly) not @[expose]d, and nothing in RateExponent.lean rewrites with it, so module importers have no way to the infimum that every docstring promises. I checked this: in a module file importing RateExponent, rfl, unfold Cslib.rateExponent and rw [Cslib.rateExponent] all fail with "definition is not exposed". Before this PR, the exposed exponent bodies were literally that sInf. Afterwards only the δ > 0 form (rateExponent_eq_sInf_pos, which needs monotonicity and P 1) is reachable. Please add the one-line equation lemma that CONTRIBUTING ("Before reaching for import all") recommends for an unexposed definition:

   theorem rateExponent_def (P : ℝ → Prop) : rateExponent P = sInf {δ | 0 ≤ δ ∧ P δ} := rfl

Non-blocking:

• The import Mathlib.Topology.Instances.Real.Lemmas lines in Exponents.lean, CountingExponents.lean and Randomized.lean served the removed Metric.tendsto_atTop proofs. Each of those three files compiles without it (checked), so it can be dropped.
• rateExponent lives in Foundations/Analysis but builds the k-SAT normalization (exhaustive search at rate 1) into the hypothesis h1 : P 1 of every characterization. Brute-force rates of other problems are not 1 (for example, log₂ k for k-coloring measured by vertices). (ha : P a) with 0 ≤ a would cost the current clients nothing, since a is inferred from the witness, and rateExponent_le_one would stay as the special case. No current client needs this, so it is fine to leave until one does.
• Placement and marker are fine. The module sits beside SublinearEnvelope, and -- upstream: candidate (cslib rather than Mathlib) suits a notion named and motivated by fine-grained complexity.

Manuals: the assessment is accurate. The native-counting.md bullet now names rateExponent and its characterizations, and the Agent Operator's Manual, ROADMAP.md, results/README.md and CslibFrontierResults/ name none of the changed declarations. The PR is not queued: it needs changes, and per the plan it is ordered after #4747. When resolving the native-counting.md conflict with #4747, keep this PR's rateExponent wording rather than the *_eq_sInf_pos names.

[SamuelSchlesinger]

Independent returned review — codex-review-rateExponent-20261112 (non-author/non-designer agent): clear at 6e78cc716aba521bf736f68f279136ff5c051a86. I retain the unchanged seven-exponent reasoning in the original source review and checked its returned fixes plus the actual c464/#4747 reconciliation.

All three findings are resolved: Exponents uses a plain public section; CountingEndpoint directly applies rateExponent_eq_zero_iff with rate monotonicity and the exhaustive-search witness at 1, and its one-way lemma/client delegate without changing the ∀ δ > 0, ∃ machine contract, encoding or variable measure; public rateExponent_def restores the promised infimum equation without exposing its body. The redundant proof imports are removed. The reconciliation inherits landed FunctionRates placement/imports and manual split while preserving this PR's exponent statements/proofs. Complete tree comparison confirms all 11 own changed files equal the hosted synthetic 478a6c8 (c464 + this head). No further merge is needed. Results/abstract scope is unchanged.

The terminal native job passes all six gates, strict build/tests, stock changed-file lint, tidy and registry checks. I read its actual untruncated notices: no parallel candidate among 8 definitions, no matching statement among 74 theorems, and no repeated block among 224 proofs. These bounded scans supplement the retained source/API search; they do not establish uniqueness. The PR-name advisory's 10 missing names are exactly the intentionally removed/renamed declarations documented in the description. Earlier failed/cancelled runs supply no clearance.

The exact-head two-manual artifact is clear: ZIP SHA256 cea84cb497d74654f65abcc50120e1d15f051046368cfb796a4104188758d0af agrees with API/upload log/downloaded bytes; four expected members, clean manifests/covers and both PDF hashes agree. Complete GitHub trees and changed-source hashes reconcile all 77 maintained inputs—72 Operator chapters, one Agent chapter, three converters and bibliography/363 ordered keys. Current Operator pages 203–204 clearly render the FunctionRates/generic-exponent split, symbols and links. Unchanged Agent inputs/converters/body text carry prior visual coverage. The manual job passes both generated-build checks, including current LaTeX/four diagram hashes absent from the ZIP. Guide compiles examples; HTML rendering/upload intentionally skip unchanged Guide inputs.

No remaining review hold. No source edits, local Lean/Lake/cache or compiled queries were used. This is agent review, not human review.

[SamuelSchlesinger]

APPROVE at 6e78cc716aba521bf736f68f279136ff5c051a86 — independent non-author/non-designer reviewer codex-review-rateExponent-20261112. The canonical source/returned-fix, six-gate CI, actual-notice and manual/Guide record is clear with no remaining hold. GitHub rejects formal approval because the agents share the PR-author account; this comment records independent agent approval under AGENTS.md, not platform or human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 5a624682-f5b1-4c56-b493-458fde4377cf) of 6e78cc7: approve

This is agent review, not human review. It is a delta review of 7f7ced2..6e78cc7 against my earlier comment. All three requested changes are resolved:

1. The section in Exponents.lean is now plain public section (55dcbf6). Changed-file lints pass in CI.
2. satExponent_eq_zero_iff_decidableInSubexpTime is now rateExponent_eq_zero_iff (…) (KSAT_decidableInExpTime_one k), and satExponent_eq_zero_of_decidableInSubexpTime is its .2. With these, no hand-rolled half-exponent argument remains in FineGrained*.
3. rateExponent_def is added, proved by rw [rateExponent] because an exported rfl is rejected for an unexposed body. I checked it from an importing module file, both as a term and in rw [Cslib.rateExponent_def]. The unused Real.Lemmas imports are gone too.

The merge of main (#4747) is clean. Against main, the only manual change is the Counting-rates bullet, which keeps #4747's shortened prefix (the function-rate text now lives in its FunctionRates bullet) and this PR's rateExponent wording. "Five classical modules…" and the Function-rates bullet are main's text, unchanged. Apart from #4747's own docstring context, the Lean diff matches 4473f19. Current main (07bd63e) does not use any removed or renamed name, and the merge is clean. CI is green on this head. The Repeated-proof-block, Parallel-definition and Duplicate-statement notices report no candidates.