OAI/Computability/MaxCut/Machines/MachineClone100.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

A finite-state validator for the concrete ordinary-binary formula encoding. It checks clause and literal framing, canonical name payloads, and the unique terminal formula marker. The last-digit register starts at true for each name, so the empty payload is accepted as zero while a nonempty payload must end in one. Every bit following the terminal formula marker causes rejection.

  1. def OAI.MaxCutGames.Explicit.MachineClone100.indices line 15
  2. def OAI.MaxCutGames.Explicit.MachineClone100.triples line 18
  3. theorem OAI.MaxCutGames.Explicit.MachineClone100.triples_length line 20
  4. theorem OAI.MaxCutGames.Explicit.MachineClone100.triples_nonempty line 23
  5. theorem OAI.MaxCutGames.Explicit.MachineClone100.equation_words line 28
  6. theorem OAI.MaxCutGames.Explicit.MachineClone100.body_words line 36
  7. theorem OAI.MaxCutGames.Explicit.MachineClone100.input_words_eq line 42
  8. theorem OAI.MaxCutGames.Explicit.MachineClone100.input_bits_eq line 51
  9. theorem OAI.MaxCutGames.Explicit.MachineClone100.serialized_polynomial_inline_MachineClone100 line 57
  10. theorem OAI.MaxCutGames.Explicit.MachineClone100.size_bound line 70
  11. def OAI.MaxCutGames.Explicit.MachineClone100.computation line 82
  12. theorem OAI.MaxCutGames.Explicit.MachineClone100.finiteAlphabet line 87
  13. def OAI.MaxCutGames.Explicit.MachineClone100.fullRunInTime line 90
  14. inductive OAI.MaxCutGames.BinaryValidatorMachine.Mode line 108
  15. def OAI.MaxCutGames.BinaryValidatorMachine.afterName line 117
  16. def OAI.MaxCutGames.BinaryValidatorMachine.nextMode line 120
  17. def OAI.MaxCutGames.BinaryValidatorMachine.run line 130
  18. theorem OAI.MaxCutGames.BinaryValidatorMachine.run_reject line 134
  19. theorem OAI.MaxCutGames.BinaryValidatorMachine.run_done_iff line 139
  20. theorem OAI.MaxCutGames.BinaryValidatorMachine.finalDigit_true_iff_inline_MachineBinaryValidatorMachine line 144
  21. theorem OAI.MaxCutGames.BinaryValidatorMachine.run_frame line 162

    Source documentation

    A valid framed payload advances exactly to the next literal or clause.

    theorem run_frame (slot : Fin 3) (bits rest : List Bool) (last : Bool)
    (valid : BinaryNameMachine.finalDigit bits (some last) = some true) :
    run (.name slot last) (frame bits ++ rest) = run (afterName slot) rest := by
…

    Mentions: OAI.MaxCutGames.BinaryNameMachine.finalDigit, OAI.MaxCutGames.BinaryValidatorMachine.run, OAI.MaxCutGames.BinaryValidatorMachine.afterName

  22. theorem OAI.MaxCutGames.BinaryValidatorMachine.run_name line 174
  23. theorem OAI.MaxCutGames.BinaryValidatorMachine.run_literal line 179
  24. theorem OAI.MaxCutGames.BinaryValidatorMachine.run_clause line 184
  25. theorem OAI.MaxCutGames.BinaryValidatorMachine.run_clauses line 188
  26. theorem OAI.MaxCutGames.BinaryValidatorMachine.run_formula line 195
  27. theorem OAI.MaxCutGames.BinaryValidatorMachine.frame_inverse line 199

    Source documentation

    Any accepting name phase consumes a complete frame with a valid last digit.

    theorem frame_inverse (slot : Fin 3) (last : Bool) (input : List Bool)
    (accepted : run (.name slot last) input = .done) :
    ∃ bits rest, input = frame bits ++ rest ∧
      BinaryNameMachine.finalDigit bits (some last) = some true ∧
      run (afterName slot) rest = .done := by
…

    Mentions: OAI.MaxCutGames.BinaryValidatorMachine.run, OAI.MaxCutGames.BinaryNameMachine.finalDigit, OAI.MaxCutGames.BinaryValidatorMachine.afterName

  28. theorem OAI.MaxCutGames.BinaryValidatorMachine.name_inverse line 229
  29. theorem OAI.MaxCutGames.BinaryValidatorMachine.literal_inverse line 238
  30. theorem OAI.MaxCutGames.BinaryValidatorMachine.clause_inverse line 249
  31. theorem OAI.MaxCutGames.BinaryValidatorMachine.clauses_inverse_aux_inline_MachineBinaryValidatorMachine line 262
  32. theorem OAI.MaxCutGames.BinaryValidatorMachine.run_clause_iff line 291

    Source documentation

    Exact language recognition, including rejection of incomplete, padded, or trailing input.

    theorem run_clause_iff (input : List Bool) :
    run .clause input = .done ↔ ∃ formula, input = formulaBits formula := by
…

    Mentions: OAI.MaxCutGames.BinaryValidatorMachine.run

  33. def OAI.MaxCutGames.BinaryValidatorMachine.accepts line 301
  34. theorem OAI.MaxCutGames.BinaryValidatorMachine.accepts_eq_decode line 303
  35. abbrev OAI.MaxCutGames.BinaryValidatorMachine.Alphabet line 325
  36. abbrev OAI.MaxCutGames.BinaryValidatorMachine.State line 326
  37. def OAI.MaxCutGames.BinaryValidatorMachine.instruction line 330

    Source documentation

    Every nonempty pop performs exactly one finite DFA transition. The empty pop emits the final acceptance bit, resets control, and halts.

    def instruction : TM2.Stmt Alphabet Unit State :=
…

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

  38. abbrev OAI.MaxCutGames.BinaryValidatorMachine.machine line 338
  39. def OAI.MaxCutGames.BinaryValidatorMachine.tapes line 349
  40. def OAI.MaxCutGames.BinaryValidatorMachine.cfg line 353
  41. theorem OAI.MaxCutGames.BinaryValidatorMachine.tapes_input line 357
  42. theorem OAI.MaxCutGames.BinaryValidatorMachine.tapes_output line 360
  43. theorem OAI.MaxCutGames.BinaryValidatorMachine.update_input_inline_MachineBinaryValidatorMachine line 363
  44. theorem OAI.MaxCutGames.BinaryValidatorMachine.update_output_inline_MachineBinaryValidatorMachine line 368
  45. theorem OAI.MaxCutGames.BinaryValidatorMachine.step_empty line 373
  46. theorem OAI.MaxCutGames.BinaryValidatorMachine.step_cons line 380
  47. theorem OAI.MaxCutGames.BinaryValidatorMachine.runTrace line 390

    Source documentation

    Exact execution on every word, including malformed, noncanonical, and trailing input. Rejection drains the entire input through a finite sink state.

    theorem runTrace (input output : List Bool) (mode : Mode) (register : Option Bool) :
    (advance machine.step)^[input.length + 1]
      (some (cfg (some ()) input output mode register)) =
      some (cfg none [] (decide (run mode input = .done) :: output) .clause) := by
…

    Mentions: OAI.MaxCutGames.BinaryValidatorMachine.Mode, OAI.MaxCutGames.BinaryValidatorMachine.cfg, OAI.MaxCutGames.BinaryValidatorMachine.run

  48. theorem OAI.MaxCutGames.BinaryValidatorMachine.initList_eq line 404
  49. theorem OAI.MaxCutGames.BinaryValidatorMachine.haltList_eq line 411
  50. theorem OAI.MaxCutGames.BinaryValidatorMachine.validatorTrace line 419

    Source documentation

    A total raw-bit validator with the exact same answer as the binary codec.

    theorem validatorTrace (input : List Bool) :
    (advance machine.step)^[input.length + 1]
      (some (initList machine input)) =
      some (haltList machine [(BinaryEncoding.decodeFormula input).isSome]) := by
…

    Mentions: OAI.MaxCutGames.BinaryValidatorMachine.machine, OAI.MaxCutGames.BinaryEncoding.decodeFormula

  51. def OAI.MaxCutGames.BinaryValidatorMachine.outputsInTime line 431
  52. def OAI.MaxCutGames.BinaryValidatorMachine.computableInPolyTime line 440

    Source documentation

    The polynomial certificate supplies the explicit machine above. There is no assumed parser, verifier, or runtime hypothesis.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime (id : List Bool → List Bool) (id : List Bool → List Bool)
      (fun input => [(BinaryEncoding.decodeFormula input).isSome]) where
…

    Mentions: OAI.MaxCutGames.BinaryEncoding.decodeFormula

  53. theorem OAI.MaxCutGames.BinaryValidatorMachine.machine_finiteAlphabet line 454
  54. inductive OAI.MaxCutGames.BinaryTotalInputMachine.Label line 477
  55. abbrev OAI.MaxCutGames.BinaryTotalInputMachine.Label.enumList line 484
  56. theorem OAI.MaxCutGames.BinaryTotalInputMachine.Label.enumList_getElem?_ctorIdx_eq line 486
  57. theorem OAI.MaxCutGames.BinaryTotalInputMachine.Label.enumList_nodup line 490
  58. instance OAI.MaxCutGames.BinaryTotalInputMachine.(instance at line 492) line 492
  59. abbrev OAI.MaxCutGames.BinaryTotalInputMachine.Alphabet line 496
  60. abbrev OAI.MaxCutGames.BinaryTotalInputMachine.State line 497
  61. def OAI.MaxCutGames.BinaryTotalInputMachine.rejectedWord line 499
  62. def OAI.MaxCutGames.BinaryTotalInputMachine.instruction line 503

    Source documentation

    Stack zero is the input, one the output, and two the reversed input. Branches inspect only the finite validator state and the popped symbol.

    def instruction : Label → TM2.Stmt Alphabet Label State
  | .scan =>
      .pop 0 (fun state head => (state.1, head))
        (.branch (fun state => state.2.isSome)
          (.push 2 (fun state => state.2.getD false)
            (.load (fun state => (nextMode state.1 (state.2.getD false), none))
              (.goto fun _ => .scan)))
          (.branch (fun state => decide (state.1 = .done))
            (.load (fun _ => (.clause, none)) (.goto fun _ => .restore))
            (.load (fun _ => (.clause, none)) (.goto fun _ => .drain))))
  | .restore => loopAt 2 1 id false .restore none
  | .drain => MachineDrain.drain 2 .drain (some .rejectOutput)
…

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

  63. abbrev OAI.MaxCutGames.BinaryTotalInputMachine.machine line 517
  64. def OAI.MaxCutGames.BinaryTotalInputMachine.tapes line 528
  65. def OAI.MaxCutGames.BinaryTotalInputMachine.cfg line 533
  66. theorem OAI.MaxCutGames.BinaryTotalInputMachine.tapes_input line 537
  67. theorem OAI.MaxCutGames.BinaryTotalInputMachine.tapes_output line 540
  68. theorem OAI.MaxCutGames.BinaryTotalInputMachine.tapes_saved line 543
  69. theorem OAI.MaxCutGames.BinaryTotalInputMachine.update_input_inline_MachineBinaryTotalInputMachine line 546
  70. theorem OAI.MaxCutGames.BinaryTotalInputMachine.update_output_inline_MachineBinaryTotalInputMachine line 552
  71. theorem OAI.MaxCutGames.BinaryTotalInputMachine.update_saved_inline_MachineBinaryTotalInputMachine line 558
  72. def OAI.MaxCutGames.BinaryTotalInputMachine.afterScan line 564
  73. theorem OAI.MaxCutGames.BinaryTotalInputMachine.step_scan_empty line 566
  74. theorem OAI.MaxCutGames.BinaryTotalInputMachine.step_scan_cons line 573
  75. theorem OAI.MaxCutGames.BinaryTotalInputMachine.scanTrace line 583

    Source documentation

    The finite DFA reads every bit, including all bits in its rejection sink. The trace also records the physical reversed copy needed by the second phase.

    theorem scanTrace (input output saved : List Bool) (mode : Mode) (register : Option Bool) :
    (advance machine.step)^[input.length + 1]
      (some (cfg (some .scan) input output saved mode register)) =
      some (cfg (some (afterScan (run mode input))) [] output (input.reverse ++ saved)) := by
…

    Mentions: OAI.MaxCutGames.BinaryTotalInputMachine.cfg, OAI.MaxCutGames.BinaryTotalInputMachine.afterScan

  76. theorem OAI.MaxCutGames.BinaryTotalInputMachine.restoreTrace line 599
  77. theorem OAI.MaxCutGames.BinaryTotalInputMachine.drainTrace line 611
  78. theorem OAI.MaxCutGames.BinaryTotalInputMachine.step_rejectOutput line 622
  79. theorem OAI.MaxCutGames.BinaryTotalInputMachine.joinTrace_inline_MachineBinaryTotalInputMachine line 632
  80. theorem OAI.MaxCutGames.BinaryTotalInputMachine.acceptedTrace line 636
  81. theorem OAI.MaxCutGames.BinaryTotalInputMachine.rejectedTrace line 647
  82. theorem OAI.MaxCutGames.BinaryTotalInputMachine.initList_eq line 662
  83. theorem OAI.MaxCutGames.BinaryTotalInputMachine.haltList_eq line 669
  84. def OAI.MaxCutGames.BinaryTotalInputMachine.steps line 676
  85. theorem OAI.MaxCutGames.BinaryTotalInputMachine.steps_le line 679
  86. theorem OAI.MaxCutGames.BinaryTotalInputMachine.totalTrace line 684

    Source documentation

    Full correspondence on every raw word, with no validity premise.

    theorem totalTrace (input : List Bool) :
    (advance machine.step)^[steps input] (some (initList machine input)) =
      some (haltList machine (BinaryEncoding.formulaBits (BinaryLanguage.totalParsed input))) := by
…

    Mentions: OAI.MaxCutGames.BinaryTotalInputMachine.steps, OAI.MaxCutGames.BinaryTotalInputMachine.machine, OAI.MaxCutGames.BinaryEncoding.formulaBits, OAI.MaxCutGames.BinaryLanguage.totalParsed

  87. def OAI.MaxCutGames.BinaryTotalInputMachine.outputsInTime line 706
  88. def OAI.MaxCutGames.BinaryTotalInputMachine.computableInPolyTime line 716

    Source documentation

    The certificate contains the displayed total machine and its linear trace; it assumes no execution, parser-cost, or malformed-input premise.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime (id : List Bool → List Bool) BinaryEncoding.formulaBits
      BinaryLanguage.totalParsed where
…

    Mentions: OAI.MaxCutGames.BinaryEncoding.formulaBits, OAI.MaxCutGames.BinaryLanguage.totalParsed

  89. theorem OAI.MaxCutGames.BinaryTotalInputMachine.machine_finiteAlphabet line 730
  90. theorem OAI.MaxCutGames.BinaryTotalInputMachine.computation_finiteAlphabet line 734