CayleyTailCount.lean`

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Actual finite binary-word tail counts for the proposed Cayley base graph.

No expander, independence, spectral, or random-generator existence result is assumed here.

def OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.upperMasks line 30
def OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.lowerMasks line 33
def OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.badMasks line 36
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.upperMasks_weight line 41
Source documentation
Weight every actual upper-tail mask by at least 3 ^ (3 * m).
```
theorem upperMasks_weight (s : Finset α) (m : ℕ) (hcard : s.card = 4 * m) :
    (upperMasks s m).card * 3 ^ (3 * m) ≤ 4 ^ (4 * m) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.upperMasks
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.lowerMasks_complement_image line 59
Source documentation
Complementation preserves multiplicity and exchanges the two closed tails.
```
theorem lowerMasks_complement_image (s : Finset α) (m : ℕ)
    (hcard : s.card = 4 * m) :
    (lowerMasks s m).image (fun t => s \ t) = upperMasks s m := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.lowerMasks, OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.upperMasks
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.lowerMasks_card_eq_upperMasks line 82
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.ratio_le_of_weight line 96
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.upperMasks_ratio_le line 110
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.lowerMasks_ratio_le line 115
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.badMasks_ratio_le_sharp line 120
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.badMasks_ratio_le line 135
def OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.trueMask line 145
def OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.countTrue line 148
def OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.badWord line 150
instance OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.(instance at line 153) line 153
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.bitSign_mean_eq line 157
Source documentation
The sign convention is the existing Walsh convention: false is +1, true is -1.
```
theorem bitSign_mean_eq [Nonempty D] (word : D → Bool) :
    (𝔼 i, bitSign (word i)) =
      1 - 2 * ((countTrue word : ℝ) / Fintype.card D) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.countTrue
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.not_badWord_bias line 174
Source documentation
Excluding both closed integer tails bounds the actual mean Walsh sign.
```
theorem not_badWord_bias (m : ℕ) (hcard : Fintype.card D = 4 * m) (hm : 0 < m)
    (word : D → Bool) (hword : ¬ badWord m word) :
    |𝔼 i, bitSign (word i)| ≤ (1 / 2 : ℝ) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.badWord
def OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.wordMaskEquiv line 195
Source documentation
All words occur once, so subset counting keeps the actual uniform law.
```
def wordMaskEquiv [DecidableEq D] : (D → Bool) ≃ Finset D where
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.twoTail_probability line 206
Source documentation
Actual real uniform expectation on binary words, including both closed tails.
```
theorem twoTail_probability [DecidableEq D] (m : ℕ) (hcard : Fintype.card D = 4 * m) :
    (𝔼 word : D → Bool, if badWord m word then (1 : ℝ) else 0) ≤
      2 * (2 / 3 : ℝ) ^ m := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.badWord
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.union_bound_le_half line 228
Source documentation
Numerical budget for a union bound over at most 2 ^ n frequencies.
```
theorem union_bound_le_half (n m : ℕ) (hm : 3 * (n + 2) ≤ m) :
    (2 : ℝ) ^ n * (2 * (2 / 3 : ℝ) ^ m) ≤ 1 / 2 := by
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.fixed_parameters line 246
Source documentation
The proposed fixed parameters meet the elementary counting margin.
```
theorem fixed_parameters : 3 * (448 + 2) ≤ 16384 ∧ 4 * 16384 = 2 ^ 16 := by
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.fixed_union_bound line 249
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.seventh_power_size line 254
Source documentation
Pure parameter identity; this does not assert existence of a graph.
```
theorem seventh_power_size : (2 : ℕ) ^ 448 = (((2 : ℕ) ^ 16) ^ 7) ^ 4 := by
…
```
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleyTailCount.seventh_power_abs_le line 258
Source documentation
Pure scalar estimate, ready for a separately proved spectral powering theorem.
```
theorem seventh_power_abs_le {a : ℝ} (ha : |a| ≤ 1 / 2) : |a ^ 7| ≤ 1 / 128 := by
…
```