OAI/Computability/MaxCut/Machines/MachineBinaryRenameLoop.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

The actual cursor loop for sparse-name renaming. A finite three-position slot counts completed clauses. Each nonempty cursor test calls the checked literal machine, then pushes one variable-count bit. Every third literal also pushes one clause-count bit. No instruction counts an unbounded list in finite control.

All nine literal-machine tapes retain their meanings. Tapes 9 and 10 are the variable and clause counters. The original token stream is preserved; the cursor is exhausted, the six work tapes are restored, and the output contains the reversed concatenation of exactly the emitted literal words.

  1. abbrev OAI.MaxCutGames.BinaryRenameLoop.Token line 24
  2. def OAI.MaxCutGames.BinaryRenameLoop.nextSlot line 26
  3. def OAI.MaxCutGames.BinaryRenameLoop.clauseIncrement line 28
  4. def OAI.MaxCutGames.BinaryRenameLoop.finalSlot line 30
  5. def OAI.MaxCutGames.BinaryRenameLoop.completedClauses line 34
  6. theorem OAI.MaxCutGames.BinaryRenameLoop.finalSlot_three line 38
  7. theorem OAI.MaxCutGames.BinaryRenameLoop.completedClauses_three line 41
  8. theorem OAI.MaxCutGames.BinaryRenameLoop.finalSlot_triples line 45
  9. theorem OAI.MaxCutGames.BinaryRenameLoop.completedClauses_triples line 50
  10. def OAI.MaxCutGames.BinaryRenameLoop.outputBody line 55
  11. theorem OAI.MaxCutGames.BinaryRenameLoop.outputBody_nil line 58
  12. theorem OAI.MaxCutGames.BinaryRenameLoop.outputBody_cons line 60
  13. def OAI.MaxCutGames.BinaryRenameLoop.steps line 64
  14. theorem OAI.MaxCutGames.BinaryRenameLoop.payload_length_le_stream line 68
  15. def OAI.MaxCutGames.BinaryRenameLoop.perLiteralBound line 83
  16. theorem OAI.MaxCutGames.BinaryRenameLoop.literal_steps_le line 86
  17. theorem OAI.MaxCutGames.BinaryRenameLoop.steps_le line 98
  18. theorem OAI.MaxCutGames.BinaryRenameLoop.steps_le_cubic line 111
  19. abbrev OAI.MaxCutGames.BinaryRenameLoop.Alphabet line 129
  20. abbrev OAI.MaxCutGames.BinaryRenameLoop.State line 130
  21. abbrev OAI.MaxCutGames.BinaryRenameLoop.clean line 131
  22. inductive OAI.MaxCutGames.BinaryRenameLoop.Label line 134
  23. def OAI.MaxCutGames.BinaryRenameLoop.literalTapes line 140
  24. theorem OAI.MaxCutGames.BinaryRenameLoop.literalTapes_injective line 143
  25. def OAI.MaxCutGames.BinaryRenameLoop.finish line 149
  26. def OAI.MaxCutGames.BinaryRenameLoop.next line 155
  27. def OAI.MaxCutGames.BinaryRenameLoop.instruction line 159
  28. def OAI.MaxCutGames.BinaryRenameLoop.loopTapes line 176

    Source documentation

    These are the only four stacks changed by the complete loop.

    def loopTapes (tape : Fin 11 → K) (base : K → List Bool)
    (cursor output variableCounter clauses : List Bool) : K → List Bool :=
…
  29. theorem OAI.MaxCutGames.BinaryRenameLoop.loopTapes_cursor line 181
  30. theorem OAI.MaxCutGames.BinaryRenameLoop.loopTapes_output line 187
  31. theorem OAI.MaxCutGames.BinaryRenameLoop.loopTapes_variables line 193
  32. theorem OAI.MaxCutGames.BinaryRenameLoop.loopTapes_clauses line 199
  33. theorem OAI.MaxCutGames.BinaryRenameLoop.update_cursor_inline_MachineBinaryRenameLoop line 204
  34. theorem OAI.MaxCutGames.BinaryRenameLoop.update_output_inline_MachineBinaryRenameLoop line 214
  35. theorem OAI.MaxCutGames.BinaryRenameLoop.update_variables_inline_MachineBinaryRenameLoop line 224
  36. theorem OAI.MaxCutGames.BinaryRenameLoop.update_clauses_inline_MachineBinaryRenameLoop line 234
  37. theorem OAI.MaxCutGames.BinaryRenameLoop.loopTapes_other line 240
  38. theorem OAI.MaxCutGames.BinaryRenameLoop.stepAux_finish line 246
  39. theorem OAI.MaxCutGames.BinaryRenameLoop.joinTrace_inline_MachineBinaryRenameLoop line 251
  40. theorem OAI.MaxCutGames.BinaryRenameLoop.peekStep line 263
  41. theorem OAI.MaxCutGames.BinaryRenameLoop.emptyStep line 275
  42. theorem OAI.MaxCutGames.BinaryRenameLoop.tallyStep line 286
  43. theorem OAI.MaxCutGames.BinaryRenameLoop.bodyTrace line 302

    Source documentation

    Peek, execute the checked literal program, then update the two counters.

    theorem bodyTrace (tokens : List Token) (token : Token) (slot : Fin 3)
    (suffix output variableCounter clauses : List Bool)
    (canonical : BinaryNameMachine.canonical token.2 = true)
    (tokensCanonical : ∀ t ∈ tokens, BinaryNameMachine.canonical t.2 = true)
    (present : token.2 ∈ BinaryNameSearch.payloads tokens)
    (permanent : base (tape 1) = BinaryNameSearch.stream tokens)
    (empty : ∀ i : Fin 11, 2 ≤ i.val → i.val ≤ 7 → base (tape i) = []) :
    (advance (TM2.step program))^[BinaryLiteralMachine.steps tokens token.2 + 2]
      (some ⟨some (labels .entry), clean ambient slot,
        loopTapes tape base (BinaryNameSearch.tokenBits token ++ suffix) output variableCounter clauses⟩) =
      some ⟨some (labels .entry), clean ambient (nextSlot slot),
        loopTapes tape base suffix
…

    Mentions: OAI.MaxCutGames.BinaryRenameLoop.Token, OAI.MaxCutGames.BinaryNameMachine.canonical, OAI.MaxCutGames.BinaryNameSearch.payloads, OAI.MaxCutGames.BinaryNameSearch.stream, OAI.MaxCutGames.BinaryLiteralMachine.steps, OAI.MaxCutGames.BinaryRenameLoop.clean, OAI.MaxCutGames.BinaryRenameLoop.loopTapes, OAI.MaxCutGames.BinaryNameSearch.tokenBits, OAI.MaxCutGames.BinaryRenameLoop.nextSlot

  44. theorem OAI.MaxCutGames.BinaryRenameLoop.loopTrace line 375

    Source documentation

    Full loop execution, including the final empty-cursor test.

    theorem loopTrace (tokens input : List Token) (slot : Fin 3)
    (output variableCounter clauses : List Bool)
    (tokensCanonical : ∀ t ∈ tokens, BinaryNameMachine.canonical t.2 = true)
    (included : ∀ t ∈ input, t ∈ tokens)
    (permanent : base (tape 1) = BinaryNameSearch.stream tokens)
    (empty : ∀ i : Fin 11, 2 ≤ i.val → i.val ≤ 7 → base (tape i) = []) :
    (advance (TM2.step program))^[steps tokens input]
      (some ⟨some (labels .entry), clean ambient slot,
        loopTapes tape base (BinaryNameSearch.stream input) output variableCounter clauses⟩) =
      some ⟨done, clean ambient (finalSlot input.length slot),
        loopTapes tape base [] ((outputBody tokens input).reverse ++ output)
          (List.replicate input.length true ++ variableCounter)
…

    Mentions: OAI.MaxCutGames.BinaryRenameLoop.Token, OAI.MaxCutGames.BinaryNameMachine.canonical, OAI.MaxCutGames.BinaryNameSearch.stream, OAI.MaxCutGames.BinaryRenameLoop.steps, OAI.MaxCutGames.BinaryRenameLoop.clean, OAI.MaxCutGames.BinaryRenameLoop.loopTapes, OAI.MaxCutGames.BinaryRenameLoop.finalSlot, OAI.MaxCutGames.BinaryRenameLoop.outputBody

  45. theorem OAI.MaxCutGames.BinaryRenameLoop.triplesTrace line 420

    Source documentation

    On complete triples the finite slot is reset and the two counters are exact.

    theorem triplesTrace (tokens input : List Token) (count : Nat)
    (length_eq : input.length = 3 * count) (output variableCounter clauses : List Bool)
    (tokensCanonical : ∀ t ∈ tokens, BinaryNameMachine.canonical t.2 = true)
    (included : ∀ t ∈ input, t ∈ tokens)
    (permanent : base (tape 1) = BinaryNameSearch.stream tokens)
    (empty : ∀ i : Fin 11, 2 ≤ i.val → i.val ≤ 7 → base (tape i) = []) :
    (advance (TM2.step program))^[steps tokens input]
      (some ⟨some (labels .entry), clean ambient 0,
        loopTapes tape base (BinaryNameSearch.stream input) output variableCounter clauses⟩) =
      some ⟨done, clean ambient 0,
        loopTapes tape base [] ((outputBody tokens input).reverse ++ output)
          (List.replicate (3 * count) true ++ variableCounter)
…

    Mentions: OAI.MaxCutGames.BinaryRenameLoop.Token, OAI.MaxCutGames.BinaryNameMachine.canonical, OAI.MaxCutGames.BinaryNameSearch.stream, OAI.MaxCutGames.BinaryRenameLoop.steps, OAI.MaxCutGames.BinaryRenameLoop.clean, OAI.MaxCutGames.BinaryRenameLoop.loopTapes, OAI.MaxCutGames.BinaryRenameLoop.outputBody

  46. def OAI.MaxCutGames.BinaryRenameLoop.triplesInTime line 438

    Source documentation

    The machine's bit-length bound includes every peek, literal run, and tally.

    def triplesInTime (tokens input : List Token) (count : Nat)
    (length_eq : input.length = 3 * count) (output variableCounter clauses : List Bool)
    (tokensCanonical : ∀ t ∈ tokens, BinaryNameMachine.canonical t.2 = true)
    (included : ∀ t ∈ input, t ∈ tokens)
    (permanent : base (tape 1) = BinaryNameSearch.stream tokens)
    (empty : ∀ i : Fin 11, 2 ≤ i.val → i.val ≤ 7 → base (tape i) = []) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .entry), clean ambient 0,
        loopTapes tape base (BinaryNameSearch.stream input) output variableCounter clauses⟩
      (some ⟨done, clean ambient 0,
        loopTapes tape base [] ((outputBody tokens input).reverse ++ output)
          (List.replicate (3 * count) true ++ variableCounter)
…

    Mentions: OAI.MaxCutGames.BinaryRenameLoop.Token, OAI.MaxCutGames.BinaryNameMachine.canonical, OAI.MaxCutGames.BinaryNameSearch.stream, OAI.MaxCutGames.BinaryRenameLoop.clean, OAI.MaxCutGames.BinaryRenameLoop.loopTapes, OAI.MaxCutGames.BinaryRenameLoop.outputBody

  47. abbrev OAI.MaxCutGames.BinaryTokenMachine.Tape line 480
  48. abbrev OAI.MaxCutGames.BinaryTokenMachine.Alphabet line 481
  49. abbrev OAI.MaxCutGames.BinaryTokenMachine.State line 482
  50. inductive OAI.MaxCutGames.BinaryTokenMachine.Label line 484
  51. def OAI.MaxCutGames.BinaryTokenMachine.afterName line 493
  52. theorem OAI.MaxCutGames.BinaryTokenMachine.afterName_zero line 496
  53. theorem OAI.MaxCutGames.BinaryTokenMachine.afterName_one line 497
  54. theorem OAI.MaxCutGames.BinaryTokenMachine.afterName_two line 498
  55. def OAI.MaxCutGames.BinaryTokenMachine.jump line 500
  56. def OAI.MaxCutGames.BinaryTokenMachine.clauseInstruction line 504

    Source documentation

    Discard a clause marker, or finish at the final formula terminator.

    def clauseInstruction : TM2.Stmt Alphabet Label State :=
…

    Mentions: OAI.MaxCutGames.BinaryTokenMachine.Alphabet, OAI.MaxCutGames.BinaryTokenMachine.Label, OAI.MaxCutGames.BinaryTokenMachine.State

  57. def OAI.MaxCutGames.BinaryTokenMachine.signInstruction line 511
  58. def OAI.MaxCutGames.BinaryTokenMachine.nameInstruction line 518

    Source documentation

    Copy both symbols of a payload pair, or copy the name terminator.

    def nameInstruction (slot : Fin 3) : TM2.Stmt Alphabet Label State :=
…

    Mentions: OAI.MaxCutGames.BinaryTokenMachine.Alphabet, OAI.MaxCutGames.BinaryTokenMachine.Label, OAI.MaxCutGames.BinaryTokenMachine.State

  59. def OAI.MaxCutGames.BinaryTokenMachine.program line 530
  60. abbrev OAI.MaxCutGames.BinaryTokenMachine.machine line 538
  61. def OAI.MaxCutGames.BinaryTokenMachine.tapes line 549
  62. def OAI.MaxCutGames.BinaryTokenMachine.cfg line 552
  63. theorem OAI.MaxCutGames.BinaryTokenMachine.tapes_zero line 556
  64. theorem OAI.MaxCutGames.BinaryTokenMachine.tapes_one line 559
  65. theorem OAI.MaxCutGames.BinaryTokenMachine.tapes_two line 562
  66. theorem OAI.MaxCutGames.BinaryTokenMachine.update_zero_inline_MachineBinaryTokenMachine line 565
  67. theorem OAI.MaxCutGames.BinaryTokenMachine.update_one_inline_MachineBinaryTokenMachine line 571
  68. theorem OAI.MaxCutGames.BinaryTokenMachine.clauseStep line 577
  69. theorem OAI.MaxCutGames.BinaryTokenMachine.finalStep line 584
  70. theorem OAI.MaxCutGames.BinaryTokenMachine.signStep line 591
  71. theorem OAI.MaxCutGames.BinaryTokenMachine.nameEndStep line 599
  72. theorem OAI.MaxCutGames.BinaryTokenMachine.nameDigitStep line 607
  73. theorem OAI.MaxCutGames.BinaryTokenMachine.nameTrace line 616
  74. theorem OAI.MaxCutGames.BinaryTokenMachine.literalTrace line 633
  75. theorem OAI.MaxCutGames.BinaryTokenMachine.joinTrace_inline_MachineBinaryTokenMachine line 650
  76. theorem OAI.MaxCutGames.BinaryTokenMachine.clauseTrace line 655

    Source documentation

    Three literal subroutines return to the next clause boundary.

    theorem clauseTrace (clause : Clause) (suffix reversed output : List Bool)
    (register : Option Bool) :
    (advance machine.step)^[clauseNameSize clause + 6]
      (some (cfg (some (.sign 0)) (clauseBits clause ++ suffix) reversed output register)) =
      some (cfg (some .clause) suffix ((clauseBits clause).reverse ++ reversed) output) := by
…

    Mentions: OAI.MaxCutGames.BinaryTokenMachine.cfg

  77. def OAI.MaxCutGames.BinaryTokenMachine.tokens line 676
  78. theorem OAI.MaxCutGames.BinaryTokenMachine.tokens_nil line 678
  79. theorem OAI.MaxCutGames.BinaryTokenMachine.tokens_cons line 680
  80. theorem OAI.MaxCutGames.BinaryTokenMachine.tokens_length line 684
  81. theorem OAI.MaxCutGames.BinaryTokenMachine.stripTrace line 694

    Source documentation

    Exact first-pass run, retaining the unread suffix and ambient output.

    theorem stripTrace (clauses : List Clause) (suffix reversed output : List Bool)
    (register : Option Bool) :
    (advance machine.step)^[7 * clauses.length + namesBitSize clauses + 1]
      (some (cfg (some .clause) (clausesBits clauses ++ suffix) reversed output register)) =
      some (cfg (some .restore) suffix ((tokens clauses).reverse ++ reversed) output) := by
…

    Mentions: OAI.MaxCutGames.BinaryTokenMachine.cfg, OAI.MaxCutGames.BinaryTokenMachine.tokens

  82. theorem OAI.MaxCutGames.BinaryTokenMachine.restoreTrace line 726
  83. theorem OAI.MaxCutGames.BinaryTokenMachine.initList_eq line 742
  84. theorem OAI.MaxCutGames.BinaryTokenMachine.haltList_eq line 749
  85. theorem OAI.MaxCutGames.BinaryTokenMachine.acceptTrace line 756
  86. theorem OAI.MaxCutGames.BinaryTokenMachine.haltStep line 774
  87. theorem OAI.MaxCutGames.BinaryTokenMachine.tokenTrace line 780

    Source documentation

    Exact transition count for the complete finite-machine computation.

    theorem tokenTrace (formula : Formula) :
    (advance machine.step)^[13 * formula.clauses.length +
        3 * namesBitSize formula.clauses + 3]
      (some (initList machine (formulaBits formula))) =
      some (haltList machine (tokens formula.clauses)) := by
…

    Mentions: OAI.MaxCutGames.BinaryTokenMachine.machine, OAI.MaxCutGames.BinaryTokenMachine.tokens

  88. theorem OAI.MaxCutGames.BinaryTokenMachine.tokenSteps_le line 789
  89. def OAI.MaxCutGames.BinaryTokenMachine.outputsInTime line 795
  90. def OAI.MaxCutGames.BinaryTokenMachine.computableInPolyTime line 804

    Source documentation

    A displayed finite machine and linear polynomial in the ordinary input bit length, proved by the transitions above rather than assumed by a caller.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime BinaryEncoding.formulaBits (id : List Bool → List Bool)
      (fun formula => tokens formula.clauses) where
…

    Mentions: OAI.MaxCutGames.BinaryEncoding.formulaBits, OAI.MaxCutGames.BinaryTokenMachine.tokens

  91. theorem OAI.MaxCutGames.BinaryTokenMachine.machine_finiteAlphabet line 819