FourierResponse.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The Fourier decoder is an actual finite law of private answers. Empty Fourier supports use an explicit fallback answer, making every response law normalized even before folding has been imposed.

def OAI.MaxCutGames.Foundations.Hastad.supportResponse line 22
theorem OAI.MaxCutGames.Foundations.Hastad.supportResponse_expectation line 35
def OAI.MaxCutGames.Foundations.Hastad.fourierResponse line 48
Source documentation
Squared Fourier coefficients select a mask; a uniform support coordinate selects the actual answer. Both stages use only this player's private table.
```
def fourierResponse (fallback : I) (F : Cube I → Bool) : FiniteDistribution I where
…
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.Cube
theorem OAI.MaxCutGames.Foundations.Hastad.fourierResponse_expectation line 58
theorem OAI.MaxCutGames.Foundations.Hastad.response_expectation_nonnegative line 73
def OAI.MaxCutGames.Foundations.Hastad.responseAgreement line 78
def OAI.MaxCutGames.Foundations.Hastad.validResponseAgreement line 83
theorem OAI.MaxCutGames.Foundations.Hastad.supportResponse_validAgreement line 90
theorem OAI.MaxCutGames.Foundations.Hastad.validAgreement_le_supportResponses line 104
theorem OAI.MaxCutGames.Foundations.Hastad.validDecoderSuccess_le_response line 130
theorem OAI.MaxCutGames.Foundations.Hastad.conditioned_folded_response_bound line 149
Source documentation
Local soundness now bounds the success of two genuine normalized answer laws. No assumption about randomized decoding or its normalization remains.
```
theorem conditioned_folded_response_bound (ε : ℝ) (π : J → I) (valid : J → Bool)
    (i₀ : I) (tableA : HalfCube i₀ → Bool)
    (j₀ : {j : J // valid j = true}) (tableB : HalfCube j₀ → Bool)
    (hε : 0 < ε) (hε' : ε ≤ 1 / 2) :
    4 * ε * testBias ε π (fun f => bitSign (foldedAnswer i₀ tableA f))
      (fun g => bitSign (conditionedFoldedAnswer valid j₀ tableB g)) ^ 2 ≤
      validResponseAgreement valid π i₀ j₀.val (foldedAnswer i₀ tableA)
        (conditionedFoldedAnswer valid j₀ tableB) :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Hastad.HalfCube, OAI.MaxCutGames.Foundations.Hastad.testBias, OAI.MaxCutGames.Foundations.Hastad.bitSign, OAI.MaxCutGames.Foundations.Hastad.foldedAnswer, OAI.MaxCutGames.Foundations.Hastad.conditionedFoldedAnswer, OAI.MaxCutGames.Foundations.Hastad.validResponseAgreement