OAI/Computability/MaxCut/Machines/MachineBinaryFormula.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

An explicit ordinary-binary codec for sparse-name three-literal CNF.

A natural name uses its canonical little-endian binary digits. Each payload digit b is represented by the pair true,b; false terminates the name. Zero has the empty payload and therefore the one-bit encoding [false]. A literal is its sign bit followed by its name. A clause contains three literal encodings. A formula contains true followed by each clause, then one final false. There is no unary expansion of a variable name, declared variable universe, or deduplication of literal or clause occurrences.

The parser rejects noncanonical name payloads, incomplete literals/clauses, and trailing input. The input length is within a fixed factor of the total ordinary binary name lengths plus signs and clause framing. Machine correspondence and runtime are proved separately; these output-size bounds are not time bounds.

  1. def OAI.MaxCutGames.BinaryFormula.sourceNames line 12
  2. def OAI.MaxCutGames.BinaryFormula.activeNames line 17

    Source documentation

    Explicit list of occurring names, with duplicates removed. The list lengths depend only on occurrences; no interval of natural-number names is enumerated.

    def activeNames (F : Formula) : List Nat :=
…

    Mentions: OAI.MaxCutGames.BinaryFormula.Formula

  3. theorem OAI.MaxCutGames.BinaryFormula.literal_mem_active line 20
  4. def OAI.MaxCutGames.BinaryFormula.compactIndex line 28
  5. def OAI.MaxCutGames.BinaryFormula.decodeName line 32
  6. def OAI.MaxCutGames.BinaryFormula.compactLiteral line 35
  7. def OAI.MaxCutGames.BinaryFormula.compactClause line 39
  8. def OAI.MaxCutGames.BinaryFormula.compactClauses line 45
  9. def OAI.MaxCutGames.BinaryFormula.dense line 48
  10. def OAI.MaxCutGames.BinaryFormula.restrictAssignment line 52
  11. def OAI.MaxCutGames.BinaryFormula.extendAssignment line 55
  12. theorem OAI.MaxCutGames.BinaryFormula.decode_compactIndex line 59
  13. theorem OAI.MaxCutGames.BinaryFormula.compactIndex_injective line 65

    Source documentation

    Distinct occurring names remain distinct. Repeated occurrences of one name use the same index, since the proof argument of compactIndex is irrelevant.

    theorem compactIndex_injective (F : Formula) (u v : Nat)
    (hu : u ∈ activeNames F) (hv : v ∈ activeNames F)
    (h : compactIndex F u hu = compactIndex F v hv) : u = v := by
…

    Mentions: OAI.MaxCutGames.BinaryFormula.Formula, OAI.MaxCutGames.BinaryFormula.activeNames, OAI.MaxCutGames.BinaryFormula.compactIndex

  14. theorem OAI.MaxCutGames.BinaryFormula.compactLiteral_positive line 71
  15. theorem OAI.MaxCutGames.BinaryFormula.eval_compact_restrict line 74
  16. theorem OAI.MaxCutGames.BinaryFormula.eval_compact_extend line 80
  17. def OAI.MaxCutGames.BinaryFormula.evaluationList line 89
  18. theorem OAI.MaxCutGames.BinaryFormula.evaluationList_restrict line 94

    Source documentation

    Evaluation lists retain every clause occurrence, so this is stronger than merely preserving satisfiability or the set of distinct clauses.

    theorem evaluationList_restrict (F : Formula) (A : Nat → Bool) :
    PCP.NameCompaction.evaluationList (dense F) (restrictAssignment F A) =
      evaluationList F A := by
…

    Mentions: OAI.MaxCutGames.BinaryFormula.Formula, OAI.MaxCutGames.BinaryFormula.dense, OAI.MaxCutGames.BinaryFormula.restrictAssignment, OAI.MaxCutGames.BinaryFormula.evaluationList

  19. theorem OAI.MaxCutGames.BinaryFormula.evaluationList_extend line 102
  20. def OAI.MaxCutGames.BinaryFormula.failedCount line 116
  21. theorem OAI.MaxCutGames.BinaryFormula.failedCount_restrict line 119
  22. theorem OAI.MaxCutGames.BinaryFormula.failedCount_extend line 123
  23. theorem OAI.MaxCutGames.BinaryFormula.clauseNames_flat_length line 127
  24. theorem OAI.MaxCutGames.BinaryFormula.dense_clause_count line 136
  25. theorem OAI.MaxCutGames.BinaryFormula.dense_variable_bound line 142

    Source documentation

    No greatest-name bound occurs: even very large, sparsely used names yield at most three dense «variables» per explicitly listed clause.

    theorem dense_variable_bound (F : Formula) :
    (dense F).«variables» ≤ 3 * F.clauses.length := by
…

    Mentions: OAI.MaxCutGames.BinaryFormula.Formula, OAI.MaxCutGames.BinaryFormula.dense

  26. theorem OAI.MaxCutGames.BinaryFormula.dense_completeness line 147
  27. theorem OAI.MaxCutGames.BinaryFormula.dense_reflects line 156
  28. theorem OAI.MaxCutGames.BinaryFormula.dense_satisfiable_iff line 166
  29. theorem OAI.MaxCutGames.BinaryFormula.dense_preserves_gap line 170
  30. theorem OAI.MaxCutGames.BinaryFormula.dense_encoding_bound line 180

    Source documentation

    Size of the reused dense formula encoding, bounded only by the number of explicit clause occurrences. This does not assert a binary input parser or a running-time bound for sparse-to-dense conversion.

    theorem dense_encoding_bound (F : Formula) :
    (Complexity.formulaBits (dense F)).length ≤
      9 * F.clauses.length * F.clauses.length + 10 * F.clauses.length + 2 := by
…

    Mentions: OAI.MaxCutGames.BinaryFormula.Formula, OAI.MaxCutGames.BinaryFormula.dense

  31. theorem OAI.MaxCutGames.BinaryEncoding.dense_encoding_bound line 222

    Source documentation

    The existing dense unary output is polynomial in this ordinary binary input length. This remains an output-size theorem, not a runtime certificate.

    theorem dense_encoding_bound (formula : Formula) :
    (MaxCutGames.Foundations.Complexity.formulaBits (dense formula)).length ≤
      9 * (formulaBits formula).length * (formulaBits formula).length +
      10 * (formulaBits formula).length + 2 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.formulaBits, OAI.MaxCutGames.BinaryEncoding.formulaBits

  32. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCompare.Alphabet line 250
  33. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCompare.State line 251
  34. def OAI.MaxCutGames.Foundations.Complexity.MachineCompare.exitAt line 254

    Source documentation

    An optional continuation, without reading or writing any tape.

    def exitAt (exit : Option Λ) : TM2.Stmt (Alphabet K) Λ (State σ) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCompare.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.State

  35. def OAI.MaxCutGames.Foundations.Complexity.MachineCompare.finish line 260

    Source documentation

    Clear both head registers and the mismatch flag after choosing the exit.

    def finish (exit : Option Λ) : TM2.Stmt (Alphabet K) Λ (State σ) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCompare.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.State

  36. def OAI.MaxCutGames.Foundations.Complexity.MachineCompare.loop line 265

    Source documentation

    The only comparison performed by the program is on two Option Bool heads. In particular, no statement is given a whole-list equality oracle.

    def loop (left right : K) (loopLabel : Λ) (equalExit differentExit : Option Λ) :
    TM2.Stmt (Alphabet K) Λ (State σ) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCompare.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.State

  37. def OAI.MaxCutGames.Foundations.Complexity.MachineCompare.mismatch line 276

    Source documentation

    Specification-only outcome, also recording an earlier mismatch.

    def mismatch (flag : Bool) (leftWord rightWord : List Bool) : Bool :=
…
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.mismatch_nil_nil line 279
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.mismatch_nil_cons line 282
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.mismatch_cons_nil line 285
  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.mismatch_true line 288
  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.mismatch_cons line 291
  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.stepAux_exitAt line 296
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.stepAux_finish line 301
  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.update_left_inline_MachineCompare line 307
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.update_right_inline_MachineCompare line 320
  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.step_empty line 326
  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.step_nil_cons line 343
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.step_cons_nil line 358
  50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.step_cons_cons line 373
  51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.trace_left_empty_inline_MachineCompare line 390
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.compareTrace_flag line 417

    Source documentation

    The exact trace with a possibly pre-existing mismatch. Every input symbol is consumed even when disagreement has already been detected.

    theorem compareTrace_flag (left right : K) (distinct : left ≠ right)
    (loopLabel : Λ) (equalExit differentExit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet K) Λ (State σ))
    (atLoop : program loopLabel = loop left right loopLabel equalExit differentExit)
    (base : K → List Bool) (leftWord rightWord : List Bool) (ambient : σ) (flag : Bool)
    (leftRegister rightRegister : Option Bool) :
    (MachineComposition.advance (TM2.step program))^[max leftWord.length rightWord.length + 1]
      (some ⟨some loopLabel, (ambient, flag, leftRegister, rightRegister),
        tapesAt left right base leftWord rightWord⟩) =
      some ⟨if mismatch flag leftWord rightWord then differentExit else equalExit,
        (ambient, false, none, none), tapesAt left right base [] []⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCompare.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.State, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.loop, OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.mismatch

  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.compareTrace line 454

    Source documentation

    With a clear initial flag, the final continuation tests equality of the two complete original words. Both tapes and all comparison registers are empty.

    theorem compareTrace (left right : K) (distinct : left ≠ right)
    (loopLabel : Λ) (equalExit differentExit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet K) Λ (State σ))
    (atLoop : program loopLabel = loop left right loopLabel equalExit differentExit)
    (base : K → List Bool) (leftWord rightWord : List Bool) (ambient : σ)
    (leftRegister rightRegister : Option Bool) :
    (MachineComposition.advance (TM2.step program))^[max leftWord.length rightWord.length + 1]
      (some ⟨some loopLabel, (ambient, false, leftRegister, rightRegister),
        tapesAt left right base leftWord rightWord⟩) =
      some ⟨if leftWord = rightWord then equalExit else differentExit,
        (ambient, false, none, none), tapesAt left right base [] []⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCompare.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.State, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.loop, OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance

  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.compareTrace_fromTapes line 469
  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.drained_other line 483

    Source documentation

    The final tape family agrees with the original at every unselected tape.

    theorem drained_other (left right k : K) (notLeft : k ≠ left) (notRight : k ≠ right)
    (base : K → List Bool) : tapesAt left right base [] [] k = base k :=
…
  56. def OAI.MaxCutGames.Foundations.Complexity.MachineCompare.compareInTime line 488

    Source documentation

    An actual timed execution witness, with the exact stored transition count.

    def compareInTime (left right : K) (distinct : left ≠ right)
    (loopLabel : Λ) (equalExit differentExit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet K) Λ (State σ))
    (atLoop : program loopLabel = loop left right loopLabel equalExit differentExit)
    (base : K → List Bool) (ambient : σ) (leftRegister rightRegister : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some loopLabel, (ambient, false, leftRegister, rightRegister), base⟩
      (some ⟨if base left = base right then equalExit else differentExit,
        (ambient, false, none, none), tapesAt left right base [] []⟩)
      (max (base left).length (base right).length + 1) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCompare.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.State, OAI.MaxCutGames.Foundations.Complexity.MachineCompare.loop

  57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCompare.compareInTime_steps line 503
  58. def OAI.MaxCutGames.BinaryNameMachine.frame line 521
  59. def OAI.MaxCutGames.BinaryNameMachine.finalDigit line 525
  60. def OAI.MaxCutGames.BinaryNameMachine.canonical line 529
  61. structure OAI.MaxCutGames.BinaryNameMachine.Result line 531
  62. def OAI.MaxCutGames.BinaryNameMachine.scanSpec line 538

    Source documentation

    A specification with the same one- or two-symbol cases as the program.

    def scanSpec : List Bool → List Bool → Option Bool → Result
  | [], acc, _ => ⟨false, [], acc⟩
  | false :: rest, acc, last => ⟨last.getD true, rest, acc⟩
  | [true], acc, _ => ⟨false, [], acc⟩
  | true :: bit :: rest, acc, _ => scanSpec rest (bit :: acc) (some bit)

    Mentions: OAI.MaxCutGames.BinaryNameMachine.Result

  63. def OAI.MaxCutGames.BinaryNameMachine.steps line 544
  64. theorem OAI.MaxCutGames.BinaryNameMachine.steps_le line 548
  65. theorem OAI.MaxCutGames.BinaryNameMachine.frame_length line 557
  66. theorem OAI.MaxCutGames.BinaryNameMachine.scanSpec_frame line 563
  67. theorem OAI.MaxCutGames.BinaryNameMachine.steps_frame line 572
  68. abbrev OAI.MaxCutGames.BinaryNameMachine.Alphabet line 582
  69. abbrev OAI.MaxCutGames.BinaryNameMachine.State line 583
  70. def OAI.MaxCutGames.BinaryNameMachine.clean line 585
  71. def OAI.MaxCutGames.BinaryNameMachine.exitAt line 587
  72. def OAI.MaxCutGames.BinaryNameMachine.finish line 592
  73. def OAI.MaxCutGames.BinaryNameMachine.scan line 596

    Source documentation

    Only the finite head and final-digit registers are inspected by branches.

    def scan (source destination : K) (again : Λ) (accepted rejected : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (State A) :=
…

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

  74. theorem OAI.MaxCutGames.BinaryNameMachine.stepAux_finish line 611
  75. theorem OAI.MaxCutGames.BinaryNameMachine.update_source_inline_MachineBinaryNameMachine line 616
  76. theorem OAI.MaxCutGames.BinaryNameMachine.update_destination_inline_MachineBinaryNameMachine line 627
  77. theorem OAI.MaxCutGames.BinaryNameMachine.step_empty line 641
  78. theorem OAI.MaxCutGames.BinaryNameMachine.step_end line 649
  79. theorem OAI.MaxCutGames.BinaryNameMachine.step_truncated line 660
  80. theorem OAI.MaxCutGames.BinaryNameMachine.step_digit line 668
  81. theorem OAI.MaxCutGames.BinaryNameMachine.scanTrace line 679

    Source documentation

    Total correspondence, including malformed input and its exact unread suffix.

    theorem scanTrace (input output : List Bool) (last register : Option Bool) :
    (advance (TM2.step program))^[steps input]
      (some ⟨some again, (ambient, last, register),
        tapesAt source destination base input output⟩) =
      some ⟨if (scanSpec input output last).accepted then accepted else rejected,
        clean ambient, tapesAt source destination base
          (scanSpec input output last).remaining (scanSpec input output last).reversedPayload⟩ := by
…

    Mentions: OAI.MaxCutGames.BinaryNameMachine.steps, OAI.MaxCutGames.BinaryNameMachine.scanSpec, OAI.MaxCutGames.BinaryNameMachine.clean

  82. def OAI.MaxCutGames.BinaryNameMachine.scanInTime line 714

    Source documentation

    A real timed execution; the instruction equation is the only program premise.

    def scanInTime (input output : List Bool) (last register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some again, (ambient, last, register), tapesAt source destination base input output⟩
      (some ⟨if (scanSpec input output last).accepted then accepted else rejected,
        clean ambient, tapesAt source destination base
          (scanSpec input output last).remaining (scanSpec input output last).reversedPayload⟩)
      (input.length + 1) where
…

    Mentions: OAI.MaxCutGames.BinaryNameMachine.scanSpec, OAI.MaxCutGames.BinaryNameMachine.clean

  83. theorem OAI.MaxCutGames.BinaryNameMachine.framedTrace line 728

    Source documentation

    A complete framed name needs exactly one transition per digit and one for the terminator. No transition inspects the magnitude denoted by the payload.

    theorem framedTrace (bits suffix output : List Bool) (register : Option Bool) :
    (advance (TM2.step program))^[bits.length + 1]
      (some ⟨some again, (ambient, none, register),
        tapesAt source destination base (frame bits ++ suffix) output⟩) =
      some ⟨if canonical bits then accepted else rejected, clean ambient,
        tapesAt source destination base suffix (bits.reverse ++ output)⟩ := by
…

    Mentions: OAI.MaxCutGames.BinaryNameMachine.frame, OAI.MaxCutGames.BinaryNameMachine.canonical, OAI.MaxCutGames.BinaryNameMachine.clean

  84. def OAI.MaxCutGames.BinaryNameMachine.machine line 743

    Source documentation

    One concrete machine with two Boolean stacks and finite control. The two exit labels expose acceptance to a caller; the scanner leaves them unexecuted.

    def machine : FinTM2 where
…
  85. theorem OAI.MaxCutGames.BinaryNameMachine.machine_finiteAlphabet line 754
  86. def OAI.MaxCutGames.BinaryNameMachine.machineInTime line 760

    Source documentation

    The bounded run instantiated with the displayed finite machine, including its actual entry and two actual exit labels.

    def machineInTime (input output : List Bool) :
    StateTransition.EvalsToInTime machine.step
      ⟨some (0 : Fin 3), clean (), tapesAt false true (fun _ : Bool => []) input output⟩
      (some ⟨if (scanSpec input output none).accepted then some (1 : Fin 3) else some (2 : Fin 3),
        clean (), tapesAt false true (fun _ : Bool => [])
          (scanSpec input output none).remaining (scanSpec input output none).reversedPayload⟩)
      (input.length + 1) :=
…

    Mentions: OAI.MaxCutGames.BinaryNameMachine.clean, OAI.MaxCutGames.BinaryNameMachine.scanSpec