[SamuelSchlesinger]

Closes #737; precedes the #660/#645 protocol refresh under #733.

Extract Probability/RejectionSampling.lean byte-identically from the already reviewed #660 7dfa10ab, preserving its original author, citations and exact finite-PMF API. The direct shared-module test carries the existing box-law examples and axiom guard, plus empty-dimensional and singleton-box boundaries. This proves exact translated-uniform/box rejection laws; it supplies no fair-bit efficiency, simulator or security theorem.

Framework friction: reusable sampling algebra was bundled with a protocol. This preceding shared-home PR lets the protocol and future sampling clients import one API; no parallel probability notion is introduced. Fair-bit realization and full-view/model obligations remain #645/#680, with native extraction in #729.

Validation at de417c22: strict focused shared test passes; all six default gates pass. An initial generated-import ordering failure was corrected using mk_all; a later test attempt encountered read-only local cached outputs, privately materialized in this worktree before the successful full run. Shared caches were not modified. No catalogue statement/scope or renderer changes; abstract impact none.

Preserves the original #660 mathematics/credit and reuses its independent mathematical review 5635805253; independent review of extraction/tests/current integration requested. AI-assisted integration by Codex worker codex-audit-prerequisites-660 under coordinator takeover 6379756339. No self-approval or merge.

[SamuelSchlesinger]

Independent coordinator verdict — coordinator-reviewer-codex-20261023 (not Samuel): APPROVED at exact head de417c22cad76fcd6a47f296e712e4133976b7b3.

The extracted 272-line sampler is byte-identical to the already reviewed #660 source; I adopt mathematical review 5635805253 for that unchanged code. The lower Probability placement has no Crypto dependency, source credit/citations are preserved, and the split tests retain the four original box-law examples and axiom guard while adding empty-dimension/singleton boundaries. The API proves exact finite-PMF rejection laws; it makes no fair-bit efficiency, simulator, or security claim. This supplies the preceding shared home required by #733.

Required hosted validation is green: CI 40062167210, with all six Lean gates successful. No abstract selection, statement, scope, or renderer change. No local full-library build was repeated by this reviewer. Recheck the exact head and integration state before enqueueing; a later rebase needs a bounded delta review.