OAI/Computability/UniqueGames/Decoding/ActualSpectralLemmas.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

The two full-table events used in the projected-witness transfer. Their sample space contains actual occurrence tuples and complete affine tables, but no projection choice. The selected witness depends on row advice only.

  1. theorem OAI.UniqueGamesTheorem.Decoder.ActualSpectral.expect_prod line 32
  2. theorem OAI.UniqueGamesTheorem.Decoder.ActualSpectral.expect_eq_uniform_sum line 37
  3. theorem OAI.UniqueGamesTheorem.Decoder.ActualSpectral.eigenvalue_eq_kernelProbability line 44

    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.UniqueGamesTheorem.Integration.SplitGadget.kernelProbability

  4. theorem OAI.UniqueGamesTheorem.Decoder.ActualSpectral.acceptance_nested line 54

    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
…
  5. theorem OAI.UniqueGamesTheorem.Decoder.ActualSpectral.acceptance_eq_equality_mean line 77

    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
…
  6. def OAI.UniqueGamesTheorem.Decoder.ActualSpectral.fiberAcceptance line 96
  7. theorem OAI.UniqueGamesTheorem.Decoder.ActualSpectral.fiberAcceptance_le_one line 102
  8. theorem OAI.UniqueGamesTheorem.Decoder.ActualSpectral.weighted_fiber_mean_lower line 115
  9. theorem OAI.UniqueGamesTheorem.Decoder.ActualSpectral.actual_fiber_mean_lower line 137
  10. def OAI.UniqueGamesTheorem.Decoder.ActualSpectral.eta line 158
  11. theorem OAI.UniqueGamesTheorem.Decoder.ActualSpectral.eta_pos line 160
  12. theorem OAI.UniqueGamesTheorem.Decoder.ActualSpectral.actual_good_fiber_mass line 164

    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.UniqueGamesTheorem.Integration.SplitGadget.kernelProbability, OAI.UniqueGamesTheorem.Decoder.ActualSpectral.eta, OAI.UniqueGamesTheorem.Decoder.ActualSpectral.fiberAcceptance

  13. def OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.table line 213
  14. theorem OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.table_acceptance line 220
  15. def OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.adviceMass line 240

    Source documentation

    The row-advice probability in actual matrix coordinates. In particular, dependent rows of A are sampled with their full multiplicity.

    def adviceMass (S : Source) (k s d r : ℕ)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s)) (α : ℝ) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount

  16. def OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.goodRowMass line 247
  17. theorem OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.goodRowMass_pos line 250
  18. theorem OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.exists_actual_advice_threshold line 255
  19. abbrev OAI.UniqueGamesTheorem.Decoder.ActualEvents.Context line 315
  20. abbrev OAI.UniqueGamesTheorem.Decoder.ActualEvents.Sample line 318
  21. abbrev OAI.UniqueGamesTheorem.Decoder.ActualEvents.FullTableSample line 321
  22. def OAI.UniqueGamesTheorem.Decoder.ActualEvents.fullTableEquiv line 326

    Source documentation

    A bijection merely rearranges the full sampled table and changes its matrix coordinates. It never appends the hidden projection to this law.

    def fullTableEquiv (S : Source) (k s d r : ℕ) :
    FullTableSample S k s d r ≃ Sample S k s d r where
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.ActualEvents.FullTableSample, OAI.UniqueGamesTheorem.Decoder.ActualEvents.Sample

  23. def OAI.UniqueGamesTheorem.Decoder.ActualEvents.unrestricted line 361
  24. def OAI.UniqueGamesTheorem.Decoder.ActualEvents.sliceEvent line 364
  25. def OAI.UniqueGamesTheorem.Decoder.ActualEvents.targetHit line 370
  26. theorem OAI.UniqueGamesTheorem.Decoder.ActualEvents.targetHit_implies_slice line 376
  27. theorem OAI.UniqueGamesTheorem.Decoder.ActualEvents.uniform_probability_expect line 384
  28. theorem OAI.UniqueGamesTheorem.Decoder.ActualEvents.unrestricted_slice_mass line 391
  29. theorem OAI.UniqueGamesTheorem.Decoder.ActualEvents.unrestricted_match_mass line 405
  30. theorem OAI.UniqueGamesTheorem.Decoder.ActualEvents.slice_probability_lower line 428

    Source documentation

    The full-table slice event pays exactly one bounded column-fiber factor.

    theorem slice_probability_lower (S : Source) (k s d r : ℕ)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s)) (α g₀ : ℝ)
    (hgood : g₀ ≤ ActualGoodRows.adviceMass S k s d r labeling α) :
    g₀ * (1 / (2 : ℝ) ^ (s * r)) ≤
      (unrestricted S k s d r).probability (sliceEvent S k s d r labeling α) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.adviceMass, OAI.UniqueGamesTheorem.Decoder.ActualEvents.unrestricted, OAI.UniqueGamesTheorem.Decoder.ActualEvents.sliceEvent

  31. theorem OAI.UniqueGamesTheorem.Decoder.ActualEvents.target_probability_lower line 439
  32. structure OAI.UniqueGamesTheorem.Decoder.MatrixGapChoice.InverseParameters line 464

    Source documentation

    Fixed dimensions, density and sparse mask for one logical alphabet. The remaining gadget codimension may be arbitrary when choosing the cube.

    structure InverseParameters (rstar : ℕ) where
…
  33. theorem OAI.UniqueGamesTheorem.Decoder.MatrixGapChoice.eta_lt_one line 486
  34. theorem OAI.UniqueGamesTheorem.Decoder.MatrixGapChoice.exists_inverse_parameters line 494
  35. theorem OAI.UniqueGamesTheorem.Decoder.MatrixGapChoice.exists_cube line 533

    Source documentation

    After all fixed dimensions are known, the cube simultaneously exceeds the inverse threshold, reduces full-table variation, and beats the decoder mass.

    theorem exists_cube {rstar : ℕ} (P : InverseParameters rstar) (d : ℕ) :
    ∃ m : ℕ, 0 < m ∧ P.tupleThreshold ≤ m ^ 3 ∧
      0 ≤ 1 / (m : ℝ) ^ 2 ∧ 1 / (m : ℝ) ^ 2 ≤ 1 ∧
      Foundations.Information.totalVariation
        (SparseLaw.independentWeights
          (SparseLaw.mixture (1 / (m : ℝ) ^ 2)
            (SparseLaw.singletonPairWeights (Ambient P.s d))) (m ^ 3))
        (SparseLaw.uniformWeights (Fin (m ^ 3) → Ambient P.s d × Ambient P.s d)) ≤
          ConstantSelection.variationBudget P.α (ActualGoodRows.goodRowMass rstar P.s P.r) P.s P.r ∧
      (1 - ((1 / (m : ℝ) ^ 2) / (2 : ℝ) ^ (d + P.r)) / 3600) ^ (m ^ 3) <
        ConstantSelection.decodingMass P.α (ActualGoodRows.goodRowMass rstar P.s P.r) P.s P.r := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.MatrixGapChoice.InverseParameters, OAI.UniqueGamesTheorem.Foundations.Information.totalVariation, OAI.UniqueGamesTheorem.Decoder.SparseLaw.independentWeights, OAI.UniqueGamesTheorem.Decoder.SparseLaw.mixture, OAI.UniqueGamesTheorem.Decoder.SparseLaw.singletonPairWeights, OAI.UniqueGamesTheorem.Decoder.SparseLaw.uniformWeights, OAI.UniqueGamesTheorem.Decoder.ConstantSelection.variationBudget, OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.goodRowMass, OAI.UniqueGamesTheorem.Decoder.ConstantSelection.decodingMass