OAI/Computability/UniqueGames/Machines/MachineSingleOrbitBridgeLemmas.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The old addressed producer is reused only as a code generator. Its exact output is the doubled codec of the new single-orbit game. The proved physical postprocessor then yields the new game, with no premise about the value of the legacy game and no legacy gadget or inverse theorem used.

  1. abbrev OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.SingleAddress.vertexCount line 24
  2. abbrev OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.SingleAddress.queryAddress line 25
  3. abbrev OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.SingleAddress.addressEdge line 26
  4. abbrev OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.SingleAddress.outputInstance line 27
  5. abbrev OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.SingleAddress.tableOutput line 28
  6. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.old_addressEdge_eq_double line 32
  7. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.old_outputInstance_eq_double line 42

    Source documentation

    Exact equality of the ordered, fully serialized constraint data.

    theorem old_outputInstance_eq_double (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g) :
    AddressGame.outputInstance S k g en = doubleInstance (SingleAddress.outputInstance S k g en) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.SingleAddress.outputInstance

  8. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.old_tableOutput_eq_double line 51
  9. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.output line 56
  10. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.old_output_eq_double line 60
  11. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.doubledComputableInPolyTime line 68

    Source documentation

    Reinterpret the existing producer using the proved exact codec equality.

    def doubledComputableInPolyTime (k : Nat) {s d : Nat}
    (T : UniqueGamesTheorem.Integration.NoiseTables.Table s d) :
    TM2ComputableInPolyTime SourceEncoding.inputBits
      (fun I => gameBits (doubleInstance I)) (output k T) := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.NoiseTables.Table, OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.output

  12. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.computableInPolyTime line 83
  13. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitBridge.workAlphabetFinite line 99