[SamuelSchlesinger]

Change

This moves the parameterized function-time tower out of FineGrained/CountingExponents.lean into a new module, FineGrained/FunctionRates.lean. The tower covers ComputableInTimeO, ComputableInExpTime and ComputableInSubexpTime, their FTIME and decision bridges, and their reduction transfers. The moved code is unchanged, and no declaration is renamed or restated.

The tower is generic and has nothing to do with #k-SAT. Before this change, a client that needed only function rates had to import the whole counting module. That module pulls in sparsification and counting-tree machinery. Randomized.lean (and through it GapETH.lean) now imports FunctionRates and Exponents directly instead of CountingExponents. CountingExponents re-exports FunctionRates through a public import, so existing importers, including SingleSubexp and the files owned by other open PRs, compile unchanged.

• Lines: +365/−320 (net +45). That covers the new file's header and docstring, the narrower CountingExponents docstring and the manual split. No proof copies are added or removed; this is a pure move.
• Randomized's docstring chain no longer mentions sharpSatExponent, which that module never proved anything about.

Manual impact

• Operator's Manual. manual/machines-and-classes/native-counting.md now lists FunctionRates as its own bullet ("Function rates"), and the module count in the section intro goes from four to five. The CountingExponents bullet keeps only the counting content.
• Agent Operator's Manual. No edit needed. It names no FineGrained module or declaration, and no workflow changes.
• Other docs. ROADMAP.md, results/README.md and CslibFrontierResults/ do not mention the moved declarations or CountingExponents.

Validation

Local scripts/check.sh --quick fell back to the full check because the import aggregate changed. Every Lean gate and audit passed: lake build, lake test, lake lint, lint-style, checkInitImports, mk_all --check, the ratchets, documentation pins, the tidy statement ratchet, result registry references and changed-file lints. I stopped the run during the final step, which re-elaborates outputs restored from the shared cache, to free a shared build slot. CI covers that step.

AI assistance

Jetski worker session 3a99a381, plan #4737.

Part of #4737

[edemaine]

Landed as c464441de4d2adb56f306a3c9326622c80a01329 on 2026-11-12 at 18:51:50 UTC. The FunctionRates extraction and migrated imports are integrated; broader #4737 remains open.

APPROVED at 6685d72f7c540f1b12457590861f064960f90029: final independent source/API/validation/manual review clears the earlier native/notices hold. The guarded helper found that exact head already queued; I made no duplicate queue mutation. No source edit or local Lean/Lake build. Agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer session c48d78b7) of 6685d72: approve

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

Pure move, verified mechanically. Old CountingExponents.lean lines 108–407 (### Parameterized function time bounds through end FunctionMachines) are byte-identical to the new FunctionRates.lean lines 52–351. All 18 declarations keep their statements, proofs, attributes, docstrings and @[expose] (only the three definitions). None is private and none is renamed. Outside that block, CountingExponents changes only its imports and module docstring. Its new docstring and Main results drop exactly the moved entries, and every name listed in FunctionRates' docstring exists there.

Imports and clients. CountingExponents re-exports FunctionRates through public import. Its import closure is therefore unchanged, and SingleSubexp, RatesNativeEndpoint and CslibFrontierTests/FineGrainedRates compile as before. SingleSubexp uses SharpKSAT/SharpETH API, so it rightly keeps that import. Every private import of FunctionRates is used by the moved proofs: Bounds (reduction_add_time_le, two_rpow_le_natCeil_mul_of_le_mul_add), Nat.Power, ResourceFacts, OCombinators and PolyTime.Bounds. Randomized needs only Exponents and FunctionRates; it uses no #k-SAT names. The new import closure drops CountingExponents, Sparsification, CountingTreeBound and Reduction: Randomized goes from 453 to 396 project modules and GapETH from 545 to 490. The docstring edit that removes sharpSatExponent from the Randomized chain is correct, since that module proves nothing about it.

Open PRs. I fetched all 54 other open heads and grepped their changed files for imports of CountingExponents, Randomized, GapETH or FunctionRates, and for the moved names. The only hits are the generated CslibFrontier.lean aggregates, and those are not touched near the new line. None of #4530, #4515, #4150 or #2532 imports these modules or uses the moved names.

Placement and name. A sibling module, rather than an append to the FineGrained hub, follows the topic-module rule. The module keeps each notion together with its FTIME/decision bridges and reduction transfer, which mirrors how Reduction holds the decision-side transfers. FunctionRates matches the manual's "rates" vocabulary and RatesNativeEndpoint, and it avoids a clash with Classes/FunctionTime.

Manuals. The Operator's Manual edit is accurate: it now lists five classical modules (FunctionRates, CountingExponents, SingleSubexp, Randomized, GapETH) plus the RatesNativeEndpoint leaf. FunctionRates imports neither CountingNativeEndpoint nor any counting module, and it does use Bounds. The Agent Operator's Manual needs no edit, since it names no FineGrained module. ROADMAP.md, results/ and CslibFrontierResults/ do not mention the moved names.

Non-blocking nits (fine as a follow-up or not at all):

• CountingExponents still privately imports CslibFrontier.Foundations.Data.Nat.Power and ...MultiTape.Internal.ResourceFacts. Their only users (add_one_pow_le_of_le_mul_pow, ComputableInTimeAndSpace.exists_space_linear/length_le) moved out, and neither module declares attributes, instances or notation. Both are still reachable through FunctionRates, so removing them changes no build graph; it would just be tidier.
• The RatesNativeEndpoint module docstring lists the classical modules as "CountingExponents, SingleSubexp, Randomized, and GapETH". It could add FunctionRates to match the manual's new count of five.

CI and advisory notices. ci-checks, build and guide pass at this head. The Parallel-definition notice (3 examined) and the Duplicate-statement notice (15 examined) are empty. All three Repeated-proof-block candidates pair ComputableInExpTime.ite_polyTime with ComputableInSingleSubexpTime.ite_polyTime or with the two SharpKSAT_length_of_numVars theorems. Every one predates this PR: the detector flags them only because the verbatim-moved proof now sits in a new file. The shared lines are the set L / 1 ≤ L + 1 / 1 ≤ 2 ^ x scalar setup. Folding them into a lemma would be new proof work, outside the scope of a pure move, so these need no action here.

[edemaine]

APPROVE 6685d72f7c540f1b12457590861f064960f90029 — independent non-author agent reviewer-codex-edemaine. The complete five-file refactor is clean; the earlier validation hold is cleared.

The entire 299-line function-rate block is byte-identical, preserving names, statements/proofs, namespace, public visibility and explicit definition exposure. CountingExponents publicly re-exports the new module; no aliases are introduced. I checked the actual randomized promise monotonicity/reduction callers, SingleSubexp bridges and counting clients. Their encodings, existential workspace and single-machine versus rate-family quantifiers remain unchanged. The source import graph confirms that Randomized and GapETH no longer reach CountingExponents/Sparsification; their internal closures shrink by 57 and 55 modules respectively. New placement and preserved credit/upstream marker fit the generic API; the aggregate adds the intended module only.

Current native CI passes all six gates and stock changed-file checks, and Guide examples pass. The tested merge e15ddc84 retains all own module/manual blobs; its aggregate also incorporates incoming main. I read all three actual reports: no parallel candidate among 3 definitions or duplicate among 15 statements; three repeated-block pairs among 151 proofs. Both sides were inspected: they share only the existing 4–5-line real-length/nonnegativity setup before different exponential/single-machine/counting clocks. The moved body is unchanged, and another helper for that setup would add no useful mathematical API. No report is truncated; these scans do not prove uniqueness.

Both-manual QA is clear. Artifact 13971130577 matches API/download ZIP digest, clean exact source, all 72+1 chapters, converters, bibliography/362 keys and both PDF hashes; hosted checks cover generated TeX/diagrams. Operator page 203 (printed 195) readably separates function rates from counting rates and locates their imports. Agent guidance needs no edit because roles/workflows are unchanged; no roadmap, inventory or abstract endpoint changes. No local Lean/Lake build or source edit. Agent review, not human approval.