StageData.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Constant-detection enlargement endpoint

The finite base alphabet and its rank threshold are fixed before the target logical space. The resulting actual gadget has the same nonlinear error and linear kernel error at most 7/8. Only the common data and experiment interface is reused from the old gadget namespace.

def OAI.MaxCutGames.Gadget.StageData.toData line 18
Source documentation
The normalized stage's actual data, with its original finite noise choices. Passing the inclusion explicitly avoids dependent casts of the shift carrier.
```
def toData (s : Stage (ZMod 2) C) (embed : C →ₗ[ZMod 2] s.Input)
    (hinj : Function.Injective embed)
    (hEquiv : ∀ u c, s.output (u + embed c) = s.output u + c) : ActualGadget.Data C where
…
```
Mentions: OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.ActualGadget.Data
theorem OAI.MaxCutGames.Gadget.StageData.count_probability_eq_expect line 32
Source documentation
Intrinsic count probability and uniform finite expectation are identical.
```
theorem count_probability_eq_expect {Ω : Type*} [Fintype Ω] (p : Ω → Prop) :
    Enlargement.probability p = 𝔼 x : Ω, if p x then (1 : ℚ) else 0 := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Enlargement.probability
theorem OAI.MaxCutGames.Gadget.StageData.count_probability_eq_harmonic line 39
theorem OAI.MaxCutGames.Gadget.StageData.stabilityError_toData line 47
theorem OAI.MaxCutGames.Gadget.StageData.stabilityError_toData_count line 61
theorem OAI.MaxCutGames.Gadget.StageData.error_eq_count_probability line 78
theorem OAI.MaxCutGames.Gadget.StageData.kernelError_toData_count line 91

theorem OAI.MaxCutGames.Gadget.StageData.kernelError_eq_one_sub_detection line 105

Source documentation

The common interface's zero-image error is exactly the complement of the v2 nonzero-image detection probability.

theorem kernelError_eq_one_sub_detection (s : Stage (ZMod 2) C) [Fintype s.Noise]
    (embed : C →ₗ[ZMod 2] s.Input) (hinj : Function.Injective embed)
    (hEquiv : ∀ u c, s.output (u + embed c) = s.output u + c)
    {E : Type} [AddCommGroup E] [Module (ZMod 2) E] (T : s.Input →ₗ[ZMod 2] E) :
    ActualGadget.kernelError (toData s embed hinj hEquiv) T =
      1 - Enlargement.probability (fun n : s.Noise => T (s.noise n) ≠ 0) := by
…

Mentions: OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.ActualGadget.kernelError, OAI.MaxCutGames.Gadget.StageData.toData, OAI.MaxCutGames.Gadget.Enlargement.probability

theorem OAI.MaxCutGames.Gadget.StageData.kernelError_le_of_detection line 126
def OAI.MaxCutGames.Gadget.EnlargementEndpoint.data line 160

theorem OAI.MaxCutGames.Gadget.EnlargementEndpoint.data_satisfies line 170

Source documentation

Base stability and base detection suffice for the complete enlarged gadget. Its detection error is the fixed constant 7/8, as required by v2.

theorem data_satisfies (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0) (p : ℚ)
    (hchange : probability (fun z : V × N => C (z.1 + noise z.2) ≠ C z.1) ≤ p)
    (hbase : ∀ (E : Type) [AddCommGroup E] [Module (ZMod 2) E]
      (U : V →ₗ[ZMod 2] E), Function.Injective (U.comp i) →
        1 / 4 ≤ probability (fun n : N => U (noise n) ≠ 0)) :
    ActualGadget.Satisfies (data i hi C hC noise hdim b₀ hb₀) p (7 / 8)
      (Module.finrank (ZMod 2) B + 2) := by
…

Mentions: OAI.MaxCutGames.Gadget.ActualGadget.Satisfies, OAI.MaxCutGames.Gadget.EnlargementEndpoint.data

theorem OAI.MaxCutGames.Gadget.EnlargementEndpoint.exists_data line 201

Source documentation

For every permitted logical space there is an actual gadget. The rank threshold dim B + 2 and all base data are independent of that space.

theorem exists_data (i : B →ₗ[ZMod 2] V) (hi : Function.Injective i)
    (C : V → B) (hC : ∀ x b, C (x + i b) = C x + b) (noise : N → V)
    (hdim : Module.finrank (ZMod 2) B ≤ Module.finrank (ZMod 2) K)
    (b₀ : B) (hb₀ : b₀ ≠ 0) (p : ℚ)
    (hchange : probability (fun z : V × N => C (z.1 + noise z.2) ≠ C z.1) ≤ p)
    (hbase : ∀ (E : Type) [AddCommGroup E] [Module (ZMod 2) E]
      (U : V →ₗ[ZMod 2] E), Function.Injective (U.comp i) →
        1 / 4 ≤ probability (fun n : N => U (noise n) ≠ 0)) :
    ∃ g : ActualGadget.Data K,
      ActualGadget.Satisfies g p (7 / 8) (Module.finrank (ZMod 2) B + 2) :=
…

Mentions: OAI.MaxCutGames.Gadget.ActualGadget.Data, OAI.MaxCutGames.Gadget.ActualGadget.Satisfies

theorem OAI.MaxCutGames.Gadget.exists_actual_gadget line 227
Source documentation
Actual finite gadget data, with a rank threshold independent of the final logical dimension and an arbitrarily small nonlinear change probability.
```
theorem exists_actual_gadget (p : ℚ) (hp : 0 < p) :
    ∃ r : ℕ, 1 ≤ r ∧ ∀ ℓ : ℕ, r ≤ ℓ →
      ∃ g : MaxCutGames.Gadget.ActualGadget.Data (Vector ℓ),
        MaxCutGames.Gadget.ActualGadget.Satisfies g p (7 / 8) r := by
…
```
Mentions: OAI.MaxCutGames.Gadget.ActualGadget.Data, OAI.MaxCutGames.Gadget.ActualGadget.Satisfies
theorem OAI.MaxCutGames.Gadget.exists_split_gadget line 276