NoiseEnumerationLemmas.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

An explicit enumeration of noise indices, retaining repeated vector values. This additional data leaves SplitGadget unchanged and supplies an executable ordering for the edge list.

structure OAI.UniqueGamesTheorem.Reduction.ActualSource.NoiseEnumeration line 17
def OAI.UniqueGamesTheorem.Reduction.ActualSource.NoiseEnumeration.ofFintype line 26
theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.NoiseEnumeration.nonempty line 31
theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.NoiseEnumeration.perm_univ line 37
theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.NoiseEnumeration.length_eq_card line 43
theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.NoiseEnumeration.sum_eq_univ line 47
theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.NoiseEnumeration.average_eq_expect line 52
Source documentation
A list average over index occurrences is precisely the uniform finite law.
```
theorem average_eq_expect (e : NoiseEnumeration g) (f : g.NoiseIndex → ℚ) :
    (e.indices.map f).sum / e.indices.length = Finset.univ.expect f := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.ActualSource.NoiseEnumeration
def OAI.UniqueGamesTheorem.Integration.NoiseTables.reindex line 73
Source documentation
Reindexing changes the names of outcomes, retaining their uniform law.
```
def reindex (g : SplitGadget s d) {I : Type} [Fintype I] [Nonempty I]
    (e : I ≃ g.NoiseIndex) : SplitGadget s d where
…
```
theorem OAI.UniqueGamesTheorem.Integration.NoiseTables.reindex_stabilityError line 82
theorem OAI.UniqueGamesTheorem.Integration.NoiseTables.reindex_kernelProbability line 89
structure OAI.UniqueGamesTheorem.Integration.NoiseTables.Table line 102
Source documentation
Only a nonempty finite list of binary vectors is required as static noise data. The correcting function is a separate witness used in the proof.
```
structure Table (s d : Nat) where
…
```
def OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.gadget line 108
def OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.ofEnumeration line 117
theorem OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.ofEnumeration_length line 121
def OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.positionEquiv line 127
Source documentation
The inverse equivalence is used only to prove the probability identity; the forward noise lookup is ordinary finite-list indexing.
```
noncomputable def positionEquiv (g : SplitGadget s d) (en : NoiseEnumeration g) :
    Fin (ofEnumeration g en).vectors.length ≃ g.NoiseIndex := by
…
```
Mentions: OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.ofEnumeration
theorem OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.noise_positionEquiv line 133
theorem OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.stabilityError_ofEnumeration line 140
theorem OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.kernelProbability_ofEnumeration line 150

theorem OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.guarantees_ofEnumeration line 161

Source documentation

Exact table conversion retains both mathematical gadget guarantees.

theorem guarantees_ofEnumeration (g : SplitGadget s d) (en : NoiseEnumeration g)
    {ζ ν : ℚ} {r : Nat}
    (hstable : g.stabilityError ≤ ζ)
    (hdisp : ∀ (P : Type) [AddCommGroup P] [Module F2 P]
      (S : Ambient s d →ₗ[F2] P),
      r ≤ Module.finrank F2 (S.comp (alphabetEmbedding s d)).range →
      SplitGadget.kernelProbability g S ≤ ν) :
    ((ofEnumeration g en).gadget g.f g.equivariant).stabilityError ≤ ζ ∧
      ∀ (P : Type) [AddCommGroup P] [Module F2 P]
        (S : Ambient s d →ₗ[F2] P),
        r ≤ Module.finrank F2 (S.comp (alphabetEmbedding s d)).range →
        SplitGadget.kernelProbability
…

Mentions: OAI.UniqueGamesTheorem.Integration.SplitGadget.kernelProbability, OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.ofEnumeration, OAI.UniqueGamesTheorem.Integration.NoiseTables.Table.gadget