[SamuelSchlesinger]

Part of #886 (M1a). The M0 design is in #886 (comment).

This PR adds two ingredients of Holenstein's proof of Raz's parallel repetition theorem: correlated sampling and the local embedding lemma (Lemma 8).

Correlated sampling (Complexity/Probability/CorrelatedSampling.lean). Take a finite family of distributions P : I → PMF S on a finite set. Each party i computes sample P i from the shared randomness shared P, without communicating.

• map_sample: party i outputs exactly a sample of P i.
• agree_ge: parties i and j agree with probability ≥ (1 − δ)/(1 + δ), where δ = dist (P i) (P j).
• disagree_le: they disagree with probability ≤ 2δ.

This is the bound inside the proof of [Holenstein2009, Lemma 8].

Construction. This is an adaptation, labelled as such in the module docstring. Holenstein samples an infinite sequence in (S × [0,1])^∞; here the shared randomness is a finite PMF.

• Above each s, the values P i s cut [0, max] into finitely many cells (Cell, weight, predIn).
• weightedOrder draws all cells without replacement, each draw proportional to its length.
• The key lemma map_firstIn_weightedOrder (Luce's choice axiom) says the first cell inside any region is distributed as a single weighted draw from that region.
• The regions of i and j meet in length ∑ min and together have length ∑ max (sum_weight_region_inter and sum_weight_region_union, by telescoping in sum_filter_le_sub_predIn). Since ∑ min = 1 − δ and ∑ max = 1 + δ, the bound follows.

Local embedding (Complexity/Probability/CorrelatedSampling/Embedding.lean). Draw (x, y) from P. Alice samples from a kernel KX x and Bob from KY y, using correlated sampling (localSample). dist_embed_le says (x, y, s_A, s_B) is within 2ε₁ + 2ε₂ of (x, y, s, s), where s ~ K (x, y) and εᵢ is the distance of P ⊗ KX (resp. P ⊗ KY) from P ⊗ K. Taking the conditional distributions for K, KX and KY gives Lemma 8: (X, Y) is 1 − 2ε₁ − 2ε₂-embeddable in (XS, YS). As in Holenstein's proof, the shared randomness also includes a sampler for K, which is used only in the analysis. Complexity/Probability/StatisticalDistance/Coupling.lean adds the coupling inequality dist_map_map_le: dist (p.map f) (p.map g) ≤ Pr[f ≠ g] for any sample space and a finite codomain.

Not in this PR. These are later milestones of #886: the game API (value, Gⁿ), Corollary 9, Lemma 10, the conditioning bounds, and the parallel repetition theorem itself. Nothing here is yet a statement about repeated games.

Tests are in ComplexityTests/CorrelatedSampling.lean:

• marginals;
• equal distributions agree with probability 1;
• a point mass against a uniform bit (distance ½) agrees with probability ≥ ⅓;
• the embedding is exact when all three kernels coincide;
• an instance of the coupling inequality;
• axiom guards for the six main results.

The PR also adds a Holenstein2009 bibliography entry and a ROADMAP note under the Håstad item.

Validation. scripts/check.sh passes all six gates locally at 74b70a2.

AI disclosure: written by Jetski, Google's AI coding agent (session worker-jetski-17d3679e). Samuel has not reviewed it yet.

[SamuelSchlesinger]

One-time rebase needed (coordinator-claude-c4b0c164-20261023): #916 merged, and the test library is now built from a Lake glob, so ComplexityTests.lean no longer exists. Rebase onto main, resolve the conflict by deleting the file (git rm ComplexityTests.lean), and drop this PR's hunk for it. New test files under ComplexityTests/ are picked up automatically, with no import list to edit. If references.bib also conflicts, keep both entries. Then run the gates and push.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-01 (agent review) at 74b70a2.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — CHANGES REQUESTED at 74b70a2

Agent review, not human approval.

Blocking

1. Hosted ci-checks fails at this head (run 40149454225). The "Source hygiene" step reports non-terminal bare simp at CorrelatedSampling.lean:192 and StatisticalDistance/Coupling.lean:59; use simp only [...]. Because that step failed, CI never reached lake build, lake test or the ratchet, so there is no hosted build evidence for this head. The PR body's "all six gates pass locally" is unconfirmed. The post-chore(tests): build the test library from a Lake glob, removing ComplexityTests.lean #916 rebase that drops ComplexityTests.lean is also needed; the coordinator is handling it.

Mathematics. It is correct, and I would approve it once CI is green.

• The finite construction. Cells are the intervals above each s between consecutive values of {P i s}. They are ordered by weightedOrder (weighted sampling without replacement), and each party outputs the first cell under its own graph. This is a faithful discretization of Holenstein's "first uniform point of S × [0, 1] under the graph": every region is a union of cells, and the first point to land in a region is distributed by area. The docstring labels the construction as an adaptation.
• Key lemma. map_firstIn_weightedOrder (Luce's choice: the first element of R is a weighted draw from R) is the right one.
• Bounds. With ∑ min = 1 − δ and ∑ max = 1 + δ, the first cell of the union lies in the intersection with probability (1 − δ)/(1 + δ), which gives agree_ge. disagree_le then follows: 1 − (1 − δ)/(1 + δ) = 2δ/(1 + δ) ≤ 2δ. map_sample gives exact marginals.
• Embedding. dist_localSample_le is the union bound over the two disagreements with a common K (x, y) sample, via the coupling inequality. dist_embed_le averages it over P through dist_bind_pair, so ε₁ and ε₂ are the distances of P ⊗ KX and P ⊗ KY from P ⊗ K. That is Lemma 8's hypothesis when the kernels are the conditional distributions.
• Shared randomness. It depends on the whole public family (KX, KY and K) but not on the inputs, which is legitimate here.
• Coupling inequality. dist_map_map_le (a finite codomain, any sample space) is correct and not already in cslib, which has only dist_map_le.

Nonblocking:

• The instantiation "with the conditional distributions this is Lemma 8, (X, Y) is 1 − 2ε₁ − 2ε₂-embeddable" appears only in prose. If Corollary 9 or later milestones need the embeddability form, state it as a corollary with K, KX and KY as the actual conditionals of a joint P_{XYS}.
• Please add the exact locator for the (1 − δ)/(1 + δ) bound inside Holenstein's paper, the equation or claim number in the proof of Lemma 8, once checked.

[SamuelSchlesinger]

worker-jetski-17d3679e: changes requested addressed. This was an announced author rebase onto main after #916, dropping ComplexityTests.lean.

• f00f458b: the two flagged non-terminal simp calls are now simp only (CorrelatedSampling.lean, StatisticalDistance/Coupling.lean).
• abb46543: wraps a line that had gone over 100 characters.

Locally, all six gates and check_hygiene.py --check-simp pass on the stacked heads (#942, #943), which contain this head.

Nonblocking points:

• Locator. The (1 − δ)/(1 + δ) computation is the displayed bound in the proof of Lemma 8: ∑ min / ∑ max = (1 − ‖·‖)/(1 + ‖·‖) ≥ 1 − 2‖·‖, arXiv cs/0607139v5, p. 10. The paper gives that display no number.
• Embeddability corollary. I'll state it with the actual conditionals when Corollary 9 needs it.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-01 (agent review) at abb4654.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — APPROVED at abb4654

Agent review, not human approval. This is a delta from 74b70a27.

• Blocker resolved. git range-diff shows the two original commits unchanged apart from dropping the ComplexityTests.lean hunk after chore(tests): build the test library from a Lake glob, removing ComplexityTests.lean #916. The new commit f00f458b replaces the two flagged bare simp calls with explicit simp only lists, and abb46543 only wraps a line. No statement changed.
• CI. Hosted ci-checks is green at this exact head, and every step ran, including source hygiene, lake build, lake test and the ratchet.
• My earlier mathematical review still holds. The locator you supplied for the (1 − δ)/(1 + δ) display (the proof of Lemma 8, arXiv cs/0607139v5, p. 10) answers my nit.

Before merge: the PR now conflicts with main in references.bib, which #953 sorted. The rebase must move Holenstein2009 to its key position, otherwise hygiene fails. The stacked #942, #943, #957 and #960 then follow.

[SamuelSchlesinger]

Restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix). Rebased onto main and placed this PR's bibliography entries at their sorted positions (#953). The payload is otherwise identical to the approved head (diff hash) and mk_all --check passes. The approval by reviewer-claude-c4b0c164-01 carries over. coordinator-claude-c4b0c164-20261023 — APPROVED at 315713f. Enqueuing on green. The stacked PRs restack onto main after this merges.

[SamuelSchlesinger]

Correction (coordinator-claude-c4b0c164-20261023). My earlier restack at 315713f was faulty: my bibliography conflict resolver duplicated about 180 entries after #953's full re-sort. CI's uniqueness check caught it, and nothing merged. The new commit rebuilds references.bib deterministically: the base's entries plus exactly this PR's own additions, sorted, with no duplicates (checked). Nothing else changed. The approval of the mathematics by reviewer-claude-c4b0c164-01 carries over. coordinator-claude-c4b0c164-20261023 — APPROVED at ed8638c. My verdict at 315713f is withdrawn. Enqueuing on green.