SurrogateFibers.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The surrogate perturbation fixes the complementary table exactly. Splitting the actual uniform matrix law therefore expresses surrogate acceptance as the mean of the uniform shortcode tests on the (U,T) fibers, including zero perturbation factors. This supplies the sampling identification needed before applying the inverse theorem to the many useful fibers.

def OAI.MaxCutGames.Decoder.SurrogateFibers.shortcodeAcceptance line 35
Source documentation
Uniform shortcode sampling; neither nonzero-factor conditioning nor rank-one-matrix-uniform sampling is substituted for its two independent factors.
```
def shortcodeAcceptance (f : (E →ₗ[F2] K) → C) : ℝ := by
…
```
theorem OAI.MaxCutGames.Decoder.SurrogateFibers.product_perturbation line 41
theorem OAI.MaxCutGames.Decoder.SurrogateFibers.surrogate_acceptance_eq_fiber_average line 47
theorem OAI.MaxCutGames.Decoder.ActualSpectral.expect_prod line 92
theorem OAI.MaxCutGames.Decoder.ActualSpectral.expect_eq_uniform_sum line 97
theorem OAI.MaxCutGames.Decoder.ActualSpectral.eigenvalue_eq_kernelProbability line 104
Source documentation
The finite noise law's multiplier is exactly the rational kernel event of the same gadget, cast to the real numbers.
```
theorem eigenvalue_eq_kernelProbability {s d : Nat} (g : SplitGadget s d)
    {P : Type} [AddCommGroup P] [Module F2 P] (S : Ambient s d →ₗ[F2] P) :
    linearNoiseEigenvalue (samplerLaw g.noise) S =
      (Integration.SplitGadget.kernelProbability g S : ℝ) := by
…
```
Mentions: OAI.MaxCutGames.Integration.SplitGadget.kernelProbability

theorem OAI.MaxCutGames.Decoder.ActualSpectral.acceptance_nested line 114

Source documentation

The four independent samples of the actual single-orbit test.

theorem acceptance_nested (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (label : Fin (vertexCount S k s d) → Fin (2 ^ s)) :
    (acceptanceProbability S k g label : ℝ) =
      𝔼 U : Question S k, 𝔼 X : Map k s d, 𝔼 i : g.NoiseIndex, 𝔼 l : Dual k,
        if unfolded S k s d label (U, X) =
          unfolded S k s d label (U, X + l.smulRight (g.noise i))
        then (1 : ℝ) else 0 := by
…

theorem OAI.MaxCutGames.Decoder.ActualSpectral.acceptance_eq_equality_mean line 137

Source documentation

No auxiliary side labeling is introduced: the same restored table occurs on both sides of the actual equality test.

theorem acceptance_eq_equality_mean (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (label : Fin (vertexCount S k s d) → Fin (2 ^ s)) :
    (acceptanceProbability S k g label : ℝ) =
      𝔼 U : Question S k,
        equalityAcceptance (samplerLaw g.noise) (fun X : Map k s d =>
          unfolded S k s d label (U, X)) := by
…

def OAI.MaxCutGames.Decoder.ActualSpectral.fiberAcceptance line 156
theorem OAI.MaxCutGames.Decoder.ActualSpectral.fiberAcceptance_le_one line 162
theorem OAI.MaxCutGames.Decoder.ActualSpectral.weighted_fiber_mean_lower line 175
theorem OAI.MaxCutGames.Decoder.ActualSpectral.actual_fiber_mean_lower line 197
def OAI.MaxCutGames.Decoder.ActualSpectral.eta line 218
theorem OAI.MaxCutGames.Decoder.ActualSpectral.eta_pos line 220

theorem OAI.MaxCutGames.Decoder.ActualSpectral.actual_good_fiber_mass line 224

Source documentation

At least 10 η of the actual (U,T) pairs have shortcode acceptance at least 4 η, exactly the input needed by row erasure.

theorem actual_good_fiber_mass (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (label : Fin (vertexCount S k s d) → Fin (2 ^ s)) (r : Nat)
    (hkernel : ∀ L : Ambient s d →ₗ[F2] ActualHomogeneous.E k,
      r ≤ Module.finrank F2 (L.comp (alphabetEmbedding s d)).range →
      Integration.SplitGadget.kernelProbability g L ≤ 7 / 8)
    (haccept : (99 : ℚ) / 100 ≤ acceptanceProbability S k g label) :
    10 * eta r ≤ 𝔼 U : Question S k,
      𝔼 T : ActualHomogeneous.E k →ₗ[F2] Vector d,
        if 4 * eta r ≤ fiberAcceptance S k s d label U T then (1 : ℝ) else 0 := by
…

Mentions: OAI.MaxCutGames.Integration.SplitGadget.kernelProbability, OAI.MaxCutGames.Decoder.ActualSpectral.eta, OAI.MaxCutGames.Decoder.ActualSpectral.fiberAcceptance