TableReduction.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniqueGamesTheorem.Integration.TableReduction.tableEnumeration line 14
def OAI.UniqueGamesTheorem.Integration.TableReduction.tableSkeleton line 22
Source documentation
The projection is used only to fill an erased witness field. It is never used when generating constraints or evaluating their permutation tables.
```
def tableSkeleton (T : Table s d) : SplitGadget s d :=
…
```
def OAI.UniqueGamesTheorem.Integration.TableReduction.output line 26
Source documentation
A total executable map with finite vector data and no nonlinear-map input.
```
def output (S : Source) (k : Nat) (T : Table s d) : Instance (2 ^ s) :=
…
```
theorem OAI.UniqueGamesTheorem.Integration.TableReduction.output_eq_with_witness line 32
Source documentation
Every correcting-map witness generates exactly the same numbered instance, including the ordered constraint list and all permutation entries.
```
theorem output_eq_with_witness (S : Source) (k : Nat) (T : Table s d)
    (f : Ambient s d → Alphabet s) (hf : ∀ x c, f (x + (c, 0)) = f x + c) :
    output S k T =
      outputInstanceWithEnumeration S k (T.gadget f hf) (tableEnumeration T f hf) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Integration.TableReduction.output, OAI.UniqueGamesTheorem.Integration.TableReduction.tableEnumeration
theorem OAI.UniqueGamesTheorem.Integration.TableReduction.completeAt_output_iff line 38
theorem OAI.UniqueGamesTheorem.Integration.TableReduction.soundAt_output_iff line 46
theorem OAI.UniqueGamesTheorem.Integration.TableReduction.edge_ofEnumeration line 54
theorem OAI.UniqueGamesTheorem.Integration.TableReduction.acceptance_ofEnumeration line 62
theorem OAI.UniqueGamesTheorem.Integration.TableReduction.rate_ofEnumeration line 74
theorem OAI.UniqueGamesTheorem.Integration.TableReduction.completeAt_ofEnumeration_iff line 85
Source documentation
Normalization to a concrete table preserves the original completeness threshold exactly; there is no additional approximation loss.
```
theorem completeAt_ofEnumeration_iff (error : RationalError)
    (S : Source) (k : Nat) (g : SplitGadget s d) (en : NoiseEnumeration g) :
    CompleteAt error (output S k (Table.ofEnumeration g en)) ↔
      CompleteAt error (outputInstance S k g) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Integration.TableReduction.output
theorem OAI.UniqueGamesTheorem.Integration.TableReduction.soundAt_ofEnumeration_iff line 97