OAI/Computability/UniqueGames/Machines/MachineBinaryValidatorMachine.lean

GitHub source file

40 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. inductive OAI.UniqueGamesTheorem.BinaryValidatorMachine.Mode line 19
  2. def OAI.UniqueGamesTheorem.BinaryValidatorMachine.afterName line 28
  3. def OAI.UniqueGamesTheorem.BinaryValidatorMachine.nextMode line 31
  4. def OAI.UniqueGamesTheorem.BinaryValidatorMachine.run line 41
  5. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.run_reject line 45
  6. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.run_done_iff line 50
  7. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.finalDigit_true_iff line 55
  8. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.run_frame line 73

    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.UniqueGamesTheorem.BinaryNameMachine.finalDigit, OAI.UniqueGamesTheorem.BinaryValidatorMachine.run, OAI.UniqueGamesTheorem.BinaryValidatorMachine.afterName

  9. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.run_name line 85
  10. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.run_literal line 90
  11. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.run_clause line 95
  12. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.run_clauses line 99
  13. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.run_formula line 106
  14. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.frame_inverse line 110

    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.UniqueGamesTheorem.BinaryValidatorMachine.run, OAI.UniqueGamesTheorem.BinaryNameMachine.finalDigit, OAI.UniqueGamesTheorem.BinaryValidatorMachine.afterName

  15. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.name_inverse line 140
  16. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.literal_inverse line 149
  17. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.clause_inverse line 160
  18. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.clauses_inverse_aux line 173
  19. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.run_clause_iff line 202

    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.UniqueGamesTheorem.BinaryValidatorMachine.run

  20. def OAI.UniqueGamesTheorem.BinaryValidatorMachine.accepts line 212
  21. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.accepts_eq_decode line 214
  22. abbrev OAI.UniqueGamesTheorem.BinaryValidatorMachine.Alphabet line 234
  23. abbrev OAI.UniqueGamesTheorem.BinaryValidatorMachine.State line 235
  24. def OAI.UniqueGamesTheorem.BinaryValidatorMachine.instruction line 239

    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.UniqueGamesTheorem.BinaryValidatorMachine.Alphabet, OAI.UniqueGamesTheorem.BinaryValidatorMachine.State

  25. abbrev OAI.UniqueGamesTheorem.BinaryValidatorMachine.machine line 247
  26. def OAI.UniqueGamesTheorem.BinaryValidatorMachine.tapes line 258
  27. def OAI.UniqueGamesTheorem.BinaryValidatorMachine.cfg line 262
  28. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.tapes_input line 266
  29. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.tapes_output line 269
  30. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.update_input line 272
  31. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.update_output line 277
  32. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.step_empty line 282
  33. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.step_cons line 289
  34. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.runTrace line 299

    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.UniqueGamesTheorem.BinaryValidatorMachine.Mode, OAI.UniqueGamesTheorem.BinaryValidatorMachine.cfg, OAI.UniqueGamesTheorem.BinaryValidatorMachine.run

  35. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.initList_eq line 313
  36. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.haltList_eq line 320
  37. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.validatorTrace line 328

    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.UniqueGamesTheorem.BinaryValidatorMachine.machine, OAI.UniqueGamesTheorem.BinaryEncoding.decodeFormula

  38. def OAI.UniqueGamesTheorem.BinaryValidatorMachine.outputsInTime line 340
  39. def OAI.UniqueGamesTheorem.BinaryValidatorMachine.computableInPolyTime line 349

    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.UniqueGamesTheorem.BinaryEncoding.decodeFormula

  40. theorem OAI.UniqueGamesTheorem.BinaryValidatorMachine.machine_finiteAlphabet line 363