PrivateStrategyLemmas.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Actual private response laws for Fourier decoding

The right response law has only its row-fiber table, the inclusion of its hidden kernel, a first-bit map, and an actual fallback answer as arguments. In particular it has no column slice or witness. Zero-mass invalid frequencies are repaired to the fallback so that the response type always consists of actual answers. Witness data occur only in the success analysis.

def OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.candidates line 36
theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.mem_candidates line 39
theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.candidates_nonempty line 42
theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.candidates_card_le line 46
theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.candidates_card_le_pow line 58

theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.candidate_preimage line 72

Source documentation

First-bit preservation converts a projected coset member into an actual answer in the left candidate set.

theorem candidate_preimage (Z : Submodule F2 E) (z : E)
    (π : E →ₗ[F2] E') (τ : E →ₗ[F2] F2) (τ' : E' →ₗ[F2] F2)
    (hτ : τ'.comp π = τ) (y : E') (hy : y - π z ∈ Z.map π)
    (hybit : τ' y = 1) : ∃ v ∈ candidates Z z τ, π v = y := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.candidates

theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.exists_unit line 96
def OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.chooseUnit line 106
theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.chooseUnit_spec line 110
abbrev OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.ActualAnswer line 113
def OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.privateSeedLaw line 116
Source documentation
The uniform output character followed by its actual Fourier frequency.
```
def privateSeedLaw (F : (E →ₗ[F2] H) → K) :
    FiniteDistribution ((K →ₗ[F2] F2) × (H →ₗ[F2] E)) where
…
```
theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.privateSeedLaw_expectation line 126
def OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.privateOutput line 137
Source documentation
The decoder receives no left witness. The first-bit repair affects only zero-mass frequencies when the table is folded.
```
def privateOutput (ι : H →ₗ[F2] K) (τ : E →ₗ[F2] F2)
    (fallback : ActualAnswer τ) (p : (K →ₗ[F2] F2) × (H →ₗ[F2] E)) :
    ActualAnswer τ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.ActualAnswer
theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.privateOutput_eq_contraction line 145
def OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.privateLaw line 160
Source documentation
This is an actual finite distribution on actual answers, for every visible row table. The sampler's normalization is Parseval, not a hypothesis.
```
def privateLaw [Fintype E] (F : (E →ₗ[F2] H) → K)
    (ι : H →ₗ[F2] K) (τ : E →ₗ[F2] F2) (fallback : ActualAnswer τ) :
    FiniteDistribution (ActualAnswer τ) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.ActualAnswer
theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.privateLaw_expectation line 165
def OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.candidateLaw line 180
Source documentation
The left rule is uniform on its own chosen affine-answer candidates.
```
def candidateLaw (Z : Submodule F2 E) (z : E) (τ : E →ₗ[F2] F2)
    (hz : τ z = 1) : FiniteDistribution (ActualAnswer τ) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.ActualAnswer
theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.candidateLaw_expectation line 187

def OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.conditionalAgreement line 212

Source documentation

Actual independent response-law success, with the literal projection test.

def conditionalAgreement (Z : Submodule F2 U) (z : U)
    (τU : U →ₗ[F2] F2) (hz : τU z = 1) (π : U →ₗ[F2] E)
    (F : (E →ₗ[F2] H) → K) (ι : H →ₗ[F2] K)
    (τ : E →ₗ[F2] F2) (fallback : ActualAnswer τ) : ℝ :=
…

Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.ActualAnswer

theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.conditionalAgreement_eq_sum line 219
def OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.goodCosetMass line 249
Source documentation
The exact good Fourier mass in a witness coset; unlike the response law, this analysis-only quantity is allowed to mention the witness.
```
def goodCosetMass (Q : Submodule F2 E) (z' : E)
    (F : (E →ₗ[F2] H) → K) (ι : H →ₗ[F2] K) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.goodCosetMass_nonneg line 256

theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.good_frequency_preimage line 268

Source documentation

A good sampled frequency has a valid left preimage. Neither decoder is given the proof or the witness used here.

theorem good_frequency_preimage (Z : Submodule F2 U) (z : U)
    (τU : U →ₗ[F2] F2) (π : U →ₗ[F2] E)
    (F : (E →ₗ[F2] H) → K) (ι : H →ₗ[F2] K)
    (τ : E →ₗ[F2] F2) (fallback : ActualAnswer τ)
    (hτ : τ.comp π = τU)
    (folded : ∀ N h, F (N + τ.smulRight h) = F N + ι h)
    (σ : K →ₗ[F2] F2) (Φ : H →ₗ[F2] E)
    (hn : σ.comp ι ≠ 0)
    (hc : Φ ∈ frequencyCoset (Z.map π).mkQ ((σ.comp ι).smulRight (π z)))
    (hp : 0 < frequencyWeight (tableSign F σ) Φ) :
    ∃ v ∈ candidates Z z τU, π v = (privateOutput ι τ fallback (σ, Φ)).1 := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.ActualAnswer, OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.candidates, OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.privateOutput

theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.conditionalAgreement_ge_mass_div_card line 289
Source documentation
The actual independent policies agree with at least the good Fourier mass divided by the number of left candidates.
```
theorem conditionalAgreement_ge_mass_div_card (Z : Submodule F2 U) (z : U)
    (τU : U →ₗ[F2] F2) (hz : τU z = 1) (π : U →ₗ[F2] E)
    (F : (E →ₗ[F2] H) → K) (ι : H →ₗ[F2] K)
    (τ : E →ₗ[F2] F2) (fallback : ActualAnswer τ)
    (hτ : τ.comp π = τU)
    (folded : ∀ N h, F (N + τ.smulRight h) = F N + ι h) :
    goodCosetMass (Z.map π) (π z) F ι / (candidates Z z τU).card ≤
      conditionalAgreement Z z τU hz π F ι τ fallback := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.ActualAnswer, OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.goodCosetMass, OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.candidates, OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.conditionalAgreement

theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.goodCosetMass_lower_from_slice line 327

Source documentation

The actual transferred affine-slice agreement supplies the sampled good Fourier mass, including removal of characters trivial on the hidden kernel.

theorem goodCosetMass_lower_from_slice (Q : Submodule F2 E)
    [Fintype (H →ₗ[F2] Q)] [Fintype ((E ⧸ Q) →ₗ[F2] H)]
    (N₀ : E →ₗ[F2] H) (F : (E →ₗ[F2] H) → K)
    (ι : H →ₗ[F2] K) (hι : Function.Injective ι) (z' : E) (b : K)
    (α : ℝ) (hα : 0 ≤ α) (ℓ r : ℕ)
    (hH : Module.finrank F2 H ≤ ℓ) (hQ : Module.finrank F2 Q ≤ r)
    (hsmall : 1 / (Fintype.card H : ℝ) ≤ α / 8)
    (hagreement : α / 4 ≤ 𝔼 A : (E ⧸ Q) →ₗ[F2] H,
      if F (N₀ + A.comp Q.mkQ) = b + ι ((N₀ + A.comp Q.mkQ) z')
      then (1 : ℝ) else 0) :
    (α / 8) ^ 2 / (2 : ℝ) ^ (ℓ * r) ≤ goodCosetMass Q z' F ι := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.goodCosetMass

theorem OAI.UniqueGamesTheorem.Decoder.PrivateStrategy.conditionalAgreement_from_slice line 397
def OAI.UniqueGamesTheorem.Decoder.SurrogateFibers.shortcodeAcceptance line 464
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.UniqueGamesTheorem.Decoder.SurrogateFibers.product_perturbation line 471
theorem OAI.UniqueGamesTheorem.Decoder.SurrogateFibers.surrogate_acceptance_eq_fiber_average line 477