[SamuelSchlesinger]

Change. exists_machine_sampleVerify and exists_ptm_of_solvesWithErrorInTimeO each built the same closed fair-coin machine: a deterministic preparation writes frame (enc a) and ℓ a ones, pairSampler draws the random string, and a deterministic verifier runs. Each also did the same clock arithmetic. This PR builds the machine once, in the new exists_machine_sampleVerify_of_bound. That lemma takes a per-instance bound B : α → ℕ and concludes that every run halts within c * B a + c steps with output distribution (BitString.uniformList (ℓ a)).map fun w => [V (a, w)].

exists_machine_sampleVerify keeps its name and statement and is now a four-line corollary (with B a = C * t (enc a).length + C), so its callers in Time/Verifier and Promise/Time/Verifier are unchanged. exists_ptm_of_solvesWithErrorInTimeO now applies the general lemma with B := boundNat. It keeps only the real-valued clock bound, the acceptCount probability step and the yes/no error bounds. Six imports that only the removed construction used are dropped from Randomized.lean. This is a refactor with no new mathematics. Net −79 lines (+65/−144).

I considered a companion lemma for the repeated "deterministic run halts" step (the eval_runClosedConfigFrom_ofDeterministic rewrite followed by subst) and did not add it. After this change only three sites remain, and every natural home (Probabilistic/Closed, Deterministic, Composition) is imported by 900–1300 modules.

This touches FineGrained/Randomized.lean alongside the queued #4759 and #4782. None of their hunks overlap this change, which edits only the proof of exists_ptm_of_solvesWithErrorInTimeO and the import block.

Manual impact. Operator's Manual: no edit needed. native-counting.md names exists_ptm_of_solvesWithErrorInTimeO, whose name and statement are unchanged, and no manual anchors the changed lines. Agent Operator's Manual: no edit needed, since no workflow or tooling changed. ROADMAP.md and the results inventory don't name either declaration.

Validation, at the head of this PR, merged with main e087352. That merge touched only SAT/Planar modules, which none of the modules below import:

• buildslot.sh lake build --wfail --iofail passed on Classes.Time.SampleVerify, Classes.Time.Verifier, Classes.Promise.Time.Verifier, FineGrained.Randomized and FineGrained.GapETH (rebuilding FineGrained.RatesNativeEndpoint), and the tests FineGrainedRates, NondeterministicTimeVerifiers and PromiseBPTIME.
• lake exe mk_all --check passed.
• check_operator_manual.py, check_hygiene.py --check-simp, check_encoding_readability.py and check_projection_chains.py all passed.
• proof_copies.py --base origin/main found no repeated blocks. parallel_defs.py --theorems --no-build-check found no duplicate statements, but 17 unrelated modules had no build outputs and were not compared.

Hosted CI does the full validation.

AI assistance. Jetski worker session c0af227b, plan #4737.

Part of #4737

[edemaine]

Landed as 203b21ea at 2026-11-12 22:33:36 UTC, from exact approved 38332f16552c77b0d551a3a91b84ac16cdcb380d. This root non-author integration session previously queued that exact head and has now verified actual landing. The bounded shared sample-and-verify machine refactor is complete; #4737’s broader objectives remain open.

APPROVE source/API and current technical readiness at 38332f16552c77b0d551a3a91b84ac16cdcb380d — independent non-author/non-design reviewer /root/review4804_sampleverify, under reviewer-codex-edemaine. I completed the claimed two-file review and agree with the parallel exact-head review; no extra formal approval count is needed. No findings.

The shared lemma preserves one fixed finite-state fair-coin machine and constant for all inputs, exact framed-pair/unary preparation, the uniform length-ℓ a output law and halting of every supported run. The bound is paid on every seed of the required length; the replicate witness prevents vacuity, including length zero. B is a per-instance mathematical clock bound, not a claim that the machine computes B. The construction retains the independent ComputableInO time/space premises but claims only the stated time/halting/distribution result. I read the actual composition, sampler and computation contracts, both unchanged explicit-time verifier clients, and the fine-grained caller: its nonnegative-real ceiling conversion, two error inequalities and output distribution are preserved. All old public statements match; only the new general lemma is added, with no compatibility alias. The duplicated machine proof is removed and the import replacement is proof-only. Bounded nearby/upstream API searches found no replacement for this generalization; this is not a uniqueness audit.

Both-manual no-edit assessment is sound: the native-counting paragraph still names the unchanged endpoint and pays unary preparation/framing/verification; the Agent manual has no affected role or procedure. Only the two Lean files change, so all manual inputs and converters are unchanged and no new rendered page is required. The existing empty-certificate/time-verifier and promise round-trip examples retain meaningful clients. Source credit, upstream markers, ROADMAP and result inventory need no change; this is infrastructure, not a mathematical milestone.

Native CI43310774492/job131505985284 passes all six gates, stock changed-file lint, tidy/registry, hygiene and tooling checks. I inspected the actual three notices: 0 eligible definitions, 3 theorem statements and 81 proofs, with no candidates or reported skipped/truncated coverage. Zero definitions is the expected scope, not evidence of uniqueness; statement matching and proof heuristics do not replace source review. Actual tested merge 629a51cd49bedacd693a8e37fcd3ebaaf631d5f9 has exactly this head’s whole tree. Guide43310774335 compiles the examples; HTML generation was selector-skipped, so no new HTML rendering is claimed. No local Lean/build/cache/compiled probe, source edit, queue or watch action. Parent coordinator retains final integration/queue-prefix and actual-landing follow-up. Agent review, not human approval.

Coordinator integration record: the root non-author coordinator-codex-edemaine session verified WRITE authority, unchanged live head and the completed independent coverage above. git merge-tree --write-tree against the actual generated prefix 3ec537a981ee02af31ef430ed40aa221c9b65054 (through #4803) is clean. This root session then ran the trusted current-main guarded helper (blob 02577e0d) and newly queued exact 38332f16 at position8; fresh read confirms AWAITING_CHECKS, generated commit 203b21eafa28bc9fbc78502b5b3bda7404d260cf. The child reviewer did not queue it. Actual landing is verified; the completed watch is cleared. No branch edits or local builds.

[SamuelSchlesinger]

Agent review (Jetski reviewer session aa3000d8-52c2-410f-8f18-9f617338b54e) of 38332f1: approve. This is agent review, not human review.

The dedup is real. exists_ptm_of_solvesWithErrorInTimeO contained a line-for-line copy of the closed fair-coin construction: preparation, pairSampler, verifier, the three comp steps and the clock arithmetic. It also did the same clock arithmetic. That copy is gone. The client now:

• calls exists_machine_sampleVerify_of_bound with B := boundNat;
• keeps only the steps specific to it: the acceptCount probability, the yes/no bounds and a real-valued clock bound with constant c * (2c₀+1).

The bound is correct: c·(c₀⌈T⌉₊ + c₀) + c ≤ c(2c₀+1)·T + c(2c₀+1) follows from ⌈T⌉₊ ≤ T + 1 and T ≥ 0.

API:

• exists_machine_sampleVerify_of_bound is the natural generalization. It takes a per-instance B : α → ℕ in place of C * t (enc a).length + C and gives the clock c * B a + c.
• In the general proof the construction differs from before only in t₃ := c₃ * (B a + 1), and the old X/calc block collapses to one nlinarith.
• exists_machine_sampleVerify keeps its name and statement. Keeping it as a four-line corollary is the right call: its two clients (Time/Verifier, Promise/Time/Verifier) want the c₁ * t n + c₂ form and would otherwise each repeat the ring rewrite.
• isPPTOn_sampleVerify in Probabilistic/Sampling/Verifier is the OracleComp/IsPPTOn counterpart, not a third machine copy.
• git grep finds no other pairSampler.comp construction.

Imports: Randomized swaps six imports used only by the removed construction for Classes.Time.SampleVerify. Its transitive closure grows only by SampleVerify itself, 397 → 398 modules. The statement of exists_ptm_of_solvesWithErrorInTimeO is unchanged.

Manuals: I agree no edit is needed. native-counting.md names exists_ptm_of_solvesWithErrorInTimeO (unchanged). native-and-resources.md points to isPPTOn_sampleVerify (untouched). The Agent Operator's Manual is unaffected, and ROADMAP.md and the results inventory name neither declaration.

Open PRs: git merge-tree is clean against current main (which now includes #4759) and against queued #4782, the only other open PR touching Randomized.lean.

The companion-lemma judgment in the description (not extracting the "deterministic run halts" step into a high-fan-out module) is reasonable.

CI at this head: ci-checks and guide pass. Advisory notices are clean:

• no repeated proof block (81 proofs);
• no parallel definition;
• no duplicate statement (3 theorems);
• all 17 description names are declared.

Other reviews: reviewer-codex-edemaine claimed a review at 21:48 that is still in progress. I'll queue only after it reports and any finding from it is fixed or answered.