OAI/Computability/UniqueGames/Reduction/OutputTranslationsLemmas.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Executable direct addresses for the actual canonical game. Every original edge occurrence and its translation table is retained, in the same order. Addresses not representing realized bodies are isolated vertices. No vertex list, duplicate removal, or inverse enumeration is evaluated by the output.

  1. theorem OAI.UniqueGamesTheorem.Reduction.OutputTranslations.translationTable_vector line 18

    Source documentation

    A forward table translates every binary vector by the same offset sum.

    theorem translationTable_vector {s : Nat} (a b x : Vector s) :
    (Encoding.translationTable a b).images[Encoding.alphabetEquiv s x] =
      Encoding.alphabetEquiv s (x + (a + b)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.Encoding.translationTable, OAI.UniqueGamesTheorem.Reduction.Encoding.alphabetEquiv

  2. theorem OAI.UniqueGamesTheorem.Reduction.OutputTranslations.translationTable_coordinates line 24

    Source documentation

    The same law on every numbered alphabet label, in fixed vector coordinates.

    theorem translationTable_coordinates {s : Nat} (a b : Vector s) (label : Fin (2^s)) :
    (Encoding.alphabetEquiv s).symm ((Encoding.translationTable a b).images[label]) =
      (Encoding.alphabetEquiv s).symm label + (a + b) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.Encoding.alphabetEquiv, OAI.UniqueGamesTheorem.Reduction.Encoding.translationTable

  3. theorem OAI.UniqueGamesTheorem.Reduction.OutputTranslations.explicitEdge_vector line 33

    Source documentation

    Every actual explicit edge has a concrete translation vector.

    theorem explicitEdge_vector (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (ω : ActualGame.Outcome S k g) :
    ∃ shift : Vector s, ∀ x : Vector s,
      (ActualGame.explicitEdge S k g ω).permutation.images[Encoding.alphabetEquiv s x] =
        Encoding.alphabetEquiv s (x + shift) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualGame.Outcome, OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitEdge, OAI.UniqueGamesTheorem.Reduction.Encoding.alphabetEquiv

  4. theorem OAI.UniqueGamesTheorem.Reduction.OutputTranslations.explicitEdge_coordinates line 43
  5. theorem OAI.UniqueGamesTheorem.Reduction.OutputTranslations.outputInstanceWithEnumeration_vector line 56

    Source documentation

    All emitted occurrences, including parallel edges and repeated noise values, use translations in the same alphabet coordinates.

    theorem outputInstanceWithEnumeration_vector (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g) :
    ∀ constraint ∈ (ActualGame.outputInstanceWithEnumeration S k g en).constraints,
      ∃ shift : Vector s, ∀ x : Vector s,
        constraint.permutation.images[Encoding.alphabetEquiv s x] =
          Encoding.alphabetEquiv s (x + shift) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualGame.outputInstanceWithEnumeration, OAI.UniqueGamesTheorem.Reduction.Encoding.alphabetEquiv

  6. theorem OAI.UniqueGamesTheorem.Reduction.OutputTranslations.outputInstanceWithEnumeration_coordinates line 66
  7. theorem OAI.UniqueGamesTheorem.Reduction.OutputTranslations.tableOutput_vector line 77

    Source documentation

    Erasing the correcting-map witness leaves the translation promise intact.

    theorem tableOutput_vector (S : Source) (k : Nat) {s d : Nat}
    (T : Integration.NoiseTables.Table s d) :
    ∀ constraint ∈ (Integration.TableReduction.output S k T).constraints,
      ∃ shift : Vector s, ∀ x : Vector s,
        constraint.permutation.images[Encoding.alphabetEquiv s x] =
          Encoding.alphabetEquiv s (x + shift) :=
…

    Mentions: OAI.UniqueGamesTheorem.Integration.NoiseTables.Table, OAI.UniqueGamesTheorem.Integration.TableReduction.output, OAI.UniqueGamesTheorem.Reduction.Encoding.alphabetEquiv

  8. theorem OAI.UniqueGamesTheorem.Reduction.OutputTranslations.tableOutput_coordinates line 86
  9. theorem OAI.UniqueGamesTheorem.Reduction.OutputTranslations.uniformOutput_vector line 95
  10. theorem OAI.UniqueGamesTheorem.Reduction.OutputTranslations.uniformOutput_coordinates line 104
  11. abbrev OAI.UniqueGamesTheorem.Reduction.AddressGame.bodyCapacity line 130
  12. def OAI.UniqueGamesTheorem.Reduction.AddressGame.vertexCount line 133
  13. def OAI.UniqueGamesTheorem.Reduction.AddressGame.vertexAddress line 136

    Source documentation

    Both bipartite sides remain distinct address blocks.

    def vertexAddress (S : Source) (k s d : Nat) (v : ActualGame.TwoSidedVertex S k s d) :
    Fin (vertexCount S k s d) :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualGame.TwoSidedVertex, OAI.UniqueGamesTheorem.Reduction.AddressGame.vertexCount

  14. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.vertexAddress_injective line 140
  15. def OAI.UniqueGamesTheorem.Reduction.AddressGame.queryAddress line 152

    Source documentation

    This is the endpoint routine used at runtime: canonicalize, serialize, apply Horner radix arithmetic, and add the side block.

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

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualGame.Query, OAI.UniqueGamesTheorem.Reduction.AddressGame.vertexCount

  16. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.vertexAddress_query line 157
  17. def OAI.UniqueGamesTheorem.Reduction.AddressGame.explicitToAddress line 163

    Source documentation

    Proof adapter only: the output constructor does not call this inverse.

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

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitVertexCount, OAI.UniqueGamesTheorem.Reduction.AddressGame.vertexCount

  18. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.explicitToAddress_injective line 167
  19. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.explicitToAddress_apply line 171
  20. def OAI.UniqueGamesTheorem.Reduction.AddressGame.semanticToAddress line 178

    Source documentation

    The corresponding injection from the original semantic vertex space.

    noncomputable def semanticToAddress (S : Source) (k s d : Nat) :
    Fin (ActualGame.vertexCount S k s d) → Fin (vertexCount S k s d) :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualGame.vertexCount, OAI.UniqueGamesTheorem.Reduction.AddressGame.vertexCount

  21. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.semanticToAddress_injective line 182
  22. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.semanticToAddress_apply line 186
  23. def OAI.UniqueGamesTheorem.Reduction.AddressGame.addressEdge line 192
  24. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.addressEdge_eq_embed line 200
  25. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.addressEdge_eq_semantic_embed line 207
  26. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.addressEdge_permutation line 214
  27. def OAI.UniqueGamesTheorem.Reduction.AddressGame.outputInstance line 220

    Source documentation

    Only canonical words, bounded radix arithmetic, and the explicit outcome list occur in the runtime path. The correcting function is not inspected.

    def outputInstance (S : Source) (k : Nat) {s d : Nat} (g : SplitGadget s d)
    (en : NoiseEnumeration g) : Instance (2^s) where
…
  28. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.outputInstance_eq_embed line 232

    Source documentation

    An exact instance equality, retaining the explicit edge-list order.

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

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressGame.outputInstance, OAI.UniqueGamesTheorem.Reduction.ActualGame.outputInstanceWithEnumeration, OAI.UniqueGamesTheorem.Reduction.AddressGame.explicitToAddress, OAI.UniqueGamesTheorem.Reduction.AddressGame.explicitToAddress_injective

  29. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.outputInstance_length line 241
  30. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.outputInstance_count line 248
  31. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.completeAt_outputInstance_iff_explicit line 259
  32. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.soundAt_outputInstance_iff_explicit line 266
  33. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.completeAt_outputInstance_iff line 273
  34. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.soundAt_outputInstance_iff line 279
  35. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.outputInstance_translations line 285
  36. def OAI.UniqueGamesTheorem.Reduction.AddressGame.tableOutput line 296

    Source documentation

    The concrete vector-table interface contains no correcting-map witness.

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

    Mentions: OAI.UniqueGamesTheorem.Integration.NoiseTables.Table

  37. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.completeAt_tableOutput_iff line 301
  38. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.soundAt_tableOutput_iff line 306
  39. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.tableOutput_translations line 311
  40. theorem OAI.UniqueGamesTheorem.Reduction.AddressGame.vertexCount_eq_polynomial line 317

    Source documentation

    Exact polynomial bound for the complete two-sided address space.

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

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressGame.vertexCount, OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.capacityPolynomial

  41. def OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.queryWords line 333
  42. def OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.queryRank line 339
  43. def OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.permutationWords line 343
  44. def OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.edgeWords line 351
  45. def OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.edgeBits line 356
  46. theorem OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.queryWords_length line 360
  47. theorem OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.permutationWords_length line 366
  48. theorem OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.queryWords_actual line 370
  49. theorem OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.queryAddress_false line 377
  50. theorem OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.queryAddress_true line 386
  51. theorem OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.addressEdge_words line 397

    Source documentation

    Exact full serialized edge, including every forward permutation image.

    theorem addressEdge_words (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (omega : ActualGame.Outcome S k g) :
    constraintWords (AddressGame.addressEdge S k g omega) =
      edgeWords (CanonicalAddress.base S.variables S.occurrences s d)
        (AddressGame.bodyCapacity S k s d)
        (CanonicalBodyTemplate.sourceFields omega.1.1 (ActualGame.names S))
        omega.1.2 (ActualGame.rightQuery S k g omega).2
        (fun j => ActualGame.rhs S (omega.1.1 j)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualGame.Outcome, OAI.UniqueGamesTheorem.Reduction.AddressGame.addressEdge, OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.edgeWords, OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.base, OAI.UniqueGamesTheorem.Reduction.AddressGame.bodyCapacity, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.sourceFields, OAI.UniqueGamesTheorem.Reduction.ActualGame.names, OAI.UniqueGamesTheorem.Reduction.ActualGame.rightQuery, OAI.UniqueGamesTheorem.Reduction.ActualGame.rhs

  52. theorem OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.addressEdge_bits line 411
  53. theorem OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.edgeBits_split line 423

    Source documentation

    The actual edge emitter's three payloads concatenate to the codec exactly.

    theorem edgeBits_split {k s d : Nat} (base capacity : Nat)
    (fields : Fin k → Fin 4 → Nat) (X Y : ActualGame.Map k s d) (b : Fin k → F2) :
    edgeBits base capacity fields X Y b =
      encodeWords [queryRank base fields X b, capacity + queryRank base fields Y b] ++
        encodeWords (permutationWords X Y b) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualGame.Map, OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.edgeBits, OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.queryRank, OAI.UniqueGamesTheorem.Reduction.AddressByteSemantics.permutationWords