RawMapLaw.lean`

64 declarations, 0 contain sorry, 0 declared as axioms

Exact uniform sampling of linear maps on the common private coordinate target.

def OAI.MaxCutGames.Soundness.RawMapLaw.rawMap line 19
theorem OAI.MaxCutGames.Soundness.RawMapLaw.coefficients_rawMap line 23
theorem OAI.MaxCutGames.Soundness.RawMapLaw.rawMap_coefficients line 34
def OAI.MaxCutGames.Soundness.RawMapLaw.rawMapEquiv line 43
instance OAI.MaxCutGames.Soundness.RawMapLaw.rawMapsFintype line 49
def OAI.MaxCutGames.Soundness.RawMapLaw.bitsRawMapEquiv line 53
theorem OAI.MaxCutGames.Soundness.RawMapLaw.bits_coefficients line 57
theorem OAI.MaxCutGames.Soundness.RawMapLaw.uniform_bits_rawMaps line 63
Source documentation
This equality counts every raw coefficient and every genuine row map once.
```
theorem uniform_bits_rawMaps {Q : Type} [Fintype Q] [DecidableEq Q]
    (H : (RawPoint J →ₗ[F2] (Q → F2)) → ℝ) :
    (𝔼 gamma : RawCoefficients J (ZeroInformation.Bits Q), H (bitsRawMapEquiv J gamma)) =
      𝔼 Y, H Y :=
…
```
Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Bits, OAI.MaxCutGames.Soundness.RawMapLaw.bitsRawMapEquiv
def OAI.MaxCutGames.Reduction.Explicit.pairs line 77
Source documentation
A Cartesian product that preserves repetitions in each input list.
```
def pairs (xs : List α) (ys : List β) : List (α × β) :=
…
```
theorem OAI.MaxCutGames.Reduction.Explicit.length_pairs line 80
theorem OAI.MaxCutGames.Reduction.Explicit.mem_pairs line 89
def OAI.MaxCutGames.Reduction.Explicit.words line 94
Source documentation
Enumerate all words of length k over an explicitly listed alphabet.
```
def words (alphabet : List α) : Nat → List (List α)
  | 0 => [[]]
  | k + 1 => (pairs alphabet (words alphabet k)).map fun p => p.1 :: p.2
```
Mentions: OAI.MaxCutGames.Reduction.Explicit.pairs
theorem OAI.MaxCutGames.Reduction.Explicit.length_words line 98
theorem OAI.MaxCutGames.Reduction.Explicit.mem_words line 107
Source documentation
The enumerator covers exactly the prescribed words.
```
theorem mem_words {alphabet : List α} {w : List α} {k : Nat} :
    w ∈ words alphabet k ↔ w.length = k ∧ ∀ a ∈ w, a ∈ alphabet := by
…
```
Mentions: OAI.MaxCutGames.Reduction.Explicit.words
abbrev OAI.MaxCutGames.Reduction.Explicit.CoordinateOutcome line 137
Source documentation
(question occurrences, binary map matrix, noise index, binary functional). The matrix is flattened and has (2*k+1)*dimR bits.
```
abbrev CoordinateOutcome := (List Nat × List Nat) × (Nat × List Nat)
```
def OAI.MaxCutGames.Reduction.Explicit.edgeOutcomes line 139
def OAI.MaxCutGames.Reduction.Explicit.edgeCount line 145
Source documentation
The formula in Equation (4.21).
```
def edgeCount (m k dimR noiseCount : Nat) : Nat :=
…
```
theorem OAI.MaxCutGames.Reduction.Explicit.length_edgeOutcomes line 148
theorem OAI.MaxCutGames.Reduction.Explicit.edgeCount_pos line 156
theorem OAI.MaxCutGames.Reduction.Explicit.edgeOutcomes_nonempty line 160
theorem OAI.MaxCutGames.Reduction.Explicit.edgeCount_mono line 167
theorem OAI.MaxCutGames.Reduction.Explicit.product_pow line 172
theorem OAI.MaxCutGames.Reduction.Explicit.edgeCount_polynomial_bound line 180
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.nodup_pairs line 211

def OAI.MaxCutGames.Reduction.ActualEnumeration.functions line 215

Source documentation

Exhaustive finite-function enumeration with a specified value list.

def functions (values : List α) : (n : Nat) → List (Fin n → α)
  | 0 => [Fin.elim0]
  | n + 1 => (pairs values (functions values n)).map
      (fun p => Fin.cons p.1 p.2)

theorem OAI.MaxCutGames.Reduction.ActualEnumeration.length_functions line 220
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.mem_functions line 226
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.nodup_functions line 236
abbrev OAI.MaxCutGames.Reduction.ActualEnumeration.Coefficients line 252
def OAI.MaxCutGames.Reduction.ActualEnumeration.fromCoefficients line 254
def OAI.MaxCutGames.Reduction.ActualEnumeration.toCoefficients line 264
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.to_fromCoefficients line 267
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.from_toCoefficients line 276
def OAI.MaxCutGames.Reduction.ActualEnumeration.coefficientEquiv line 283
Source documentation
Actual matrix-coefficient equivalence, rather than just a count model.
```
def coefficientEquiv : Coefficients k R ≃ (E k →ₗ[F2] R) where
…
```
Mentions: OAI.MaxCutGames.Reduction.ActualEnumeration.Coefficients
def OAI.MaxCutGames.Reduction.ActualEnumeration.allLinearMaps line 289
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.length_allLinearMaps line 292
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.mem_allLinearMaps line 299
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.nodup_allLinearMaps line 306
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.cardinal_linearMaps line 311
def OAI.MaxCutGames.Reduction.ActualEnumeration.vectors line 323
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.length_vectors line 326
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.mem_vectors line 329
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.nodup_vectors line 333
abbrev OAI.MaxCutGames.Reduction.ActualEnumeration.Ambient line 336
def OAI.MaxCutGames.Reduction.ActualEnumeration.ambientVectors line 339
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.length_ambientVectors line 341
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.mem_ambientVectors line 344
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.nodup_ambientVectors line 347
abbrev OAI.MaxCutGames.Reduction.ActualEnumeration.Query line 350
def OAI.MaxCutGames.Reduction.ActualEnumeration.queries line 352
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.mem_queries line 355
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.nodup_queries line 359
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.length_queries line 363
abbrev OAI.MaxCutGames.Reduction.ActualEnumeration.Outcome line 368
def OAI.MaxCutGames.Reduction.ActualEnumeration.outcomes line 372
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.length_outcomes line 377
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.mem_outcomes line 387
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.nodup_outcomes line 396
def OAI.MaxCutGames.Reduction.ActualEnumeration.indexedOutcomes line 406
Source documentation
The executable edge experiment for an arbitrary explicitly ordered noise index type. Equal noise vectors still have separate indices and entries.
```
def indexedOutcomes (m k s d : Nat) (indices : List N) :
    List (Query m k s d × (N × (E k →ₗ[F2] F2))) :=
…
```
Mentions: OAI.MaxCutGames.Reduction.ActualEnumeration.Query
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.length_indexedOutcomes line 410
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.mem_indexedOutcomes line 415
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.nodup_indexedOutcomes line 422
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.indexedOutcomes_nonempty line 427
theorem OAI.MaxCutGames.Reduction.ActualEnumeration.length_indexedOutcomes_polynomial_bound line 436
Source documentation
A genuine polynomial size bound for the actual linear-map edge list. This is deliberately separate from a certified machine running-time bound.
```
theorem length_indexedOutcomes_polynomial_bound {m n coefficient degree : Nat}
    (h : m ≤ coefficient * (n+1)^degree) (k s d : Nat) (indices : List N) :
    (indexedOutcomes m k s d indices).length ≤
      (coefficient^k * 2^((2*k+1)*(s+d+1)) * indices.length) *
        (n+1)^(degree*k) := by
…
```
Mentions: OAI.MaxCutGames.Reduction.ActualEnumeration.indexedOutcomes