OAI/Computability/MaxCut/Games/FinalCNFStream.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

Exact row enumeration and input/output stream identities for the concrete final-CNF machine. Rows occur in stored order, including repeated rows.

  1. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents line 16

    Source documentation

    The actual unprocessed suffix of the finite table's stored row indices.

    def remainingEvents (table : GraphTables.Table) (r : Nat) : List (Fin table.darts) :=
…
  2. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents line 19
  3. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream line 22
  4. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream line 25
  5. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_zero line 30
  6. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_length line 34
  7. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_done line 38
  8. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_cons line 42
  9. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_zero line 49
  10. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_done line 52
  11. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_succ line 56
  12. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.processed_append_remaining line 63
  13. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_nil line 67
  14. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_cons line 69
  15. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_append line 74
  16. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_nil line 79
  17. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_cons line 82
  18. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_append line 88
  19. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_cons line 94
  20. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_remaining_cons line 101
  21. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_processed_succ line 109
  22. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_split line 118
  23. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_split line 124
  24. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap_rows_inline_FinalCNFStream line 130
  25. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowList_eq_finRange_map line 136
  26. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_all line 143

    Source documentation

    The stream starts at exactly the row suffix left by the checked header phase.

    theorem inputStream_all (table : GraphTables.Table) :
    inputStream table (List.finRange table.darts) = tableRowsBits (genericTable table) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits

  27. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_zero line 154
  28. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_accumulator_succ line 159

    Source documentation

    Pushing a row's reversed emission realizes extension of the forward prefix.

    theorem outputStream_accumulator_succ (plan : Plan) (table : GraphTables.Table)
    (r : Nat) (h : r < table.darts) (header : List Bool) :
    (plan.flatMap (Emitter.commandBits (rowOperands table ⟨r, h⟩)
      (rowRelation table ⟨r, h⟩))).reverse ++
        (header ++ outputStream plan table (processedEvents table r)).reverse =
      (header ++ outputStream plan table (processedEvents table (r + 1))).reverse := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowRelation, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents

  29. structure OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.LoopInvariant line 176
  30. structure OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.LoopRun line 187
  31. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowInvariant_succ line 199
  32. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowWords_nonempty line 219
  33. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.loopInTime line 225

    Source documentation

    Induction follows the actual unary row counter and the actual unconsumed input suffix. Every iteration invokes the checked row program.

    noncomputable def loopInTime (headerPlan plan : Plan) (table : GraphTables.Table)
    (remaining : Nat) :
    ∀ (r : Nat) (_hcount : r + remaining = table.darts) (base : Tape → List Bool)
      (ambient : Ambient), LoopInvariant table r base →
        LoopRun headerPlan plan table r remaining base ambient := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.LoopInvariant, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.LoopRun

  34. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes line 292
  35. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rawBudget line 296
  36. structure OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.RawRun line 301
  37. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.header_loopInvariant line 309
  38. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rawRun line 326

    Source documentation

    The input is read from the genuine initList configuration. Header, every row, final guard, and reversal are all actual transitions of this one program.

    noncomputable def rawRun (plan : Plan) (table : GraphTables.Table) : RawRun plan table := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.RawRun

  39. inductive OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.Reference line 383
  40. structure OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.LiteralTemplate line 388
  41. abbrev OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.ClauseTemplate line 393
  42. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.queryLiteral line 395
  43. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.auxiliaryLiteral line 398
  44. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.tautologyTemplate line 401
  45. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.chainTemplates line 405

    Source documentation

    The same prefix-chain clauses used by splitLong, in their output order.

    def chainTemplates (bits : Fin 12 → Bool) : Vector ClauseTemplate 10 :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.ClauseTemplate

  46. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.blockTemplates line 418
  47. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.templates line 421
  48. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.literalAt line 425

    Source documentation

    Fixed clause/slot indexing for the machine's finite emission plan.

    def literalAt (accepted : Bool) (bits : Fin 12 → Bool)
    (clause : Fin 10) (slot : Fin 3) : LiteralTemplate :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.LiteralTemplate

  49. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.templates_length line 429
  50. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.templates_true line 432
  51. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.templates_false line 435
  52. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.literalTemplates line 438
  53. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.literalTemplates_length line 441
  54. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.literalWords line 446
  55. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.clauseWords line 449
  56. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.words line 452
  57. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.words_length line 455
  58. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.resolve line 464
  59. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.resolve_query_value line 468
  60. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.resolve_auxiliary_value line 472
  61. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.instantiateLiteral line 480
  62. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause line 483
  63. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.splitLong_twelve line 488

    Source documentation

    A symbolic twelve-input chain expands to exactly these ten clauses.

    theorem splitLong_twelve {n : Nat} (ls : Fin 12 → Literal n) (ys : Fin 9 → Fin n) :
    VerifierToCNF.splitLong (List.ofFn ls) (List.ofFn ys) =
      [#v[ls 0, ls 1, ⟨ys 0, true⟩],
       #v[⟨ys 0, false⟩, ls 2, ⟨ys 1, true⟩],
       #v[⟨ys 1, false⟩, ls 3, ⟨ys 2, true⟩],
       #v[⟨ys 2, false⟩, ls 4, ⟨ys 3, true⟩],
       #v[⟨ys 3, false⟩, ls 5, ⟨ys 4, true⟩],
       #v[⟨ys 4, false⟩, ls 6, ⟨ys 5, true⟩],
       #v[⟨ys 5, false⟩, ls 7, ⟨ys 6, true⟩],
       #v[⟨ys 6, false⟩, ls 8, ⟨ys 7, true⟩],
       #v[⟨ys 7, false⟩, ls 9, ⟨ys 8, true⟩],
       #v[⟨ys 8, false⟩, ls 10, ls 11]] := by
…
  64. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.instantiate_templates line 504

    Source documentation

    Instantiating the fixed plan reproduces the actual converter's entire block.

    theorem instantiate_templates :
    (templates (V.accepts e (VerifierToCNF.patternAt 12 p))
      (VerifierToCNF.patternAt 12 p)).map (instantiateClause V e p) =
        VerifierToCNF.block V (by decide) e p := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.templates, OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause

  65. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.instantiate_templates_of_acceptance line 518
  66. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause_words line 525
  67. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.words_eq_block line 530

    Source documentation

    The finite plan's sixty natural fields are the converter's actual row words.

    theorem words_eq_block :
    words (V.accepts e (VerifierToCNF.patternAt 12 p)) (VerifierToCNF.patternAt 12 p)
      (fun r => (resolve V e p r).val) =
        (VerifierToCNF.block V (by decide) e p).flatMap Complexity.clauseWords := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.words, OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.resolve, OAI.MaxCutGames.Foundations.Complexity.clauseWords

  68. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTemplate.block_words_length line 538
  69. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.referenceValue line 555
  70. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.auxiliaryFlag line 559
  71. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.tailFlag line 563
  72. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headFlag line 567
  73. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.pattern_lt line 571
  74. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.referenceOffset line 575
  75. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan line 580

    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.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan

  76. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_length line 589
  77. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_bits line 592
  78. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.patternLiteral line 620
  79. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan line 625
  80. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan line 629
  81. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_length line 632
  82. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_length line 643
  83. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap line 650
  84. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_bits line 656
  85. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.referenceValue_eq_resolve line 687
  86. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_bits line 713