Couplings of random systems

[MarcIlunga]

Proof-technique stack, layer 1 (systems level). Based on the ℝ≥0 bounds PR.

A PDS is a distribution over deterministic systems, so a coupling of two PDSs is just a coupling of distributions, Distribution.IsCoupling J P Q: no new structure. This ports the easy direction of Lanzenberger–Maurer's coupling theorem.

New file RandomSystems/Distance/Coupling.lean:

• System.tr s σ n: the transcript of a deterministic system with a strategy within n rounds (Lanzenberger–Maurer, Definition 7, p. 12), and tr_eq_iff.
• PDS.sLaw_behavior_eq_fTransform: the transcript law of the random system of a PDS is the pushforward of the PDS by the transcript map (footnote 9, p. 14; Definition 4, p. 10).
• PDS.statDist_sLaw_behavior_le_of_isCoupling, per environment: under a coupling, the transcript laws are within the probability that the two transcripts differ.
• PDS.transcriptDistance_behavior_le_of_isCoupling, globally: the transcript distance is at most the probability that the two systems differ (the inequality of Theorem 2, p. 15). The attainment half of Theorem 2 is not part of this PR.

The new transcript function replaces the run of an environment against a total resource (TotRes, eRun, tr E n s and their lemmas in Distance/Transcript.lean), which nothing used, so one transcript function remains.

THEORY.md §1.4 gets a paragraph on couplings.

Checks: build with --wfail, axiom audit, linter set on the new file, anchors, math rendering, citations checked on the PDF.

The stack

Proof techniques for the HCTR2 port, one technique per PR, ordered by abstraction (merge bottom-up):

1. Bounds in ℝ≥0 #25 Bounds in ℝ≥0 (convention)
2. Couplings of random systems #26 Couplings of random systems (systems) ← this PR
3. The H-coefficient bound for random systems #27 The H-coefficient bound for random systems (systems)
4. Games equivalent as games and the fundamental lemma #28 Games equivalent as games and the fundamental lemma (games)
5. Identical until bad: a common part, per-step costs, and coupled games #29 Identical until bad (games)

🤖 Generated with Claude Code

https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9