OAI/Computability/MaxCut/Machines/MachineBinaryRenameWords.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

The word-level correspondence used by the ordinary-binary renaming machine. Literal occurrences stay in clause order, and equality is tested on canonical binary payloads. The output body consists of the first occurrence index and the sign of every literal, in the inherited dense formula codec.

  1. def OAI.MaxCutGames.BinaryRenameWords.clauseLiterals line 18
  2. def OAI.MaxCutGames.BinaryRenameWords.literals line 20
  3. def OAI.MaxCutGames.BinaryRenameWords.token line 22
  4. def OAI.MaxCutGames.BinaryRenameWords.tokens line 25
  5. theorem OAI.MaxCutGames.BinaryRenameWords.literals_nil line 28
  6. theorem OAI.MaxCutGames.BinaryRenameWords.literals_cons line 30
  7. theorem OAI.MaxCutGames.BinaryRenameWords.literals_length line 33
  8. theorem OAI.MaxCutGames.BinaryRenameWords.tokens_length line 39
  9. theorem OAI.MaxCutGames.BinaryRenameWords.literals_names line 42
  10. theorem OAI.MaxCutGames.BinaryRenameWords.tokens_payloads line 47
  11. theorem OAI.MaxCutGames.BinaryRenameWords.token_bits line 52
  12. theorem OAI.MaxCutGames.BinaryRenameWords.tokens_stream line 58

    Source documentation

    The marker-removal machine's actual output is the search machine's stream.

    theorem tokens_stream (cs : List Clause) :
    BinaryNameSearch.stream (tokens cs) = BinaryTokenMachine.tokens cs := by
…

    Mentions: OAI.MaxCutGames.BinaryNameSearch.stream, OAI.MaxCutGames.BinaryRenameWords.tokens, OAI.MaxCutGames.BinaryTokenMachine.tokens

  13. theorem OAI.MaxCutGames.BinaryRenameWords.tokens_canonical line 69
  14. theorem OAI.MaxCutGames.BinaryRenameWords.payload_index line 75
  15. theorem OAI.MaxCutGames.BinaryRenameWords.token_payload_mem line 80
  16. theorem OAI.MaxCutGames.BinaryRenameWords.payloadSize_tokens line 87
  17. def OAI.MaxCutGames.BinaryRenameWords.outputLiteral line 100
  18. def OAI.MaxCutGames.BinaryRenameWords.body line 104
  19. theorem OAI.MaxCutGames.BinaryRenameWords.encoded_clause line 107
  20. theorem OAI.MaxCutGames.BinaryRenameWords.encodeWords_flatMap_inline_MachineBinaryRenameWords line 115
  21. theorem OAI.MaxCutGames.BinaryRenameWords.encoded_body line 123

    Source documentation

    The output contains every literal occurrence, including repetitions.

    theorem encoded_body (F : Formula) :
    Complexity.encodeWords ((BinaryOccurrenceRename.renamed F).clauses.flatMap
      Complexity.clauseWords) = body F := by
…

    Mentions: OAI.MaxCutGames.BinaryOccurrenceRename.renamed, OAI.MaxCutGames.BinaryRenameWords.body

  22. theorem OAI.MaxCutGames.BinaryRenameWords.encoded_renamed line 137

    Source documentation

    Exact ordinary-binary-machine target, including its two count headers.

    theorem encoded_renamed (F : Formula) :
    Complexity.formulaBits (BinaryOccurrenceRename.renamed F) =
      Complexity.encodeWord (3 * F.clauses.length) ++
        Complexity.encodeWord F.clauses.length ++ body F := by
…

    Mentions: OAI.MaxCutGames.BinaryOccurrenceRename.renamed, OAI.MaxCutGames.BinaryRenameWords.body

  23. abbrev OAI.MaxCutGames.BinaryHeaderMachine.Alphabet line 168
  24. abbrev OAI.MaxCutGames.BinaryHeaderMachine.State line 169
  25. def OAI.MaxCutGames.BinaryHeaderMachine.delimiter line 176

    Source documentation

    A fixed one-bit push; the finite register is cleared before continuation.

    def delimiter (destination : K) (next : Λ) : TM2.Stmt (Alphabet (K := K)) Λ (State A) :=
…

    Mentions: OAI.MaxCutGames.BinaryHeaderMachine.Alphabet, OAI.MaxCutGames.BinaryHeaderMachine.State

  26. def OAI.MaxCutGames.BinaryHeaderMachine.tapes line 180
  27. theorem OAI.MaxCutGames.BinaryHeaderMachine.tapes_variables line 185
  28. theorem OAI.MaxCutGames.BinaryHeaderMachine.tapes_clauses line 192
  29. theorem OAI.MaxCutGames.BinaryHeaderMachine.tapes_destination line 199
  30. theorem OAI.MaxCutGames.BinaryHeaderMachine.tapes_other line 205
  31. theorem OAI.MaxCutGames.BinaryHeaderMachine.update_variables_inline_MachineBinaryHeaderMachine line 211
  32. theorem OAI.MaxCutGames.BinaryHeaderMachine.update_clauses_inline_MachineBinaryHeaderMachine line 228
  33. theorem OAI.MaxCutGames.BinaryHeaderMachine.update_destination_inline_MachineBinaryHeaderMachine line 242
  34. theorem OAI.MaxCutGames.BinaryHeaderMachine.clauseDelimiterStep line 261
  35. theorem OAI.MaxCutGames.BinaryHeaderMachine.variableDelimiterStep line 273
  36. theorem OAI.MaxCutGames.BinaryHeaderMachine.clauseCounterTrace line 285
  37. theorem OAI.MaxCutGames.BinaryHeaderMachine.variableCounterTrace line 305
  38. theorem OAI.MaxCutGames.BinaryHeaderMachine.joinTrace_inline_MachineBinaryHeaderMachine line 324
  39. theorem OAI.MaxCutGames.BinaryHeaderMachine.headerTrace line 331

    Source documentation

    The actual four-phase routine, with exact unary header and preserved body.

    theorem headerTrace (n m : Nat) (body : List Bool) (register : Option Bool) :
    (advance (TM2.step program))^[n + m + 4]
      (some ⟨some clauseStart, (ambient, register),
        tapes variableTape clauses destination base
          (List.replicate n true) (List.replicate m true) body⟩) =
      some ⟨exit, (ambient, none),
        tapes variableTape clauses destination base [] [] (encodeWord n ++ encodeWord m ++ body)⟩ := by
…

    Mentions: OAI.MaxCutGames.BinaryHeaderMachine.tapes

  40. def OAI.MaxCutGames.BinaryHeaderMachine.headerInTime line 360
  41. abbrev OAI.MaxCutGames.BinaryHeaderMachine.ConcreteTape line 375
  42. abbrev OAI.MaxCutGames.BinaryHeaderMachine.ConcreteLabel line 376
  43. def OAI.MaxCutGames.BinaryHeaderMachine.concreteProgram line 378
  44. abbrev OAI.MaxCutGames.BinaryHeaderMachine.machine line 385
  45. def OAI.MaxCutGames.BinaryHeaderMachine.start line 397

    Source documentation

    Concrete entry configuration carries two physical counters and the body.

    def start (n m : Nat) (body : List Bool) : machine.Cfg :=
…
  46. theorem OAI.MaxCutGames.BinaryHeaderMachine.haltList_eq line 401
  47. def OAI.MaxCutGames.BinaryHeaderMachine.machineInTime line 410

    Source documentation

    Genuine staged execution of the concrete four-label finite machine.

    def machineInTime (n m : Nat) (body : List Bool) :
    StateTransition.EvalsToInTime machine.step (start n m body)
      (some (haltList machine (encodeWord n ++ encodeWord m ++ body))) (n + m + 4) := by
…

    Mentions: OAI.MaxCutGames.BinaryHeaderMachine.start, OAI.MaxCutGames.BinaryHeaderMachine.machine

  48. theorem OAI.MaxCutGames.BinaryHeaderMachine.machine_finiteAlphabet line 420
  49. abbrev OAI.MaxCutGames.BinaryRenameMachine.Tape line 439
  50. abbrev OAI.MaxCutGames.BinaryRenameMachine.Alphabet line 440
  51. abbrev OAI.MaxCutGames.BinaryRenameMachine.State line 441
  52. inductive OAI.MaxCutGames.BinaryRenameMachine.Label line 443
  53. def OAI.MaxCutGames.BinaryRenameMachine.loopTapes line 450
  54. theorem OAI.MaxCutGames.BinaryRenameMachine.loopTapes_injective line 452
  55. def OAI.MaxCutGames.BinaryRenameMachine.program line 457
  56. abbrev OAI.MaxCutGames.BinaryRenameMachine.machine line 470
  57. def OAI.MaxCutGames.BinaryRenameMachine.tapes line 481
  58. def OAI.MaxCutGames.BinaryRenameMachine.cfg line 491
  59. theorem OAI.MaxCutGames.BinaryRenameMachine.initList_eq line 496
  60. theorem OAI.MaxCutGames.BinaryRenameMachine.haltList_eq line 503
  61. theorem OAI.MaxCutGames.BinaryRenameMachine.copyTrace line 510
  62. theorem OAI.MaxCutGames.BinaryRenameMachine.restoreTrace line 527
  63. theorem OAI.MaxCutGames.BinaryRenameMachine.headerTrace line 548
  64. theorem OAI.MaxCutGames.BinaryRenameMachine.cleanupTrace line 572
  65. theorem OAI.MaxCutGames.BinaryRenameMachine.outputBody_eq line 590
  66. theorem OAI.MaxCutGames.BinaryRenameMachine.loopTrace line 605
  67. theorem OAI.MaxCutGames.BinaryRenameMachine.joinTrace_inline_MachineBinaryRenameMachine line 648
  68. def OAI.MaxCutGames.BinaryRenameMachine.steps line 652
  69. theorem OAI.MaxCutGames.BinaryRenameMachine.renameTrace line 659
  70. theorem OAI.MaxCutGames.BinaryRenameMachine.clause_count_le_stream line 678
  71. theorem OAI.MaxCutGames.BinaryRenameMachine.body_length_le line 683
  72. def OAI.MaxCutGames.BinaryRenameMachine.timePolynomial line 694
  73. theorem OAI.MaxCutGames.BinaryRenameMachine.steps_le line 698
  74. def OAI.MaxCutGames.BinaryRenameMachine.outputsInTime line 718
  75. def OAI.MaxCutGames.BinaryRenameMachine.tokenComputation line 728

    Source documentation

    The token-stream phase has a displayed finite machine and actual execution bound; its polynomial argument is the token stream's physical bit length.

    noncomputable def tokenComputation :
    TM2ComputableInPolyTime (fun formula : BinaryFormula.Formula =>
      BinaryTokenMachine.tokens formula.clauses) formulaBits BinaryOccurrenceRename.renamed where
…

    Mentions: OAI.MaxCutGames.BinaryFormula.Formula, OAI.MaxCutGames.BinaryTokenMachine.tokens, OAI.MaxCutGames.BinaryOccurrenceRename.renamed

  76. def OAI.MaxCutGames.BinaryRenameMachine.preprocessing line 743

    Source documentation

    Repackage the checked marker-removal machine without changing any machine or word: the intermediate semantic value is the same formula.

    noncomputable def preprocessing :
    TM2ComputableInPolyTime BinaryEncoding.formulaBits
      (fun formula : BinaryFormula.Formula => BinaryTokenMachine.tokens formula.clauses)
      (id : BinaryFormula.Formula → BinaryFormula.Formula) where
…

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

  77. def OAI.MaxCutGames.BinaryRenameMachine.computableInPolyTime line 755

    Source documentation

    Actual finite-alphabet polynomial-time sparse binary to dense unary renaming. Sparse name magnitudes are never expanded in unary.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime BinaryEncoding.formulaBits formulaBits
      BinaryOccurrenceRename.renamed :=
…

    Mentions: OAI.MaxCutGames.BinaryEncoding.formulaBits, OAI.MaxCutGames.BinaryOccurrenceRename.renamed

  78. theorem OAI.MaxCutGames.BinaryRenameMachine.machine_finiteAlphabet line 760
  79. theorem OAI.MaxCutGames.BinaryRenameMachine.computation_finiteAlphabet line 764