Decoder.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

The parity projection and finite Fourier decoder used in Håstad's three-query argument. Probabilities are explicit finite sums.

def OAI.MaxCutGames.Foundations.Hastad.parityProjection line 18
theorem OAI.MaxCutGames.Foundations.Hastad.walsh_support line 21
theorem OAI.MaxCutGames.Foundations.Hastad.sign_power_parity line 29
theorem OAI.MaxCutGames.Foundations.Hastad.walsh_pullback line 39
theorem OAI.MaxCutGames.Foundations.Hastad.projectedCoefficient_eq line 49
theorem OAI.MaxCutGames.Foundations.Hastad.projection_has_preimage line 54
theorem OAI.MaxCutGames.Foundations.Hastad.scaled_geometric_power_le_one line 67
Source documentation
A purely algebraic decay estimate used instead of exponential bounds.
```
theorem scaled_geometric_power_le_one {t : ℝ} (ht : 0 ≤ t) (ht' : t ≤ 1) (n : Nat) :
    (n : ℝ) * (1 - t) * t ^ n ≤ 1 := by
…
```
theorem OAI.MaxCutGames.Foundations.Hastad.noise_decay_bound line 81
def OAI.MaxCutGames.Foundations.Hastad.zeroMask line 94
theorem OAI.MaxCutGames.Foundations.Hastad.support_eq_empty_iff line 97
theorem OAI.MaxCutGames.Foundations.Hastad.parityProjection_zero line 109
def OAI.MaxCutGames.Foundations.Hastad.agreementProbability line 116
Source documentation
Choose uniform coordinates in the two masks and check the projection. An empty support contributes zero.
```
def agreementProbability (π : J → I) (a : Cube I) (b : Cube J) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube
theorem OAI.MaxCutGames.Foundations.Hastad.agreementProbability_nonneg line 121
theorem OAI.MaxCutGames.Foundations.Hastad.agreementProbability_projection line 129
def OAI.MaxCutGames.Foundations.Hastad.decoderSuccess line 157
Source documentation
Select independent Walsh masks by squared coefficients and uniform points in each support. The two selections use only the respective private tables.
```
def decoderSuccess (π : J → I) (A : Cube I → Bool) (B : Cube J → Bool) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube
def OAI.MaxCutGames.Foundations.Hastad.decodingEnergy line 161
theorem OAI.MaxCutGames.Foundations.Hastad.decodingEnergy_le_success line 164
theorem OAI.MaxCutGames.Foundations.Hastad.bias_sq_le_weighted_energy line 198
theorem OAI.MaxCutGames.Foundations.Hastad.decoder_four_epsilon_bias_sq line 215
theorem OAI.MaxCutGames.Foundations.Hastad.folded_decoder_bound line 242
Source documentation
A concrete folded half-table discharges the zero-coefficient condition.
```
theorem folded_decoder_bound (ε : ℝ) (π : J → I)
    (i₀ : I) (table : HalfCube i₀ → Bool) (B : Cube J → Bool)
    (hε : 0 < ε) (hε' : ε ≤ 1 / 2) :
    4 * ε * testBias ε π (fun f => bitSign (foldedAnswer i₀ table f))
      (fun g => bitSign (B g)) ^ 2 ≤ decoderSuccess π (foldedAnswer i₀ table) B := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.HalfCube, OAI.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.testBias, OAI.MaxCutGames.Foundations.Hastad.bitSign, OAI.MaxCutGames.Foundations.Hastad.foldedAnswer, OAI.MaxCutGames.Foundations.Hastad.decoderSuccess
def OAI.MaxCutGames.Foundations.Hastad.validAgreementProbability line 250
theorem OAI.MaxCutGames.Foundations.Hastad.validAgreementProbability_eq line 257
def OAI.MaxCutGames.Foundations.Hastad.validDecoderSuccess line 270
theorem OAI.MaxCutGames.Foundations.Hastad.conditioned_validDecoderSuccess line 278
Source documentation
Clause validity in the decoded game follows from the concrete conditioned table; no Fourier-support hypothesis is passed to this theorem.
```
theorem conditioned_validDecoderSuccess (valid : J → Bool) (π : J → I)
    (A : Cube I → Bool) (j₀ : {j : J // valid j = true})
    (table : HalfCube j₀ → Bool) :
    validDecoderSuccess valid π A (conditionedFoldedAnswer valid j₀ table) =
      decoderSuccess π A (conditionedFoldedAnswer valid j₀ table) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.HalfCube, OAI.MaxCutGames.Foundations.Hastad.validDecoderSuccess, OAI.MaxCutGames.Foundations.Hastad.conditionedFoldedAnswer, OAI.MaxCutGames.Foundations.Hastad.decoderSuccess
theorem OAI.MaxCutGames.Foundations.Hastad.conditioned_folded_decoder_bound line 296