OAI/Computability/UniqueGames/Machines/FinalCNFRowPlanLemmas.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

The fixed finite emission plan for one directed graph row. All choices based on the relation are functions of its 4096-bit finite register. Vertex counts, endpoint names and row indices are read by preserving unary scans.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.referenceValue line 23
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.auxiliaryFlag line 27
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.tailFlag line 31
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headFlag line 35
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.pattern_lt line 39
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.referenceOffset line 43
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.literalPlan line 48

    Source documentation

    Seven real commands for the two unary fields of a literal.

    def literalPlan (p : VerifierToCNF.PatternIndex 12) (literal : Ambient → LiteralTemplate) : Plan :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan

  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_length line 57
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_bits line 60
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.patternLiteral line 88
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.patternPlan line 93
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowPlan line 97
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_length line 100
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_length line 111
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap line 119
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_bits line 125
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.referenceValue_eq_resolve line 156
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_bits line 182
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.endpointTapes line 211
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.endpointsInTime line 218

    Source documentation

    Read the two fields actually stored in a graph row: tail and reverse dart.

    def endpointsInTime (headerPlan plan : Plan) (base : Tape → List Bool)
    (tail reverse : Nat) (rest : List Bool)
    (hinput : base .input = encodeWord tail ++ encodeWord reverse ++ rest)
    (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan plan))
      ⟨some .startTail, ((ambient, ()), none), base⟩
      (some ⟨some .headTableFirst, ((ambient, ()), none),
        endpointTapes base tail reverse rest⟩) (tail + reverse + 4) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.endpointTapes

  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.relationInTime line 244

    Source documentation

    The fixed unary relation reader occupies one finite TM2 statement.

    def relationInTime (headerPlan plan : Plan) (base : Tape → List Bool)
    (relation : GraphTables.RelationTable) (rest : List Bool)
    (hinput : base .input = encodeWords (GraphTables.relationWords relation) ++ rest)
    (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan plan))
      ⟨some .readRelation, ((ambient, ()), none), base⟩
      (some ⟨some (.row (Emitter.labelAt plan.length 36864 0 .entry)),
        ((((), fun i => relation[i]), ()), none), Function.update base .input rest⟩) 1 where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.program

  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.emitInTime line 259

    Source documentation

    Execute the complete fixed row emission plan against physical unary tapes.

    def emitInTime (headerPlan plan : Plan) (base : Tape → List Bool)
    (operands : Fin 5 → Nat) (hoperands : ∀ i, base (source i) = encodeWord (operands i))
    (hscratch : base .scratch = []) (ambient : Ambient)
    (N : Nat) (hbounded : ∀ i, operands i ≤ N) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan plan))
      ⟨some (.row (Emitter.labelAt plan.length 36864 0 .entry)),
        ((ambient, ()), none), base⟩
      (some ⟨some .clearTail, ((ambient, ()), none),
        Function.update base .accumulator
          ((plan.flatMap (Emitter.commandBits operands ambient)).reverse ++ base .accumulator)⟩)
      (plan.length * (3 * (N + 1) + 3) + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.source, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.program

  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.finishTapes line 276
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.finishInTime line 283

    Source documentation

    Clear precisely the three isolated temporary fields and increment the physical row counter before returning to the input guard.

    def finishInTime (headerPlan plan : Plan) (base : Tape → List Bool)
    (tail head reverse row : Nat)
    (htail : base .tail = encodeWord tail) (hhead : base .head = encodeWord head)
    (hreverse : base .reverseIndex = encodeWord reverse)
    (hrow : base .rowIndex = encodeWord row) (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan plan))
      ⟨some .clearTail, ((ambient, ()), none), base⟩
      (some ⟨some .guard, ((ambient, ()), none), finishTapes base row⟩)
      (tail + head + reverse + 4) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.guard, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.finishTapes

  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headRoles_zero line 320
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headRoles_one line 321
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headRoles_two line 322
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headRoles_three line 323
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headRoles_four line 324
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headRoles_five line 325
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowOperands line 327
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowRelation line 331
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowRest line 334
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.preparedTapes line 337
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.prepared_input line 343
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.prepared_head line 349
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.prepared_tail line 357
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.prepared_reverse line 363
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.prepared_frame line 370
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.emittedTapes line 378
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowResultTapes line 384
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowResult_input line 388
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowResult_tail line 393
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowResult_head line 398
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowResult_reverse line 403
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowResult_index line 408
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowResult_accumulator line 413
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowResult_frame line 420
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.guardRowInTime line 431
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.guardEndInTime line 444
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.prepared_operands line 457

    Source documentation

    All five unbounded operands remain isolated encoded naturals after the row parser and head lookup, including both independently retrieved endpoints.

    theorem prepared_operands (base : Tape → List Bool) (table : GraphTables.Table)
    (e : Fin table.darts) (rest : List Bool)
    (hn : base .vertices = encodeWord table.vertices)
    (hm : base .darts = encodeWord table.darts)
    (hr : base .rowIndex = encodeWord e.val)
    (ht : base .tail = []) :
    ∀ i, (Function.update (preparedTapes base table e rest) Tape.input rest) (source i) =
      encodeWord (rowOperands table e i) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.preparedTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.source, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowOperands

  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowOperands_bounded line 486
  53. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowTime line 497
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowInTime line 503

    Source documentation

    Run one complete stored row, including the actual table-based head lookup. The only hypotheses describe the physical input tapes; no execution or serialization correctness of a caller-provided body is assumed.

    noncomputable def rowInTime (headerPlan plan : Plan) (base : Tape → List Bool)
    (table : GraphTables.Table) (e : Fin table.darts) (rest : List Bool)
    (hinput : base .input = encodeWords (GraphTables.rowWords table.rows[e]) ++ rest)
    (harchive : base .archive = GraphTables.tableBits table)
    (hn : base .vertices = encodeWord table.vertices)
    (hm : base .darts = encodeWord table.darts)
    (hrow : base .rowIndex = encodeWord e.val)
    (ht : base .tail = []) (hh : base .head = []) (hr : base .reverseIndex = [])
    (hscratch : base .scratch = []) (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan plan))
      ⟨some .startTail, ((ambient, ()), none), base⟩
      (some ⟨some .guard, ((rowRelation table e, ()), none),
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.guard, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowRelation