Identical until bad: a common part, per-step costs, and coupled games

[MarcIlunga]

Proof-technique stack, layer 4 (games on top of the systems level): identical until bad. It combines couplings (#26) with games equivalent as games (#28), and adds the per-step cost bound. The potential argument is proved once.

Systems level (RandomSystems/Distance/UntilBad.lean)

• transcriptCost β h: the sum over the steps of a transcript of the cost β p x of the query x after the prefix p.
• RandomSystem.one_sub_le_sum_tSupp, the potential argument (the union bound over the steps). If g lies below a random system R, g [] = 1, each step from a possible transcript by an admitted query loses at most β h x · R h of g, and every possible transcript costs at most ε, then the transcripts of a compatible environment within n rounds carry at least 1 - ε of g.
• RandomSystem.transcriptDistance_le_of_transcriptCost_le: random systems above a common part, with those per-step costs, are within ε. The proof ladders' transcriptDistance_le_of_untilBad is the case β h x = β x (Upstream candidates from downstream projects: a layer-by-layer PR stack #14, L1d).

Games (RandomSystems/Game/UntilBad.lean)

• A game that sets the MBO at each step with probability at most β h x times that of the unset transcript is won with probability at most ε, by a deterministic or a probabilistic distinguisher: winProbability_le_of_transcriptCost_le.
• RandomSystem.GameEquivalent.transcriptDistance_visible_le: two games equivalent as games share their unset part, which is a common part of their visible systems, and the first game's per-step costs bound its missing mass. So the visible systems are within ε. Neither game needs to be monotone, and only the first needs to reply at the queried interface.
• PDG.gameEquivalent_behavior_of_isCoupling: two discrete games with a joint law (Lanzenberger–Maurer, Theorem 2), whose pairs share the condition and answer alike while it does not hold, are equivalent as games (CR18, Definition 4.16; Maurer 2002, Definition 5).

Helpers in lower files

• Distribution.mass_sub_mass_le_of_le: the one-sided common-part bound, which needs only the first law to have weight one; abs_mass_sub_le_of_le now applies it twice.
• RandomSystem.sum_tSupp_succ: sums over transcripts within m + 1 rounds; sum_tSupp now uses it.
• RandomSystem.sum_tagMBO: extracted from the proof of RandomSystem.visible.

THEORY.md §1.5 gets a paragraph.

Checks: build with --wfail, axiom audit (10,392 declarations), linter set on the new and changed code, anchors, math rendering, citations checked on the PDFs.

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)
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) ← this PR

🤖 Generated with Claude Code

https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9