PrivateFourier.lean`

63 declarations, 0 contain sorry, 0 declared as axioms

Actual private response laws for v2 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.MaxCutGames.Decoder.PrivateFourier.sign line 21
Source documentation
A real-valued binary character, with the uniform Fourier normalization.
```
def sign (a : F2) : ℝ := (binarySign a).re
```
theorem OAI.MaxCutGames.Decoder.PrivateFourier.sign_zero line 23
theorem OAI.MaxCutGames.Decoder.PrivateFourier.sign_one line 24
theorem OAI.MaxCutGames.Decoder.PrivateFourier.sign_sq line 26
theorem OAI.MaxCutGames.Decoder.PrivateFourier.sign_abs line 29
theorem OAI.MaxCutGames.Decoder.PrivateFourier.sign_add line 32
theorem OAI.MaxCutGames.Decoder.PrivateFourier.sign_add_one line 35
theorem OAI.MaxCutGames.Decoder.PrivateFourier.binary_neg_eq_self line 46
theorem OAI.MaxCutGames.Decoder.PrivateFourier.binary_add_eq_zero_iff line 52
theorem OAI.MaxCutGames.Decoder.PrivateFourier.average_sign_dual line 55
theorem OAI.MaxCutGames.Decoder.PrivateFourier.average_sign_primal line 61
theorem OAI.MaxCutGames.Decoder.PrivateFourier.average_sign_equality line 68
Source documentation
Exact character expansion of equality in the actual output space.
```
theorem average_sign_equality [Fintype (K →ₗ[F2] F2)] (x y : K) :
    (𝔼 σ : K →ₗ[F2] F2, sign (σ x) * sign (σ y)) =
      if x = y then 1 else 0 := by
…
```
Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.sign
theorem OAI.MaxCutGames.Decoder.PrivateFourier.trivial_restriction_probability line 77
Source documentation
The ambient uniform character has trivial restriction to H with exactly the reciprocal cardinality of H. No conditioning on the private character is substituted for the real experiment.
```
theorem trivial_restriction_probability [Fintype H] [Fintype (K →ₗ[F2] F2)]
    (ι : H →ₗ[F2] K) (hι : Function.Injective ι) :
    (𝔼 σ : K →ₗ[F2] F2, if σ.comp ι = 0 then (1 : ℝ) else 0) =
      1 / (Fintype.card H : ℝ) := by
…
```
theorem OAI.MaxCutGames.Decoder.PrivateFourier.trivial_restriction_probability_pow line 98
def OAI.MaxCutGames.Decoder.PrivateFourier.tableSign line 121
Source documentation
The private sign function, formed from the table on one visible row fiber.
```
def tableSign (F : (E →ₗ[F2] H) → K) (σ : K →ₗ[F2] F2)
    (N : E →ₗ[F2] H) : ℝ := sign (σ (F N))
```
Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.sign
def OAI.MaxCutGames.Decoder.PrivateFourier.frequencyWeight line 125
Source documentation
The actual probability assigned to a reverse-map frequency.
```
def frequencyWeight (f : (E →ₗ[F2] H) → ℝ) (Φ : H →ₗ[F2] E) : ℝ :=
…
```
theorem OAI.MaxCutGames.Decoder.PrivateFourier.frequencyWeight_nonneg line 129
theorem OAI.MaxCutGames.Decoder.PrivateFourier.tableSign_frequencyWeight_sum line 133
Source documentation
Squared Fourier coefficients of the private sign form a probability law.
```
theorem tableSign_frequencyWeight_sum (F : (E →ₗ[F2] H) → K)
    (σ : K →ₗ[F2] F2) :
    ∑ Φ : H →ₗ[F2] E, frequencyWeight (tableSign F σ) Φ = 1 := by
…
```
Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.frequencyWeight, OAI.MaxCutGames.Decoder.PrivateFourier.tableSign
theorem OAI.MaxCutGames.Decoder.PrivateFourier.tableSign_antifold line 140

theorem OAI.MaxCutGames.Decoder.PrivateFourier.linearCoeff_translate line 150

Source documentation

Translation of the input multiplies a coefficient by its character.

theorem linearCoeff_translate (f : (E →ₗ[F2] H) → ℝ)
    (D : E →ₗ[F2] H) (Φ : H →ₗ[F2] E) :
    linearCoeff (fun N => f (N + D)) Φ =
      linearCoeff f Φ * (linearTraceCharacter Φ D).re := by
…

theorem OAI.MaxCutGames.Decoder.PrivateFourier.positive_frequency_first_bit line 167

Source documentation

Anti-folding forces every positive-mass frequency to return first bit one.

theorem positive_frequency_first_bit (f : (E →ₗ[F2] H) → ℝ)
    (τ : E →ₗ[F2] F2) (h : H) (Φ : H →ₗ[F2] E)
    (folded : ∀ N, f (N + τ.smulRight h) = -f N)
    (positive : 0 < frequencyWeight f Φ) : τ (Φ h) = 1 := by
…

Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.frequencyWeight

def OAI.MaxCutGames.Decoder.PrivateFourier.frequencyCoset line 201
Source documentation
Frequencies in the affine target's annihilator coset. With q = Q.mkQ, this is exactly θ + Hom(H,Q) in the ambient reverse-map space.
```
def frequencyCoset (q : E →ₗ[F2] V) (θ : H →ₗ[F2] E) :
    Finset (H →ₗ[F2] E) := Finset.univ.filter fun Φ => q.comp (Φ + θ) = 0
```
def OAI.MaxCutGames.Decoder.PrivateFourier.sliceCorrelation line 206
Source documentation
Correlation on a genuine affine slice. N₀ is retained: its phase cannot be discarded when the witness has a nonzero affine intercept.
```
def sliceCorrelation (q : E →ₗ[F2] V) (N₀ : E →ₗ[F2] H)
    (f : (E →ₗ[F2] H) → ℝ) (θ : H →ₗ[F2] E) : ℝ :=
…
```
theorem OAI.MaxCutGames.Decoder.PrivateFourier.traceCharacter_re_mul line 212
theorem OAI.MaxCutGames.Decoder.PrivateFourier.sliceCorrelation_eq_coset line 219
Source documentation
The exact Fourier coset expansion of the affine conditional correlation.
```
theorem sliceCorrelation_eq_coset (q : E →ₗ[F2] V) (N₀ : E →ₗ[F2] H)
    (f : (E →ₗ[F2] H) → ℝ) (θ : H →ₗ[F2] E) :
    sliceCorrelation q N₀ f θ =
      ∑ Φ ∈ frequencyCoset q θ,
        linearCoeff f Φ * (linearTraceCharacter (Φ + θ) N₀).re := by
…
```
Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.sliceCorrelation, OAI.MaxCutGames.Decoder.PrivateFourier.frequencyCoset
theorem OAI.MaxCutGames.Decoder.PrivateFourier.sliceCorrelation_sq_le_coset_mass line 246
Source documentation
Cauchy--Schwarz bounds an affine correlation by the actual Fourier mass in its target coset; no spectral mass is assumed.
```
theorem sliceCorrelation_sq_le_coset_mass (q : E →ₗ[F2] V)
    (N₀ : E →ₗ[F2] H) (f : (E →ₗ[F2] H) → ℝ) (θ : H →ₗ[F2] E) :
    sliceCorrelation q N₀ f θ ^ 2 ≤
      (frequencyCoset q θ).card *
        ∑ Φ ∈ frequencyCoset q θ, frequencyWeight f Φ := by
…
```
Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.sliceCorrelation, OAI.MaxCutGames.Decoder.PrivateFourier.frequencyCoset, OAI.MaxCutGames.Decoder.PrivateFourier.frequencyWeight
theorem OAI.MaxCutGames.Decoder.PrivateFourier.target_character line 274
Source documentation
The pure-tensor target character is literally evaluation at z.
```
theorem target_character (σ : H →ₗ[F2] F2) (z : E) (N : E →ₗ[F2] H) :
    (linearTraceCharacter (σ.smulRight z) N).re = sign (σ (N z)) := by
…
```
Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.sign

theorem OAI.MaxCutGames.Decoder.PrivateFourier.affine_equality_character_expansion line 285

Source documentation

Affine target equality expands into the correlations with the intercept phase sign (σ b). In the projected experiment b = M₀ z + u.

theorem affine_equality_character_expansion (q : E →ₗ[F2] V)
    (N₀ : E →ₗ[F2] H) (F : (E →ₗ[F2] H) → K)
    (ι : H →ₗ[F2] K) (z : E) (b : K) :
    (𝔼 A : V →ₗ[F2] H,
      if F (N₀ + A.comp q) = b + ι ((N₀ + A.comp q) z) then (1 : ℝ) else 0) =
      𝔼 σ : K →ₗ[F2] F2, sign (σ b) *
        sliceCorrelation q N₀ (tableSign F σ) ((σ.comp ι).smulRight z) := by
…

Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.sign, OAI.MaxCutGames.Decoder.PrivateFourier.sliceCorrelation, OAI.MaxCutGames.Decoder.PrivateFourier.tableSign

theorem OAI.MaxCutGames.Decoder.PrivateFourier.sliceCorrelation_tableSign_abs_le_one line 314
Source documentation
Every slice correlation has absolute value at most one.
```
theorem sliceCorrelation_tableSign_abs_le_one (q : E →ₗ[F2] V)
    (N₀ : E →ₗ[F2] H) (F : (E →ₗ[F2] H) → K)
    (σ : K →ₗ[F2] F2) (θ : H →ₗ[F2] E) :
    |sliceCorrelation q N₀ (tableSign F σ) θ| ≤ 1 := by
…
```
Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.sliceCorrelation, OAI.MaxCutGames.Decoder.PrivateFourier.tableSign

theorem OAI.MaxCutGames.Decoder.PrivateFourier.agreement_le_average_abs_correlation line 332

Source documentation

Dropping the unit intercept phase can only increase the average absolute correlation; the hypothesis is the actual affine-slice agreement probability.

theorem agreement_le_average_abs_correlation (q : E →ₗ[F2] V)
    (N₀ : E →ₗ[F2] H) (F : (E →ₗ[F2] H) → K)
    (ι : H →ₗ[F2] K) (z : E) (b : K) :
    (𝔼 A : V →ₗ[F2] H,
      if F (N₀ + A.comp q) = b + ι ((N₀ + A.comp q) z) then (1 : ℝ) else 0) ≤
      𝔼 σ : K →ₗ[F2] F2,
        |sliceCorrelation q N₀ (tableSign F σ) ((σ.comp ι).smulRight z)| := by
…

Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.sliceCorrelation, OAI.MaxCutGames.Decoder.PrivateFourier.tableSign

theorem OAI.MaxCutGames.Decoder.PrivateFourier.frequencyCoset_card line 358
Source documentation
The exact number of frequencies in the affine coset. Translation does not alter the annihilator cardinality, including when the target is nonzero.
```
theorem frequencyCoset_card (Q : Submodule F2 E) [Fintype (H →ₗ[F2] Q)]
    (θ : H →ₗ[F2] E) :
    (frequencyCoset Q.mkQ θ).card =
      2 ^ (Module.finrank F2 H * Module.finrank F2 Q) := by
…
```
Mentions: OAI.MaxCutGames.Decoder.PrivateFourier.frequencyCoset
theorem OAI.MaxCutGames.Decoder.PrivateFourier.frequencyCoset_card_le line 372

theorem OAI.MaxCutGames.Decoder.PrivateFourier.remove_bad_characters line 387

Source documentation

Discarding a set of characters costs at most its actual uniform mass.

theorem remove_bad_characters (C : SigmaChar → ℝ) (good : SigmaChar → Prop)
    (a b : ℝ) (hC : ∀ σ, |C σ| ≤ 1)
    (hcorrelation : a ≤ 𝔼 σ, |C σ|)
    (hbad : (𝔼 σ, if good σ then (0 : ℝ) else 1) ≤ b) :
    a - b ≤ 𝔼 σ, if good σ then |C σ| else 0 := by
…

theorem OAI.MaxCutGames.Decoder.PrivateFourier.average_coset_mass_lower line 407

Source documentation

The second Cauchy--Schwarz step in private decoding. The first step is sliceCorrelation_sq_le_coset_mass; the mass is the actual sampled Fourier mass and good selects nontrivial output characters.

theorem average_coset_mass_lower (C mass : SigmaChar → ℝ) (good : SigmaChar → Prop)
    (N c : ℝ) (hN : 0 < N) (hc : 0 ≤ c)
    (hcorrelation : c ≤ 𝔼 σ, if good σ then |C σ| else 0)
    (hpoint : ∀ σ, good σ → C σ ^ 2 ≤ N * mass σ) :
    c ^ 2 / N ≤ 𝔼 σ, if good σ then mass σ else 0 := by
…

theorem OAI.MaxCutGames.Decoder.PrivateFourier.contraction_mem_target_coset line 437

Source documentation

A frequency in the target coset contracts into z + Q.

theorem contraction_mem_target_coset (Q : Submodule F2 E)
    (σ : H →ₗ[F2] F2) (z : E) (Φ : H →ₗ[F2] E) (h : H)
    (hσ : σ h = 1) (hcoset : Q.mkQ.comp (Φ + σ.smulRight z) = 0) :
    Φ h - z ∈ Q := by
…

theorem OAI.MaxCutGames.Decoder.PrivateFourier.uniform_preimage_probability line 461
Source documentation
If the returned projected answer has a preimage in the candidate set, the uniform, independently sampled candidate finds a preimage with this probability.
```
theorem uniform_preimage_probability (s : Finset U) (π : U → O) (b : O)
    (preimage : ∃ u ∈ s, π u = b) :
    1 / (s.card : ℝ) ≤ 𝔼 u ∈ s, if π u = b then (1 : ℝ) else 0 := by
…
```

theorem OAI.MaxCutGames.Decoder.PrivateFourier.independent_agreement_lower line 478

Source documentation

An explicit product sampling law: the left strategy samples uniformly from s, independently of the right strategy's private sample. Only positive-mass good samples need a preimage; no private Fourier information is passed left.

theorem independent_agreement_lower (s : Finset U) (π : U → O)
    (answer : Ω → O) (weight : Ω → ℝ) (good : Ω → Prop)
    (hweight : ∀ ω, 0 ≤ weight ω)
    (preimage : ∀ ω, good ω → 0 < weight ω → ∃ u ∈ s, π u = answer ω) :
    (∑ ω, if good ω then weight ω else 0) / (s.card : ℝ) ≤
      ∑ ω, weight ω * (𝔼 u ∈ s, if π u = answer ω then (1 : ℝ) else 0) := by
…

def OAI.MaxCutGames.Decoder.PrivateStrategy.candidates line 527
theorem OAI.MaxCutGames.Decoder.PrivateStrategy.mem_candidates line 530
theorem OAI.MaxCutGames.Decoder.PrivateStrategy.candidates_nonempty line 533
theorem OAI.MaxCutGames.Decoder.PrivateStrategy.candidates_card_le line 537
theorem OAI.MaxCutGames.Decoder.PrivateStrategy.candidates_card_le_pow line 549

theorem OAI.MaxCutGames.Decoder.PrivateStrategy.candidate_preimage line 563

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.MaxCutGames.Decoder.PrivateStrategy.candidates

theorem OAI.MaxCutGames.Decoder.PrivateStrategy.exists_unit line 587
def OAI.MaxCutGames.Decoder.PrivateStrategy.chooseUnit line 597
theorem OAI.MaxCutGames.Decoder.PrivateStrategy.chooseUnit_spec line 601
abbrev OAI.MaxCutGames.Decoder.PrivateStrategy.ActualAnswer line 604
def OAI.MaxCutGames.Decoder.PrivateStrategy.privateSeedLaw line 607
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.MaxCutGames.Decoder.PrivateStrategy.privateSeedLaw_expectation line 617
def OAI.MaxCutGames.Decoder.PrivateStrategy.privateOutput line 628
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.MaxCutGames.Decoder.PrivateStrategy.ActualAnswer
theorem OAI.MaxCutGames.Decoder.PrivateStrategy.privateOutput_eq_contraction line 636
def OAI.MaxCutGames.Decoder.PrivateStrategy.privateLaw line 651
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.MaxCutGames.Decoder.PrivateStrategy.ActualAnswer
theorem OAI.MaxCutGames.Decoder.PrivateStrategy.privateLaw_expectation line 656
def OAI.MaxCutGames.Decoder.PrivateStrategy.candidateLaw line 671
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.MaxCutGames.Decoder.PrivateStrategy.ActualAnswer
theorem OAI.MaxCutGames.Decoder.PrivateStrategy.candidateLaw_expectation line 678

def OAI.MaxCutGames.Decoder.PrivateStrategy.conditionalAgreement line 703

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.MaxCutGames.Decoder.PrivateStrategy.ActualAnswer

theorem OAI.MaxCutGames.Decoder.PrivateStrategy.conditionalAgreement_eq_sum line 710
def OAI.MaxCutGames.Decoder.PrivateStrategy.goodCosetMass line 740
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.MaxCutGames.Decoder.PrivateStrategy.goodCosetMass_nonneg line 748

theorem OAI.MaxCutGames.Decoder.PrivateStrategy.good_frequency_preimage line 761

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.MaxCutGames.Decoder.PrivateStrategy.ActualAnswer, OAI.MaxCutGames.Decoder.PrivateStrategy.candidates, OAI.MaxCutGames.Decoder.PrivateStrategy.privateOutput

theorem OAI.MaxCutGames.Decoder.PrivateStrategy.conditionalAgreement_ge_mass_div_card line 782

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.MaxCutGames.Decoder.PrivateStrategy.ActualAnswer, OAI.MaxCutGames.Decoder.PrivateStrategy.goodCosetMass, OAI.MaxCutGames.Decoder.PrivateStrategy.candidates, OAI.MaxCutGames.Decoder.PrivateStrategy.conditionalAgreement

theorem OAI.MaxCutGames.Decoder.PrivateStrategy.goodCosetMass_lower_from_slice line 820

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.MaxCutGames.Decoder.PrivateStrategy.goodCosetMass

theorem OAI.MaxCutGames.Decoder.PrivateStrategy.conditionalAgreement_from_slice line 888