From e0db706d02df2c2e0e7cd13796a3a29514adb83c Mon Sep 17 00:00:00 2001 From: Marc Ilunga Date: Mon, 12 Oct 2026 17:16:29 +0100 Subject: [PATCH] Games: equivalence as games and the fundamental lemma MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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, the cumulative condition CR18 states as equivalent to identical pre-winning behavior; Maurer 2002, Definition 5 (F^A ≡ G^C), is the same notion with a monotone event sequence in place of the unset MBO. Such games are won alike (`GameEquivalent.winProbability_eq`, `Domain.Distinguisher.winProbability_eq_of_gameEquivalent`; CR18, Lemma 4.15; Maurer 2002, Lemma 7 and Lemma 6 (ii)), and the advantage between their visible systems is at most the winning probability, the fundamental lemma (`GameEquivalent.abs_decisionProbability_sub_le`, `Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent`; CR18, Lemma 4.16; Maurer 2002, Lemma 7 and Theorem 1 (i)). `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 `RandomSystem.abs_decisionProbability_sub_le_winProbability` now uses it instead of proving the step inline. THEORY.md §1.5 gets a paragraph; `#print axioms` lines for the four theorems. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9 --- THEORY.md | 50 +++++--- src/Probability/Distribution.lean | 42 ++++++- src/RandomSystems/Game/MBO.lean | 196 +++++++++++++++++++++++------- src/Tests/Axioms/Systems.lean | 4 + 4 files changed, 232 insertions(+), 60 deletions(-) diff --git a/THEORY.md b/THEORY.md index 2d35850..351b515 100644 --- a/THEORY.md +++ b/THEORY.md @@ -205,6 +205,21 @@ G \mathrel{|\!\equiv} T, \quad \Pr_G[\text{MBO set} \mid x^n] \le \varepsilon \ \Delta(G^-, T) \le \varepsilon . ``` +Two games are [**equivalent as games**][RandomSystem.GameEquivalent], $`G \overset{g}{\equiv} H`$, +when they behave alike as long as the MBO is unset: they give every transcript with every MBO +unset the same probability [3, Definition 4.16], [4, Definition 5]. A distinguisher then +[wins both alike][Domain.Distinguisher.winProbability_eq_of_gameEquivalent] [3, Lemma 4.15], and +by the fundamental lemma its advantage between their visible systems is +[at most its winning probability][Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent] +[3, Lemma 4.16], [4, Lemma 7 and Theorem 1 (i)]: to tell them apart, it must set the MBO. For +games replying at the queried label: + +```math +G\big(x^n, (y, 0)^n\big) = H\big(x^n, (y, 0)^n\big) +\quad \Longrightarrow \quad +\mathrm{Adv}_P(G^-, H^-) \le \Pr[P \text{ wins } G] = \Pr[P \text{ wins } H] . +``` + **Attachment**: the library defines the action of a PDC $`\alpha`$ on a game by its [MBO-forwarding lift][PDCBehavior.liftMBO] $`\hat\alpha`$: the lift runs $`\alpha`$, which does not see the inside MBOs, and gives each outside reply the MBO of the latest inside reply. CR18 states this @@ -944,14 +959,17 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [DDG]: src/RandomSystems/Game/DiscreteMBO.lean#L50 [PDG]: src/RandomSystems/Game/DiscreteMBO.lean#L54 [PDG.ofFunction]: src/RandomSystems/Game/FunctionGame.lean#L37 -[RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L290 -[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L299 -[DDE.blindMBO]: src/RandomSystems/Game/MBO.lean#L392 -[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L462 -[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L505 -[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L759 -[Domain.Distinguisher.winProbability_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L838 -[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L863 +[RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L305 +[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L314 +[DDE.blindMBO]: src/RandomSystems/Game/MBO.lean#L407 +[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L477 +[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L520 +[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L753 +[Domain.Distinguisher.winProbability_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L948 +[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L973 +[RandomSystem.GameEquivalent]: src/RandomSystems/Game/MBO.lean#L534 +[Domain.Distinguisher.winProbability_eq_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L857 +[Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L871 [PDCBehavior.liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L455 [PDCBehavior.liftMBO_id]: src/RandomSystems/Game/MBOAttachment.lean#L495 [PDCBehavior.liftMBO_comp]: src/RandomSystems/Game/MBOAttachment.lean#L1515 @@ -1229,14 +1247,14 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [not_supAgreement_disagreement_le_every_pair]: src/Probability/MultiCoupling.lean#L778 [supAgreement]: src/Probability/MultiCoupling.lean#L87 [supAgreement_eq_weight_overlapDist]: src/Probability/MultiCoupling.lean#L397 -[Distribution]: src/Probability/Distribution.lean#L54 -[ProbDist]: src/Probability/Distribution.lean#L147 -[isProbDist]: src/Probability/Distribution.lean#L126 -[mass]: src/Probability/Distribution.lean#L215 -[fTransform]: src/Probability/Distribution.lean#L547 -[prod]: src/Probability/Distribution.lean#L902 -[pi]: src/Probability/Distribution.lean#L1543 -[uniform]: src/Probability/Distribution.lean#L481 +[Distribution]: src/Probability/Distribution.lean#L55 +[ProbDist]: src/Probability/Distribution.lean#L148 +[isProbDist]: src/Probability/Distribution.lean#L127 +[mass]: src/Probability/Distribution.lean#L216 +[fTransform]: src/Probability/Distribution.lean#L587 +[prod]: src/Probability/Distribution.lean#L942 +[pi]: src/Probability/Distribution.lean#L1583 +[uniform]: src/Probability/Distribution.lean#L521 [statDist]: src/Probability/StatisticalDistance.lean#L88 [statDist_triangle]: src/Probability/StatisticalDistance.lean#L243 [statDist_fTransform_le]: src/Probability/StatisticalDistance.lean#L615 diff --git a/src/Probability/Distribution.lean b/src/Probability/Distribution.lean index beb6445..299bfe8 100644 --- a/src/Probability/Distribution.lean +++ b/src/Probability/Distribution.lean @@ -29,7 +29,8 @@ Lanzenberger–Maurer, *Coupling of Random Systems*, Definitions 1, 2 and 4. ## Main results -* the mass calculus: additivity, complements, monotonicity, `mass_le_weight` +* the mass calculus: additivity, complements, monotonicity, `mass_le_weight`; + `abs_mass_sub_le_of_le`: laws above a common part differ by at most the rest * pushforward: `mass_fTransform`, `weight_fTransform`, `fTransform_comp`, `fTransform_prod`, `fTransform_equiv_uniform` * products: `prod_apply`, `weight_prod`, `mass_prod_fst`, `mass_prod_snd`, @@ -341,6 +342,45 @@ theorem mass_mono {A : Type*} {X : Distribution A} (hX : X.NonNeg) {P Q : A → · simp [hP, h a hP] · by_cases hQ : Q a <;> simp [hP, hQ, hX a] +/-- **A common part bounds the difference of masses**: two laws of weight one that both lie +above `ν` differ on every event by at most the weight they do not share with `ν`, +`|μ₁(P) − μ₂(P)| ≤ 1 − |ν|`. -/ +theorem abs_mass_sub_le_of_le {A : Type*} {μ₁ μ₂ ν : Distribution A} (h₁ : μ₁.weight = 1) + (h₂ : μ₂.weight = 1) (hν₁ : ∀ a, ν a ≤ μ₁ a) (hν₂ : ∀ a, ν a ≤ μ₂ a) (P : A → Prop) : + |μ₁.mass P - μ₂.mass P| ≤ 1 - ν.weight := by + -- Plan. Each μ splits as ν + (μ − ν), with μ − ν ≥ 0 of weight 1 − |ν|. So + -- μ(P) − ν(P) = (μ − ν)(P) lies in [0, 1 − |ν|] for μ = μ₁ and μ = μ₂, and + -- |μ₁(P) − μ₂(P)| = |(μ₁(P) − ν(P)) − (μ₂(P) − ν(P))| ≤ 1 − |ν|. + -- Mass is additive, ν + (μ − ν) = μ: so (μ − ν)(P) = μ(P) − ν(P). + have hsub : ∀ μ : Distribution A, (μ - ν).mass P = μ.mass P - ν.mass P := by + intro μ + have := mass_add ν (μ - ν) P + rw [add_sub_cancel] at this + linarith + -- For μ of weight 1 above ν: 0 ≤ μ(P) − ν(P) ≤ 1 − |ν|. + have hbound : ∀ μ : Distribution A, μ.weight = 1 → (∀ a, ν a ≤ μ a) → + 0 ≤ μ.mass P - ν.mass P ∧ μ.mass P - ν.mass P ≤ 1 - ν.weight := by + intro μ hw hle + -- μ − ν ≥ 0 pointwise. + have hnn : (μ - ν).NonNeg := fun a => by + simp only [Finsupp.coe_sub, Pi.sub_apply, sub_nonneg] + exact hle a + rw [← hsub] + refine ⟨hnn.mass_nonneg P, ?_⟩ + -- |μ − ν| = |μ| − |ν| = 1 − |ν|: additivity on the sure event. + have hwt : (μ - ν).weight = 1 - ν.weight := by + have := mass_add ν (μ - ν) (fun _ => True) + rw [add_sub_cancel, mass_true, mass_true, mass_true, hw] at this + linarith + -- A mass of the nonnegative μ − ν is at most its weight. + rw [← hwt] + exact mass_le_weight hnn P + -- Both differences lie in [0, 1 − |ν|], so theirs is at most 1 − |ν| in absolute value. + obtain ⟨hlo₁, hhi₁⟩ := hbound μ₁ h₁ hν₁ + obtain ⟨hlo₂, hhi₂⟩ := hbound μ₂ h₂ hν₂ + rw [abs_le] + constructor <;> linarith + /-- **A single atom is below the mass of any event it satisfies**: `X a ≤ X(P)` when `P a`. Non-negativity is what makes the other summands harmless — the signed-carrier form of `Finset.single_le_sum` for `Distribution.mass`. diff --git a/src/RandomSystems/Game/MBO.lean b/src/RandomSystems/Game/MBO.lean index ce27923..faa7983 100644 --- a/src/RandomSystems/Game/MBO.lean +++ b/src/RandomSystems/Game/MBO.lean @@ -18,8 +18,15 @@ about the MBO: if the MBO is set with probability at most `ε` on every fixed se queries, every winner wins with probability at most `ε`, and the visible system is within `ε` of `T`. -Sources: CR18, §3.7.1 (games), Definition 4.5 (the winning probability), Definition 4.18 (the -visible system `S⁻`), Definition 4.19 (conditional equivalence), Lemma 4.16 and Theorem 4.17. +Two games are equivalent as games when they behave alike as long as the game is not won: they +give every transcript with every MBO unset the same probability. A distinguisher then wins both +alike, and its advantage between their visible systems is at most its winning probability: to +tell them apart it must set the MBO (the fundamental lemma). + +Sources: CR18, §3.7.1 (games), Definition 4.5 (the winning probability), Definition 4.16 +(equivalence as games `G ≡g H`), Lemmas 4.15 and 4.16, Definition 4.18 (the visible system +`S⁻`), Definition 4.19 (conditional equivalence), Theorem 4.17; Maurer 2002, Definition 5 +(`F^A ≡ G^C`), Lemma 6 (ii), Lemma 7 and Theorem 1 (i). ## Main definitions @@ -29,6 +36,7 @@ visible system `S⁻`), Definition 4.19 (conditional equivalence), Lemma 4.16 an * `DDE.blindMBO`, `finalMBO`, `RandomSystem.winProbability`, `Domain.Distinguisher.winProbability`: winning * `RandomSystem.unsetProbability`, `RandomSystem.ConditionallyEquivalent` +* `RandomSystem.GameEquivalent`: equivalence as games ## Main results @@ -36,6 +44,13 @@ visible system `S⁻`), Definition 4.19 (conditional equivalence), Lemma 4.16 an * `RandomSystem.abs_decisionProbability_sub_le_winProbability`, `Domain.Distinguisher.advantage_le_winProbability`: conditional equivalence bounds the advantage by the winning probability +* `RandomSystem.GameEquivalent.winProbability_eq`, + `Domain.Distinguisher.winProbability_eq_of_gameEquivalent`: games equivalent as games are won + alike +* `RandomSystem.GameEquivalent.abs_decisionProbability_sub_le`, + `Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent`: the fundamental lemma, + the advantage between the visible systems of games equivalent as games is at most the winning + probability * `RandomSystem.winProbability_le_of_unsetProbability`, `Domain.Distinguisher.winProbability_le_of_unsetProbability`: under conditional equivalence, the probability that the MBO is set on fixed queries bounds the winning probability @@ -508,6 +523,19 @@ def RandomSystem.ConditionallyEquivalent {𝒟 : Domain (Σ i, X i) (Σ i, Y i)} (T : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟) : Prop := ∀ h, G (unsetMBOs h) = G.unsetProbability (h.map Prod.fst) * T h +/-- **Equivalence as games** `G ≡g H` (CR18, Definition 4.16, printed p. 105: "Two +(probabilistic) games G and H are equivalent as games, denoted G ≡g H, if their pre-winning +behavior is identical"): the two games give every transcript with every MBO unset the same +probability. This is the equivalent cumulative condition CR18 states on the same page, +`p^G_{Yⁱ,Aᵢ=0|Xⁱ} = p^H_{Yⁱ,Aᵢ=0|Xⁱ}` for `i ≥ 1`, where on a game `Aᵢ = 0` means that every +MBO so far is unset (the product (4.36) of the pre-winning behavior). Maurer 2002, +Definition 5 (`F^A ≡ G^C`), is the same notion, with the event that a monotone condition holds +in place of the unset MBO. -/ +def RandomSystem.GameEquivalent {D₁ D₂ : Domain (Σ i, X i) (Σ i, withMBO Y i)} + (G : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) D₁) + (H : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) D₂) : Prop := + ∀ h, G (unsetMBOs h) = H (unsetMBOs h) + variable {E : List (Σ i, X i) → Prop} {m : ℕ} {hE : ∀ h, E h → h.length ≤ m} /-- A random system on the input domain admits the fixed queries of a possible transcript of @@ -665,11 +693,10 @@ theorem RandomSystem.abs_decisionProbability_sub_le_winProbability -- Step 2. ν ≤ μV: G (h with every MBO 0) is one term of G⁻ h, the sum over the MBOs. -- Step 3. ν ≤ μT: by conditional equivalence, G (h with every MBO 0) -- = Pr[MBO stays 0 on h's queries] · T h ≤ T h. - -- Step 4. If μ₁ has weight 1 and ν ≤ μ₁, then 0 ≤ μ₁(P) − ν(P) ≤ 1 − weight ν. - -- Step 5. The chain: + -- Step 4. The chain, as μV and μT have weight 1 and lie above ν (Steps 2 and 3): -- |p_D(G⁻) − p_D(T)| - -- = |(μV(P) − ν(P)) − (μT(P) − ν(P))| (subtract and add ν(P)) - -- ≤ 1 − weight ν (Steps 2–4: both lie in [0, 1 − weight ν]) + -- = |μV(P) − μT(P)| + -- ≤ 1 − weight ν (Distribution.abs_mass_sub_le_of_le) -- = Γ_D(G) (Step 1) set e := ddeOf hD set n := hD.2.1.choose @@ -714,44 +741,11 @@ theorem RandomSystem.abs_decisionProbability_sub_le_winProbability -- Both transcript laws have weight 1. have hμV := G.visible.sLaw_isProbDist hV n have hμT := T.sLaw_isProbDist hTc n - -- Step 4. Bound the part of μV and μT beyond ν. - -- Masses of the differences. - have hsub : ∀ (μ₁ : Distribution (List ((Σ i, X i) × Σ i, Y i))) - (P : List ((Σ i, X i) × Σ i, Y i) → Prop), - (μ₁ - ν).mass P = μ₁.mass P - ν.mass P := by - intro μ₁ P - -- Mass is additive: ν + (μ₁ − ν) = μ₁. - have := Distribution.mass_add ν (μ₁ - ν) P - rw [add_sub_cancel] at this - linarith - -- If μ₁ has weight 1 and ν ≤ μ₁, then μ₁ − ν is nonnegative with weight 1 − weight ν, so - -- each of its masses lies in [0, 1 − weight ν]. - have hbound : ∀ μ₁ : Distribution (List ((Σ i, X i) × Σ i, Y i)), μ₁.weight = 1 → - (∀ h, ν h ≤ μ₁ h) → ∀ P, 0 ≤ μ₁.mass P - ν.mass P ∧ - μ₁.mass P - ν.mass P ≤ 1 - ν.weight := by - intro μ₁ hw hle P - -- μ₁ − ν ≥ 0 pointwise. - have hnn : (μ₁ - ν).NonNeg := fun h => by - simp only [Finsupp.coe_sub, Pi.sub_apply, sub_nonneg] - exact hle h - rw [← hsub] - refine ⟨hnn.mass_nonneg P, ?_⟩ - -- weight (μ₁ − ν) = weight μ₁ − weight ν = 1 − weight ν. - have hwt : (μ₁ - ν).weight = 1 - ν.weight := by - rw [← Distribution.mass_true, hsub, Distribution.mass_true, Distribution.mass_true, hw] - rw [← hwt] - exact Distribution.mass_le_weight hnn P - -- Step 5. Step 4 for μV and for μT, with P = "D decides 1". - obtain ⟨h1, h2⟩ := hbound μV hμV.2 hνV + -- Step 4. Γ_D(G) = 1 − weight ν; the decision probabilities are, by definition, μV(P) and + -- μT(P) with P = "D decides 1", which lie above the common part ν. + rw [hwin] + exact Distribution.abs_mass_sub_le_of_le hμV.2 hμT.2 hνV hνT (fun h => ⟨.dec, true⟩ ∈ (trim D) (dHist (h.map Prod.snd))) - obtain ⟨h3, h4⟩ := hbound μT hμT.2 hνT - (fun h => ⟨.dec, true⟩ ∈ (trim D) (dHist (h.map Prod.snd))) - -- Γ_D(G) = 1 − weight ν; |a| ≤ c is −c ≤ a ∧ a ≤ c. - rw [hwin, abs_le] - -- The decision probabilities are μV(P) and μT(P) by definition. - change -(1 - ν.weight) ≤ μV.mass _ - μT.mass _ ∧ μV.mass _ - μT.mass _ ≤ 1 - ν.weight - -- Both inequalities follow from Step 4 by linear arithmetic. - constructor <;> linarith /-- **Conditional equivalence bounds distinguishing by winning** (CR18, Lemma 4.16 and Theorem 4.17): a distinguisher's advantage between the visible system of a game and a random @@ -782,6 +776,122 @@ theorem Domain.Distinguisher.advantage_le_winProbability (RandomSystem.abs_decisionProbability_sub_le_winProbability hG hT hm hc D.1 D.2.1 D.2.2) (P.2.1 D) +/-- **Games equivalent as games are won alike**, by a deterministic distinguisher (CR18, +Lemma 4.15, printed p. 106: "If G ≡g H then, for any winner W for (X, Y)-games, we have +Ḡ = H̄"; Maurer 2002, Lemma 7: "P^{DF}(Āₖ) = P^{DG}(B̄ₖ)"). -/ +theorem RandomSystem.GameEquivalent.winProbability_eq + {G H : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE)} + (hG : G.RepliesAtQueriedInterface) (hH : H.RepliesAtQueriedInterface) + (hmG : G.MonotoneMBO) (hmH : H.MonotoneMBO) (he : G.GameEquivalent H) + (D : DDD I X Y) (hD : IsDDD D) + (hdc : (Domain.ofInputs E m hE : Domain (Σ i, X i) (Σ i, Y i)).DecisionCompatible D) : + G.winProbability D hD = H.winProbability D hD := by + -- Γ_D(K) = 1 − weight ν_K for K = G, H, where ν_K h = K (h with every MBO 0) on the + -- transcripts h complete for D's environment (exists_unset_winProbability). Equivalence as + -- games makes ν_G = ν_H, so Γ_D(G) = Γ_D(H). + obtain ⟨ν, hν, hwin⟩ := G.exists_unset_winProbability hG hmG D hD hdc + obtain ⟨ν', hν', hwin'⟩ := H.exists_unset_winProbability hH hmH D hD hdc + -- ν_G = ν_H pointwise: G and H agree on every transcript with every MBO 0. + have hνν : ν = ν' := Finsupp.ext fun h => by rw [hν, hν', he h] + rw [hwin, hwin', hνν] + +open scoped Classical in +/-- **The fundamental lemma**, for a deterministic distinguisher (CR18, Lemma 4.16, printed +p. 107: "if S ≡g T, then the distinguishing advantage of any distinguisher D in distinguishing +S⁻ and T⁻ is upper bounded by D's winning probability for game S"; Maurer 2002, Lemma 7). -/ +theorem RandomSystem.GameEquivalent.abs_decisionProbability_sub_le + {G H : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE)} + (hG : G.RepliesAtQueriedInterface) (hH : H.RepliesAtQueriedInterface) + (hmG : G.MonotoneMBO) (he : G.GameEquivalent H) + (D : DDD I X Y) (hD : IsDDD D) + (hdc : (Domain.ofInputs E m hE : Domain (Σ i, X i) (Σ i, Y i)).DecisionCompatible D) : + |G.visible.decisionProbability D hD - H.visible.decisionProbability D hD| ≤ + G.winProbability D hD := by + -- Plan. D plays the visible systems G⁻ and H⁻ through its environment e for n rounds: + -- + -- ┌───┐ ──x──▶ ┌───┐ ┌───┐ ──x──▶ ┌───┐ + -- │ D │ │ G │ ──▶ a (dropped) │ D │ │ H │ ──▶ a (dropped) + -- └───┘ ◀──y── └───┘ └───┘ ◀──y── └───┘ + -- + -- The transcript laws of G⁻ and H⁻ with e have weight 1; P is the event "D decides 1", so + -- that the decision probabilities are their masses of P. + -- Step 1. ν h = G (h with every MBO 0) on the h complete for e, and D's winning + -- probability is Γ_D(G) = 1 − weight ν. + -- Step 2. By equivalence as games, ν h = H (h with every MBO 0) as well. + -- Step 3. ν lies below both transcript laws: K (h with every MBO 0) is one term of K⁻ h, + -- the sum over the MBOs, for K = G and K = H. + -- Step 4. The chain: + -- |p_D(G⁻) − p_D(H⁻)| ≤ 1 − weight ν (Distribution.abs_mass_sub_le_of_le) + -- = Γ_D(G) (Step 1) + set e := ddeOf hD + set n := hD.2.1.choose + -- G⁻ and H⁻ are compatible with e, as D is compatible with the input domain. + have henv := hdc.environment hD + -- Step 1. ν, with Γ_D(G) = 1 − weight ν. + obtain ⟨ν, hν, hwin⟩ := G.exists_unset_winProbability hG hmG D hD hdc + -- Step 3, for any game K that ν describes: ν ≤ the transcript law of K⁻ with e. + have below : ∀ K : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE), + (∀ h, ν h = if Good e.1 n h then K (unsetMBOs h) else 0) → + ∀ h, ν h ≤ K.visible.sLaw e.1 n h := by + intro K hK h + rw [hK, sLaw_apply] + -- Split on whether h is complete for e; if not, both sides are 0. + split_ifs + -- le_sumMBO: K (h with every MBO 0) ≤ sumMBO K h = K⁻ h. + · have := le_sumMBO K.mass_nonneg (unsetMBOs h) + rwa [forgetMBOs_unsetMBOs, ← RandomSystem.visible_apply] at this + · exact le_rfl + -- Step 2. ν describes H too: G and H agree on every transcript with every MBO 0. + have hνH : ∀ h, ν h = if Good e.1 n h then H (unsetMBOs h) else 0 := fun h => by + rw [hν, he h] + -- Step 4. Γ_D(G) = 1 − weight ν; both transcript laws have weight 1 and lie above ν. + rw [hwin] + exact Distribution.abs_mass_sub_le_of_le + (G.visible.sLaw_isProbDist (henv _ hG.visible) n).2 + (H.visible.sLaw_isProbDist (henv _ hH.visible) n).2 (below G hν) (below H hνH) + (fun h => ⟨.dec, true⟩ ∈ (trim D) (dHist (h.map Prod.snd))) + +/-- **Games equivalent as games are won alike** (CR18, Lemma 4.15; Maurer 2002, Lemma 7, and +Lemma 6 (ii) for the best winner): each distinguisher, used as a winner, wins two games +equivalent as games with the same probability. -/ +theorem Domain.Distinguisher.winProbability_eq_of_gameEquivalent + (P : (Domain.ofInputs E m hE : Domain (Σ i, X i) (Σ i, Y i)).Distinguisher) + {G H : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE)} + (hG : G.RepliesAtQueriedInterface) (hH : H.RepliesAtQueriedInterface) + (hmG : G.MonotoneMBO) (hmH : H.MonotoneMBO) (he : G.GameEquivalent H) : + P.winProbability G = P.winProbability H := by + -- Γ_P(K) = Σ_D P(D)·Γ_D(K), and Γ_D(G) = Γ_D(H) for each deterministic D. + simp only [Domain.Distinguisher.winProbability] + exact Finsupp.sum_congr fun D _ => by + rw [he.winProbability_eq hG hH hmG hmH D.1 D.2.1 D.2.2] + +/-- **The fundamental lemma** (CR18, Lemma 4.16; Maurer 2002, Lemma 7, and Theorem 1 (i) for +the best distinguisher): a distinguisher's advantage between the visible systems of two games +equivalent as games is at most its winning probability for the first. -/ +theorem Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent + (P : (Domain.ofInputs E m hE : Domain (Σ i, X i) (Σ i, Y i)).Distinguisher) + {G H : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE)} + (hG : G.RepliesAtQueriedInterface) (hH : H.RepliesAtQueriedInterface) + (hmG : G.MonotoneMBO) (he : G.GameEquivalent H) : + |P.probability G.visible - P.probability H.visible| ≤ P.winProbability G := by + -- P is a distribution over deterministic distinguishers D, with weights P(D) ≥ 0: + -- |Σ_D P(D)·p_D(G⁻) − Σ_D P(D)·p_D(H⁻)| + -- = |Σ_D P(D)·(p_D(G⁻) − p_D(H⁻))| + -- ≤ Σ_D P(D)·|p_D(G⁻) − p_D(H⁻)| (triangle inequality, P(D) ≥ 0) + -- ≤ Σ_D P(D)·Γ_D(G) (the deterministic case) + -- = Γ_P(G) + simp only [Domain.Distinguisher.probability, Domain.Distinguisher.winProbability, + Finsupp.sum] + -- The difference of the sums is the sum of the differences. + rw [← Finset.sum_sub_distrib] + -- Triangle inequality, then compare termwise. + refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum fun D _ => ?_) + -- |P(D)·a − P(D)·b| = P(D)·|a − b|, as P(D) ≥ 0. + rw [← mul_sub, abs_mul, abs_of_nonneg (P.2.1 D)] + -- The deterministic case, scaled by P(D) ≥ 0. + exact mul_le_mul_of_nonneg_left (he.abs_decisionProbability_sub_le hG hH hmG D.1 D.2.1 D.2.2) + (P.2.1 D) + open scoped Classical in /-- **Winning on fixed queries bounds winning**, for a deterministic distinguisher: a game conditionally equivalent to a random system, whose MBO stays unset with probability at least diff --git a/src/Tests/Axioms/Systems.lean b/src/Tests/Axioms/Systems.lean index 503b456..fc5d3aa 100644 --- a/src/Tests/Axioms/Systems.lean +++ b/src/Tests/Axioms/Systems.lean @@ -182,6 +182,10 @@ parallel composition, distance and games, and the counterexamples, depend only o #print axioms SystemAlgebra.RandomSystem.visible #print axioms SystemAlgebra.RandomSystem.abs_decisionProbability_sub_le_winProbability #print axioms SystemAlgebra.Domain.Distinguisher.advantage_le_winProbability +#print axioms SystemAlgebra.RandomSystem.GameEquivalent.winProbability_eq +#print axioms SystemAlgebra.RandomSystem.GameEquivalent.abs_decisionProbability_sub_le +#print axioms SystemAlgebra.Domain.Distinguisher.winProbability_eq_of_gameEquivalent +#print axioms SystemAlgebra.Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent #print axioms SystemAlgebra.Domain.Distinguisher.winProbability_le_of_unsetProbability #print axioms SystemAlgebra.RandomSystem.transcriptDistance_visible_le_of_unsetProbability