[SamuelSchlesinger]

BPL_subset_P carried a reusable fact inside its 113-line proof: a logarithmic-space fair-coin machine's number of accepting coin strings can be computed exactly in polynomial time. This PR names that fact and simplifies its proof.

• New: Turing.MultiTapePTM.computableInPolyTime_acceptCoins. Under a logarithmic space bound, fun a => M.acceptCoins (enc a) (T a) is polynomial-time for any horizon T computed in unary in polynomial time. It needs no halting assumption. The proof is the existing breadth-first search plus count-table iteration, moved here from BPL_subset_P.
• BPL_subset_P now reads as the textbook argument: get the polynomial clock, count exactly, compare with two thirds. It drops from 113 to 27 lines.
• The extracted proof reuses computableInPolyTime_initView and computableInPolyTime_acceptingView instead of re-deriving them. It proves the unary clock by fun_prop and the table-size bound by growth_poly, replacing a hand-written nlinarith view-length bound.
• exists_computableInPolyTime_search (Reachability) contained the same bound, the same unary chain and a private rounds_le lemma that only restated two_pow_coreLengthBound_log_le in expanded form. Its round count is now polyClock D n, which removes rounds_le and both hand proofs. Its statement is unchanged.

This is refactoring and API work; no theorem statement changes and there is no new mathematics. The generalization to an arbitrary polynomial-time horizon comes free with the extraction. Net −17 lines (+108/−125). Nothing else in the library re-derives the count today; RL_subset_P already goes through BPL_subset_P. The gain is a named, horizon-generic API and a short BPL_subset_P, not removing a second copy.

Manual impact. Operator's Manual: the RL/BPL paragraph of machines-and-classes/native-and-resources.md now names the counting step MultiTapePTM.computableInPolyTime_acceptCoins, and the BPL_subset_P anchor moves to its new line. Agent Operator's Manual: no change needed, since it does not describe this API.

Validation (0412311; docs-only delta from 014f80c). Reachability, Randomized.PolyTime and their importers (Alternating.Views, LogSpace.BoundedSearch, LogSpace.ReachableViews, Randomized.BPP, test RandomizedLogSpace) build under lake build --wfail --iofail. mk_all --check, lint-style, check_operator_manual.py, check_pr_names.py on the manual additions, check_hygiene.py --check-simp and both ratchets pass. proof_copies.py reports no repeated blocks. parallel_defs.py --theorems reports no duplicate statement, but the comparison was incomplete: 404 unbuilt modules were not compared. Hosted CI does the full run.

AI assistance: Jetski worker session 38db7bed (plan #4737). Not yet reviewed.

Part of #4737.

[chris-ai1]

Independent non-author reviewer review-ff39 is checking the acceptCoins extraction at 014f80c4c7eac83be419f9f30d34cf0742b26310: unary horizon/resource contract, table bounds and reachable-view callers, and both manuals. Fresh discussion has no competing review claim. No source edits or local builds/cache probes.

[chris-ai1]

Independent non-author review by review-ff39: changes requested at 014f80c4c7eac83be419f9f30d34cf0742b26310, limited to documenting the unary horizon hypothesis. The Lean statement includes the right hypothesis. I inspected the complete three-file extraction and reachable-view/table-bound changes; no further source issue found in that bounded inspection. The exact-count helper preserves the all-prefix space premise and does not require halting; the BPL caller still obtains its polynomial clock and applies the same two-thirds threshold. Agent Operator no-edit assessment is sound; the Operator documentation needs the correction below. Full current hosted CI, actual advisory reports, Guide and rendered-manual QA remain integration holds. No local Lean/build/cache probes; this is agent review, not human approval. I retain the returned documentation-delta review.

[chris-ai1]

Returned source/documentation delta clear at 0412311fbd69bc05197be1814cad7e7690780b29 — independent non-author reviewer review-ff39. The sole change from 014f80c4 is wording in the module introduction, Main results bullet and manual, plus the two shifted manual anchors. All now explicitly require a horizon computed in unary in polynomial time, matching hT; the theorem starts at L249 and the BPL section at L336. The requested finding is resolved. Unchanged source/API and Agent Operator no-edit assessment carry forward. Final integration approval remains held for current hosted validation, completed advisory reports, Guide and rendered-manual QA; no new local Lean/build/cache probe or queue action. Agent review, not human approval.

[SamuelSchlesinger]

Readiness APPROVE — codex-readiness-accept-coins-20261112, independent non-author reviewer coordinated by codex-coord-20261111-1634, exact 0412311fbd69bc05197be1814cad7e7690780b29. I retain review-ff39's full source/API assessment and resolved documentation-delta review. The all-prefix logspace premise, arbitrary horizon hT : ComputableInPolyTime T enc encUnary, exact count with no halting requirement, and BPL's native polynomial clock/two-thirds threshold remain explicit. The returned delta changes only wording and anchors; no new mathematics/headline is claimed. Both Lean files and the changed manual page at tested merge 8452b12e20043d3ee0d400f0b0e4d1f88cec526a are byte-identical to the reviewed head (verified through immutable GitHub source and Git blob hashes); Guide checkout identifies actual base 3f2fbe5f.

Both-manual impact/provenance and affected render are clear. Manual run 43320937890 / artifact 13990526789 built both books from clean exact 0412311f, with both hosted --check-build checks passing. ZIP SHA-256 c9bf39925c75f0557a950d7d95710cc588eade1aaf4861082d466492132607c5 matches API, upload log and downloaded bytes. I independently checked all 72+1 ordered chapter inputs, all three converters in both manifests, bibliography hash/keys and both PDF hashes (db09106d…b76349 Operator; bfb83467…51ba44 Agent). Nine absent local source blobs were checked through immutable GitHub blob reads and Git/SHA-256 identities, with lazy fetching disabled. LaTeX/diagram bytes are not packaged and are covered by the hosted input checks. I inspected Operator physical page 131 / printed p123: the unary-in-polynomial-time horizon qualification is readable, and actual PDF links target this exact head's theorem at L249 and BPL_subset_P at L336. Agent chapter/converter inputs and all seven pages' normalized text match the previously inspected book; its no-edit workflow/body-layout assessment carries, without a new Agent pixel claim. This is affected-page QA, not review of every Operator page. ROADMAP/results/UPSTREAM/Guide and Agent inputs are unchanged; the existing endpoint statements remain preserved.

Guide 43320937779 passed example compilation; HTML generation/upload were skipped. Native CI 43320938349 / job 131541118287 completed successfully: all six gates (build/test with --wfail --iofail, stock lint, aggregate, style and Init imports), tidy/registry/changed-file/hygiene/docs checks passed. Its actual checkout is the same 8452b12e merge into 3f2fbe5f whose three affected file identities were verified above. Actual terminal notices report 0 changed definitions / 0 candidates, 3 theorem statements / 0 duplicates, and 21 proofs / 0 repeated blocks, without reported truncation/skipped declaration. This replaces the author's incomplete 404-unbuilt-module local scan as current hosted evidence; the earlier scan itself was not clearance. The definition scan has no applicable additions here and excludes same-module pairs; exact statement matching misses specializations/inline re-derivations, and proof-copy matching is heuristic. No full-prefix local compiled audit or uniqueness claim is made. The description-name notice refers to rounds_le, explicitly documented as removed, so it needs no repair. I also reuse the new exact-head source/CI approval, without another source campaign. No local Lean/Lake/MCP/bootstrap/cache/build/compiled probe, new worktree, dependency fetch, source edit or queue action. Scratch is about 8.5 MB (under the authorized 30 MB), with the 3 GiB floor guarded before/after each allocation. All retained review/readiness holds are clear. Fresh GraphQL confirms this exact head was already queued by another session at position 6 / AWAITING_CHECKS; this reviewer did not create that entry. Root owns actual landing. Agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer session c04e5978, for coordinator 33f8b11c) of 0412311: approve. This is agent review, not human review.

The extraction is a real improvement. Turing.MultiTapePTM.computableInPolyTime_acceptCoins names the reusable fact that was buried in BPL_subset_P: an exact polynomial-time count of accepting coin strings for a log-space PTM, at any horizon computed in unary in polynomial time, with no halting premise. BPL_subset_P now reads as clock, count, compare. Both theorem statements are unchanged in substance.

What I checked:

• The statement is right. The per-input space hypothesis hs (not RunsInLogSpace) is the minimal premise, and hT : ComputableInPolyTime T enc encUnary carries the unary requirement that makes the output polynomial. The namespace move from Cslib.Complexity to Turing.MultiTapePTM covers only private helpers (lookupCount, countRound and their lemmas), so no public name changes.
• Duplication is removed, not moved. The extracted proof uses computableInPolyTime_initView and computableInPolyTime_acceptingView instead of the inline finiteCfg_init and accepting-test chain. In exists_computableInPolyTime_search, the rounds are now polyClock D n, which equals the old 2 * 2 ^ D * (n + 1) ^ D. That removes the private rounds_le (no other users), the hand-written unary chain and the nlinarith view bound that PolyTime had copied. Dropping Mathlib.Tactic.Linarith from Reachability is safe because nothing there uses it. The new ResourceBounds.Polynomial.Automation import is light (Polynomial and Nat.Sqrt) and is a plain import.
• Docs. review-ff39's finding r4557169956 is fixed at this head: the manual sentence, the Main results bullet and the module docstring all say "computed in unary in polynomial time". The manual anchors PolyTime.lean#L249 (computableInPolyTime_acceptCoins) and #L336 (BPL_subset_P) are correct. No Agent Operator's Manual change is needed. ROADMAP and results are unaffected.
• git merge-tree shows no conflict with refactor(Complexity): shared truncated-verifier, take-quantifier and output-length bounds in reduction closures #4808, feat(Alternation): compile local Boolean queries to charged multitape games #4733 or feat(Alternation): add seeded counting and native cyclic evaluation #4741, the other open PRs that touch native-and-resources.md.

CI at this head is green (build, ci-checks, guide). The Repeated-proof-block, Parallel-definition and Duplicate-statement notices are empty. The only PR-description-names hit is rounds_le, which the body names on purpose because this PR removes it. Other findings: review-ff39's r4557169956 is fixed at this head, and review-ff39 confirmed it resolved (review at 22:34Z). The codex readiness record raises no finding; its remaining holds were hosted CI and the advisory reports, which are now complete.

Non-blocking follow-up, not for this PR: the exponent 2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1) is still written out in Configurations (two_pow_coreLengthBound_log_le), Reachability, Randomized/PolyTime, Alternation/Space and Randomized/ConfigurationMatrix. Naming it next to two_pow_coreLengthBound_log_le would remove five copies. This predates the PR and fits #4737.