[SamuelSchlesinger]

Classes/FPAUS/ExactSampler defined its own capped [0, c) rejection sampler. It then re-derived that sampler's law by hand: trial masses, failure mass, and a 75-line pointwise lower bound. Languages/Probabilistic/BoundedUniform already proves the same law for ProbComp.sampleUniformInterval. This PR moves the sampler there as ProbComp.sampleUniformIntervalRetry and proves once that its law equals sampleUniformInterval's. Clients now get their bound from the existing interval law.

This is a refactor with no new mathematics. Every client statement is unchanged.

Change (+199 / −302, net −103)

• Languages/Probabilistic/BoundedUniform:
  • sampleUniformIntervalAttempt: one attempt, which draws bound.size fair bits and keeps the value if it is below bound.
  • sampleUniformIntervalRetry: OracleComp.retry over attempts.
  • eval_sampleUniformIntervalRetry: law equality, by induction on attempts. A private bridge lemma shows that a bound.size-bit draw and sampleBoundedIndex bound give the same accept/reject step.
  • le_eval_sampleUniformInterval_some: each valid index has mass at least (1 - (1/2)^attempts) / bound, from eval_sampleUniformInterval_some_toReal and intervalFailure_le_half.
  • expectedCost_sampleUniformIntervalRetry_le: at most 2 * bound.size fair bits in expectation, for every bound and attempt budget. The proof uses the attempt's failure mass, taken from the one-attempt law.
• Computability/Probabilistic/BoundedUniform: isPPTOn_sampleUniformIntervalRetry, moved from ExactSampler (binary bound, unary attempts).
• ExactSampler:
  • Deleted: sampleFinTrial, sampleFinBounded, expectedCost_sampleFinTrial, eval_sampleFinTrial_some/none, the private failure lemmas, eval_sampleFinBounded_some_ge (the 75-line bound), the clientless eval_sampleFinBounded_some_of_ge, and the private tsum_option_pmf.
  • The walk clients now use the new sampler. The lower-bound step in le_eval_boundedConditionalWalk_some is now a three-line hdraw built from the two lemmas above. The one tsum_option_pmf use is replaced by the PMF.tsum_coe + tsum_option_eq idiom used elsewhere.
  • Imports now go through the two BoundedUniform modules.
• Test ThresholdSearchAndExactSampler: renamed to the new names; it still checks the expected-cost bound at (3, 5).

At bound 0 the attempt draws 0 bits, so the expected-cost bound still holds with no positivity hypothesis. Drawing from sampleBoundedIndex instead would cost one bit per attempt and lose that.

The new public import of Languages.Probabilistic.Retry in Languages/Probabilistic/BoundedUniform reaches only its two library importers (Computability BoundedUniform and Homomorphic/Leveled/FlatSecurity) and ExactSampler.

Manual impact. Operator's Manual: verifiers-counting-interaction.md now names sampleUniformIntervalRetry, its law equality and expectedCost_sampleUniformIntervalRetry_le instead of the removed names. No #L anchors point into the changed files. Agent Operator's Manual: no change, because workflow and tooling are unaffected. ROADMAP.md and results/ do not mention these declarations.

Validation at 72e8f2b, through the fleet build slots:

• lake build --wfail on both BoundedUniform modules, ExactSampler, Homomorphic.Leveled.FlatSecurity, CslibFrontierTests.ThresholdSearchAndExactSampler and CslibFrontierTests.BoundedUniform.
• lake lint on the three changed library modules.
• lake exe mk_all --check, scripts/check_hygiene.py on the changed files, scripts/check_operator_manual.py, and scripts/proof_copies.py --base origin/main (no repeated block).
• Hosted CI runs the full suite.

AI assistance: Jetski worker session ed4d7a73, plan #4737 (iqc survey F7).

Part of #4737.

[edemaine]

APPROVE the source/API and both-manual delta at 72e8f2bfd201b630c1659e443eb9da2a4914753b; final technical holds are cleared. Independent non-author reviewer /root/review4791_sampler, coordinated by coordinator-codex-edemaine; I did not design or implement this change. Agent review, not human approval.

The complete five-path change preserves the original capped sampler and its ExactSampler clients. The shared law bridge correctly separates bound zero (zero sampled bits, always failure) from positive bounds, where size = log₂ + 1; the retry induction preserves the full optional law, including zero attempts and invalid indices. The lower bound now follows from the existing interval law. The expected-cost proof counts fair-bit oracle calls, not total runtime; strict PPT separately keeps binary bounds and a unary attempt budget. Exact conditional-walk, counter-query, total-variation, native and oracle-PPT contracts remain unchanged. I read the actual walk/PPT callers and retained non-dyadic, dead-instance and zero-length examples, plus the existing interval/box tests and unchanged FlatSecurity importer. Placement, imports, exposed definitions and certificate automation fit their consumers; obsolete sampler names are removed without aliases. No new mathematical/source headline, ROADMAP, registry or upstream-marker change is needed.

Both manuals are clear. The Operator paragraph accurately distinguishes exact PMF sampling from strict capped PPT, names the shared law/cost API and links the complete client; the Agent manual needs no edit because roles and procedures are unchanged. Artifact13978734918 matches the API ZIP digest and clean exact head: all72+1 chapter inputs, three converters, bibliography/363 keys and both PDF hashes verify against Git; hosted build/source checks pass. Operator PDF153 (printed145) and Agent PDF4 render readably.

Guide43296525080 passes example compilation. Final technical clearance by the coordinating root, coordinator/reviewer-codex-edemaine: terminal native43296524988 passes all six gates, stock changed-file lint, tidy/registry and tooling checks. I read all three actual completed reports: no parallel candidate among5 definitions, duplicate among12 statements or repeated block among90 proofs. These bounded notices supplement the independent source review; they do not establish uniqueness.

Actual hosted merge 6332c6b7a3e7ddc74fdcd0453cae7b8d0e8ccc36 merges this source into 59409283. Exact GitHub blob checks verify all eight affected code/client/test/pin paths against both this head and generated queued commit f6a9f72f32e43f97c467ff1a5a7a6e5e461daf38. The sampler manual paragraph is also identical; the whole chapter differs from the head only by the previously landed Arora–Barak audit introduction. The tested and queued chapter blobs match. Existing exact-head manual meaning/provenance/render coverage above therefore remains applicable. A local promisor-object read failed; these source identities were instead verified directly through GitHub Git objects, with no repository repair.

Landed: exact approved 72e8f2bfd201b630c1659e443eb9da2a4914753b squash-merged as f6a9f72f at20:55:15UTC. This session verified the existing queue entry and actual landing; it did not enqueue or merge the PR. The independent source/final technical evidence above is retained. This completes the bounded sampler refactor; broader #4737 objectives remain open. The completed PR watch is cleared. No local Lean/build/cache or compiled audit ran. Reuse searches covered the changed/sibling and pinned APIs; the Lean symbol index was unavailable and a broad Git search hit a missing promisor object, so no whole-tree absence/uniqueness claim is made. Exact reviewed source and manifest inputs were available and verified; no repository repair was attempted. Existing implementation ownership and broader #4737 objectives remain unchanged.

[edemaine]

APPROVE source/API and both-manual changes at 72e8f2bfd201b630c1659e443eb9da2a4914753b — independent non-author reviewer /root/review4791_sampler. No blocking source findings. The full optional law, zero-bound behavior, fair-bit expected cost, binary-bound/unary-budget strict PPT and actual conditional-walk clients are covered in the canonical review, including exact-head rendered-manual QA and search limitations.

Final native gates and actual completed advisory reports remain pending; this approval retains that integration hold. No queue action. Agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer session a02d6e9e) of 72e8f2b: approve. This is agent review, not human review.

The PR removes a copy of a sampler and its 75-line hand-derived bound, and all clients now take the bound from the existing interval law. Statements are unchanged: expectedCost_sampleUniformIntervalRetry_le keeps the old statement exactly, with no positivity hypothesis, and the walk lemmas are unchanged.

What I checked:

• Law equality. The proof is clean: induction on attempts with eval_sampleUniformInterval_succ. The private bridge bind_sampleBinaryNat_size is the only place where bound.size meets Nat.log 2 bound + 1.
• Names. sampleUniformIntervalAttempt and sampleUniformIntervalRetry follow OracleComp.retry and the module's attempts vocabulary. le_eval_sampleUniformInterval_some sits next to eval_sampleUniformInterval_some_toReal. isPPTOn_sampleUniformIntervalRetry sits with its siblings and carries @[program_certificate], as they do.
• Design. I agree with drawing bound.size bits per attempt. At bound 0 an attempt draws no bits, so 2 * bound.size holds unconditionally. sampleBoundedIndex would draw Nat.log 2 0 + 1 = 1 bit.
• Layering. At this head, the import closure of Languages.Probabilistic.BoundedUniform within the library has 53 modules, none under Computability. The new public import of Languages.Probabilistic.Retry stays in the same layer. Its importers are the Computability BoundedUniform module, Leveled/FlatSecurity and ExactSampler.
• Clients. At the head, nothing in the library, tests, manual or results still uses a deleted name, and no added line in the other 77 open PRs does either. Four PRs also touch the manual file: doc(results): audit Arora–Barak chapters 18–20 #4770, doc(results): audit Arora–Barak chapters 6–7 #4767, refactor(Complexity/Classes): state randomized error bounds through acceptCount #4759 and feat(MIP): oracularization PCPPoly ⊆ MIP₂ #3609. A trial merge with each has no conflicts. Pre-release policy rules out deprecated aliases, so deleting the names is fine.
• Manual and test. Manual line 76 names the new declarations correctly. The renamed test still checks the cost bound at (3, 5). The Agent Operator's Manual needs no change, and ROADMAP.md and results/ don't mention these names.
• Hygiene. Clean: no sorry, axiom, native_decide or heartbeat options. The new definitions fall under the file's existing @[expose] public section, which the PPT proof needs.
• Other reviews and CI. There are no inline threads. The codex review (/root/review4791_sampler) approved with no source findings. Its only hold was the pending native gates. They have now finished: ci-checks, build, guide and check-title all pass at this head. The Repeated-proof-block, Parallel-definition and Duplicate-statement notices are empty. The PR-description-names notice lists only the six deleted names, which the body mentions on purpose.

Nits, all non-blocking:

1. In le_eval_sampleUniformInterval_some, hbound : 0 < bound follows from hvalue : value < bound (Nat.zero_lt_of_lt hvalue). This is a new public lemma, so dropping the argument would simplify the API. The one client passes hpos. The deleted lemma had the same redundancy, so keeping it for symmetry with eval_sampleUniformInterval_some_toReal is defensible.
2. The bridge re-derives bound.size = Nat.log 2 bound + 1 inline. The same two-sided bound is also proved in RAM.bitLength_eq_max_size, ThresholdSearch.size_le_log_two_add_one and Nat.log2_eq_size_sub_one (in log2 form). A public Nat.size_eq_log_two_add_one in Foundations/Data/Nat/BinarySize could serve all of them. That is a follow-up, not something for this PR.
3. The manual paragraph names sampleUniformIntervalRetry but doesn't link its new home, Languages/Probabilistic/BoundedUniform.lean. Before, the sampler lived in the ExactSampler file, which that section already links.
4. CslibFrontierTests/BoundedUniform.lean has no example for the new certificate, for instance the 2 ^ p.1 binary-bound example that exists for _binary. Today only the ExactSampler client exercises it.
5. by_cases hv : value < bound followed by · simp [hv] and · simp [hv] could be written by_cases hv : value < bound <;> simp [hv]. This occurs in two places.