OAI/Computability/UniqueGames/Decoding/TableKeysAddressGameLemmas.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Direct addresses for the v2 single-orbit matrix game. There is one canonical body address space, with no side bit and no extra right-endpoint offset. Unused addresses are isolated. Runtime construction uses canonical words and radix arithmetic, not deduplication or inverse vertex enumeration.

  1. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.vertexCount line 23
  2. def OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.vertexAddress line 26
  3. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.vertexAddress_injective line 29
  4. def OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.queryAddress line 36

    Source documentation

    Both endpoints use this same routine and this same address block.

    def queryAddress (S : Source) (k s d : Nat) (q : TableKeysGame.Query S k s d) :
    Fin (vertexCount S k s d) :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.Query, OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.vertexCount

  5. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.vertexAddress_query line 40
  6. def OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.explicitToAddress line 46

    Source documentation

    This inverse is a proof adapter only; the output constructor never calls it.

    def explicitToAddress (S : Source) (k s d : Nat) :
    Fin (TableKeysGame.explicitVertexCount S k s d) → Fin (vertexCount S k s d) :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.explicitVertexCount, OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.vertexCount

  7. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.explicitToAddress_injective line 50
  8. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.explicitToAddress_apply line 55
  9. def OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.semanticToAddress line 61
  10. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.semanticToAddress_injective line 65
  11. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.semanticToAddress_apply line 70
  12. def OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.addressEdge line 76
  13. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.addressEdge_eq_embed line 84
  14. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.addressEdge_eq_semantic_embed line 91
  15. def OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.outputInstance line 99

    Source documentation

    The correcting function is not evaluated when producing an edge list.

    def outputInstance (S : Source) (k : Nat) {s d : Nat} (g : SplitGadget s d)
    (en : NoiseEnumeration g) : Instance (2^s) where
…
  16. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.outputInstance_eq_embed line 111

    Source documentation

    Every occurrence, its order, and its full permutation table are retained.

    theorem outputInstance_eq_embed (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g) :
    outputInstance S k g en =
      embedInstance (TableKeysGame.outputInstanceWithEnumeration S k g en)
        (explicitToAddress S k s d) (explicitToAddress_injective S k s d) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.outputInstance, OAI.UniqueGamesTheorem.Decoder.TableKeysGame.outputInstanceWithEnumeration, OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.explicitToAddress, OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.explicitToAddress_injective

  17. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.outputInstance_length line 120
  18. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.outputInstance_count line 127
  19. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.completeAt_outputInstance_iff_explicit line 138
  20. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.soundAt_outputInstance_iff_explicit line 145
  21. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.completeAt_outputInstance_iff line 152
  22. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.soundAt_outputInstance_iff line 159
  23. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.outputInstance_translations line 166
  24. def OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.tableOutput line 184

    Source documentation

    Fixed finite noise data suffice for executable output.

    def tableOutput (S : Source) (k : Nat) {s d : Nat} (T : Integration.NoiseTables.Table s d) :
    Instance (2^s) :=
…

    Mentions: OAI.UniqueGamesTheorem.Integration.NoiseTables.Table

  25. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.tableOutput_eq_with_witness line 190

    Source documentation

    The nonlinear correctness witness is erased from the output program.

    theorem tableOutput_eq_with_witness (S : Source) (k : Nat) {s d : Nat}
    (T : Integration.NoiseTables.Table s d) (f : Ambient s d → Alphabet s)
    (hf : ∀ x c, f (x + (c, 0)) = f x + c) :
    tableOutput S k T = outputInstance S k (T.gadget f hf)
      (Integration.TableReduction.tableEnumeration T f hf) := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.NoiseTables.Table, OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.tableOutput, OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.outputInstance, OAI.UniqueGamesTheorem.Integration.TableReduction.tableEnumeration

  26. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.completeAt_tableOutput_iff line 197
  27. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.soundAt_tableOutput_iff line 205
  28. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.tableOutput_translations line 213
  29. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.vertexCount_eq_polynomial line 219

    Source documentation

    Exact polynomial capacity, without the legacy two-side factor.

    theorem vertexCount_eq_polynomial (S : Source) (k s d : Nat) :
    vertexCount S k s d = (CanonicalAddress.capacityPolynomial k s d).eval
      (S.variables + S.occurrences) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.vertexCount

  30. theorem OAI.UniqueGamesTheorem.Decoder.MatrixGap.address_rate_eq_semantic_acceptance line 243
  31. theorem OAI.UniqueGamesTheorem.Decoder.MatrixGap.address_value_le_of_semantic_acceptance line 271

    Source documentation

    Soundness is measured on the generated direct-address instance. Unused addresses and reindexing introduce no additional labeling advantage.

    theorem address_value_le_of_semantic_acceptance (S : Source) (k : Nat) {s d : Nat}
    (T : NoiseTables.Table s d) (f : Ambient s d → Alphabet s)
    (hf : ∀ x c, f (x + (c, 0)) = f x + c)
    (h : ∀ labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s),
      TableKeysGame.acceptanceProbability S k (T.gadget f hf) labeling ≤ (99 : ℚ) / 100) :
    InstanceValue.value (TableKeysAddressGame.tableOutput S k T) ≤ (99 : ℝ) / 100 := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.TableKeysGame.acceptanceProbability, OAI.UniqueGamesTheorem.Decoder.TableKeysAddressGame.tableOutput