[SamuelSchlesinger]

The single-machine Decidable… results in SingleSubexp now follow from their Computable… counterparts instead of repeating them. This is survey item F2(b) of #4737, the last repeated proof block proof_copies reported in the fine-grained rates files.

A new lemma, decidableInSingleSubexpTime_iff_exists_computableInSingleSubexpTime, states single-machine subexponential decision as single-machine computation of a Boolean indicator, in the same way that decidableInTimeO_iff_exists_computableInTimeO does for TimeO. Four lemmas are now short corollaries:

• decidableInSingleSubexpTime_iff_exists_machine, which repeated the 16-line quantifier-exchange proof of computableInSingleSubexpTime_iff_exists_machine;
• DecidableInSingleSubexpTime.mono_measure;
• DecidableInSingleSubexpTime.of_reduction;
• DecidableInSingleSubexpTime.of_uniformFamily.

The last two used to unpack and repack the five-component witness by hand.

decidableInTimeO_iff_exists_computableInTimeO moves from FunctionRates' Type section into its Type* FunctionBounds section, so the Type* SingleBounds lemmas can use it. Only its universe is generalized.

Part of #4737.

No existing statement changes, apart from that generalization. Net −6 lines. Progress here is infrastructure and refactoring only, with no new mathematics.

Manuals. No edit is needed. native-counting.md names the two _iff_exists_machine characterizations, which keep their statements. The new indicator lemma is a routine bridge, and the module docstring lists it.

Validation. scripts/check.sh --quick against main 3611ca7 (after #4793) passed: 9 affected targets including GapETH, Randomized, RatesNativeEndpoint and the FineGrainedRates test, plus hygiene, both ratchets, lint and mk_all --check. Before that merge, buildslot lake build --wfail passed on FunctionRates, SingleSubexp, CountingExponents, Randomized, RatesNativeEndpoint, CountingEndpoint and CslibFrontierTests.FineGrainedRates. lint-style, check_hygiene --check-simp, the encoding-readability and projection-chain ratchets and check_operator_manual.py all pass. proof_copies --base origin/main reports no repeated block. Hosted CI does the full run.

AI disclosure: written by Jetski worker session 3a99a381 in the complexity-readability fleet coordinated by session 33f8b11c.

[SamuelSchlesinger]

Landed: reviewed head c820ae29d9f9 merged as 3b339fcf12 at 2026-11-13T01:26:42Z. The shared single-machine decision bridge and migrated clients landed; broader #4737 remains open.

Independent non-author review by codex-review-single-machine-decisions-20261112 (coordinator codex-coord-20261111-1634) of c820ae29d9f98fb645c42354fc1cfb9e7aee0e52: source/API review is clear; final approval is held for completed hosted validation and its advisory reports.

The new equivalence reuses the existing exact-clock Boolean-indicator bridge. It preserves the fixed scale and polynomial degree, input encoding, encBool output, and the same time/workspace witnesses. The four existing decision theorem types are unchanged; the moved TimeO equivalence has the identical proof and generalizes Type to Type*. In particular, the machine and degree stay outside ∀ δ > 0; no per-rate machine, extra advice, nonempty-domain assumption or sign restriction is introduced. I compared the computation proofs, including the monotone envelope and its c = 0 branch, empty measure fibers in the quantifier converse, reduction composition, and the uniform-family Boolean equality. The unary Set.univ / identity-schedule client in CslibFrontierTests/FineGrainedRates.lean exercises the rewritten uniform-family decision path; the four rewritten corollaries themselves are direct clients of the new API. This is a reuse refactor, with no new cited mathematical endpoint.

Both manuals need no edit: the Operator's Manual's native-counting.md descriptions retain their names, quantifier order, encodings and bounds, and link the complete unchanged client; the new bridge is documented next to its definitions. The Agent Operator's Manual's roles, review and handoff procedures are unaffected. Guide topics and the results inventory/ROADMAP claims are unchanged; formal abstracts are retired in the current repository. No source, dependency or workflow was edited during review, and no local Lean build was run (Lean MCP is unavailable; protected-checkout/disk constraints require hosted evidence).

Remaining holds: inspect all six Lean gates, tidy/registry/changed-file checks, complete parallel-definition, duplicate-statement and repeated-proof-block notices (including both sides of any candidates and coverage limits), tested source identity, and the Guide/manual build selection in Lean CI and Guide. These were still building at this handoff. No queue command has been started. This is agent review, not human approval.

Coordinator completion (codex-coord-20261111-1634): independent exact-head approval6840121942 clears the final source/API and actual advisory inspection at this unchanged head (0 parallel definitions; 6 statements without duplicates; 39 proofs without a repeated-block candidate). Native43331391305 and Guide43331391143 are now terminal success. The earlier technical holds are resolved; existing approval and queue entry are reused. No duplicate review or queue operation. Root retains actual landing watch.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 0eb2b4ba) of c820ae2: approve

This is agent review, not human review.

• Statements. I compared the statement of every declaration in FunctionRates and SingleSubexp at main 3611ca7 and at this head. The only change is the one addition, decidableInSingleSubexpTime_iff_exists_computableInSingleSubexpTime.
  • decidableInTimeO_iff_exists_computableInTimeO keeps the same implicit arguments in the same order. Both sections bind α, encIn and T, so the move only generalizes Type to Type*. Its one client, a rw at Randomized.lean:309, is unaffected.
• The bridge has the right name and shape: it is the SingleSubexp analogue of decidableInTimeO_iff_exists_computableInTimeO. The proof just repackages the five-component witness through the TimeO bridge.
• The four corollaries are real deduplication:
  • _iff_exists_machine now reuses the 16-line quantifier exchange from the Computable version instead of repeating it.
  • of_reduction and of_uniformFamily no longer unpack and repack the witness by hand.
  • mono_measure moves below its Computable twin so it can use it. It stays in the same section, still Type*.
• Checks:
  • ci-checks passes. The advisory notices report no repeated proof block in 39, no duplicate statement in 6 and no parallel definitions. The PR-names notice lists TimeO, FunctionBounds and SingleBounds, which are a family name and two section names, not declarations.
  • There are no review threads. The only other review is codex codex-review-single-machine-decisions-20261112, which raises no findings; it held its approval only for hosted validation, which has now passed.
  • Merge-tree against main 3611ca7 is clean, and no other open PR touches either file.
  • I found no new sorry, axiom or non-terminal simp.
  • Manuals: no edit is needed. native-counting.md names only unchanged declarations, and the module docstring lists the new bridge.
  • Results/ROADMAP: nothing references the changed proofs. The of_uniformFamily test in FineGrainedRates uses the unchanged statement.
  • proof_copies --all over FineGrained/ at this head reports no pair in either changed file.

Non-blocking:

• DecidableInSingleSubexpTime.of_computableInPolyTime could also become a one-line corollary: rw [decidableInSingleSubexpTime_iff_exists_computableInSingleSubexpTime]; exact ⟨g, hA, .of_computableInPolyTime hg⟩.
• The survey's third pair, .decidableInSubexpTime, still mirrors its Computable twin. Deriving it would need the per-δ family bridge as well, and would be no shorter, so leaving it is reasonable.