Games equivalent as games and the fundamental lemma

[MarcIlunga]

Proof-technique stack, layer 3 (games). Based on the H-coefficient PR, though independent of the two layers below it.

RandomSystem.GameEquivalent: two games equivalent as games, G ≡g H (CR18, Definition 4.16, p. 105). They give every transcript with every MBO unset the same probability, which is the cumulative condition CR18 states as equivalent to identical pre-winning behavior. Maurer 2002, Definition 5 (F^A ≡ G^C), is the same notion.

• Won alike: GameEquivalent.winProbability_eq and Domain.Distinguisher.winProbability_eq_of_gameEquivalent (CR18, Lemma 4.15, p. 106; Maurer 2002, Lemma 7 and Lemma 6 (ii)).
• The fundamental lemma: the advantage between the visible systems is at most the winning probability: GameEquivalent.abs_decisionProbability_sub_le and Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent (CR18, Lemma 4.16, p. 107; Maurer 2002, Lemma 7 and Theorem 1 (i)).
• Common part: Distribution.abs_mass_sub_le_of_le: two laws of weight one above a common part ν differ on every event by at most 1 - ν.weight. The conditional-equivalence bound from Games with a monotone binary output: Games, DistinctionGames and the interface instance #4 now uses it instead of proving the step inline.

There is no ≡g notation: the systems level has no scoped notation of its own.

THEORY.md §1.5 gets a paragraph.

Checks: build with --wfail, axiom audit, linter set, anchors, math rendering, CR18 pages 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)
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) ← this PR
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