OAI/Computability/MaxCut/Machines/MachineClone100Table.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

The literal four-word row used by the hundred-clone finite machine. The natural-number triple is a fixed program parameter; its bounds and distinctness are needed only when identifying the output with the typed parity instance.

  1. def OAI.MaxCutGames.Explicit.MachineClone100Table.cloneEquationWords line 18
  2. inductive OAI.MaxCutGames.Explicit.MachineClone100Model.Tape line 33
  3. abbrev OAI.MaxCutGames.Explicit.MachineClone100Model.Context line 37
  4. abbrev OAI.MaxCutGames.Explicit.MachineClone100Model.State line 38
  5. abbrev OAI.MaxCutGames.Explicit.MachineClone100Model.Alphabet line 39
  6. inductive OAI.MaxCutGames.Explicit.MachineClone100Model.Label line 41
  7. def OAI.MaxCutGames.Explicit.MachineClone100Model.defaultControl line 57
  8. def OAI.MaxCutGames.Explicit.MachineClone100Model.initialState line 58
  9. def OAI.MaxCutGames.Explicit.MachineClone100Model.headerTape line 60
  10. def OAI.MaxCutGames.Explicit.MachineClone100Model.contextSource line 62
  11. def OAI.MaxCutGames.Explicit.MachineClone100Model.contextScale line 66
  12. def OAI.MaxCutGames.Explicit.MachineClone100Model.tripleField line 70
  13. def OAI.MaxCutGames.Explicit.MachineClone100Model.contextOffset line 77
  14. def OAI.MaxCutGames.Explicit.MachineClone100Model.affineEmit line 81
  15. def OAI.MaxCutGames.Explicit.MachineClone100Model.emission line 85
  16. def OAI.MaxCutGames.Explicit.MachineClone100Model.contextNext line 88
  17. def OAI.MaxCutGames.Explicit.MachineClone100Model.cleanupNext line 95
  18. def OAI.MaxCutGames.Explicit.MachineClone100Model.drain line 98
  19. def OAI.MaxCutGames.Explicit.MachineClone100Model.program line 105
  20. def OAI.MaxCutGames.Explicit.MachineClone100Model.machine line 128
  21. theorem OAI.MaxCutGames.Explicit.MachineClone100Context.contextSource_ne_scratch line 149
  22. theorem OAI.MaxCutGames.Explicit.MachineClone100Context.contextSource_ne_reversed line 157
  23. def OAI.MaxCutGames.Explicit.MachineClone100Context.contextTapes line 165
  24. theorem OAI.MaxCutGames.Explicit.MachineClone100Context.contextTapes_reversed line 171
  25. theorem OAI.MaxCutGames.Explicit.MachineClone100Context.contextTapes_other line 178
  26. theorem OAI.MaxCutGames.Explicit.MachineClone100Context.contextTapes_source line 184
  27. theorem OAI.MaxCutGames.Explicit.MachineClone100Context.contextTapes_scratch line 189
  28. theorem OAI.MaxCutGames.Explicit.MachineClone100Context.setupStep line 195

    Source documentation

    Setup discards arbitrary old control and register values before scanning.

    theorem setupStep (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
    (context : Context triples.length) (base : Tape → List Bool)
    (state : State triples.length) :
    TM2.step (program triples nonempty) ⟨some (.setup context), state, base⟩ =
      some ⟨some (.scan context), (((), context), none), base⟩ := rfl
  29. theorem OAI.MaxCutGames.Explicit.MachineClone100Context.contextTrace line 201
  30. def OAI.MaxCutGames.Explicit.MachineClone100Context.contextInTime line 225

    Source documentation

    The exact trace packaged for composition with neighboring cloning stages.

    def contextInTime (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
    (context : Context triples.length) (base : Tape → List Bool)
    (scratchEmpty : base .scratch = []) (state : State triples.length) :
    StateTransition.EvalsToInTime (TM2.step (program triples nonempty))
      ⟨some (.setup context), state, base⟩
      (some ⟨contextNext context, initialState _, contextTapes triples context base⟩)
      (3 * (base (contextSource context)).length + 3) where
…

    Mentions: OAI.MaxCutGames.Explicit.MachineClone100Context.contextTapes

  31. theorem OAI.MaxCutGames.Explicit.MachineClone100Context.contextInTime_steps line 236
  32. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_eq_flatMap line 252

    Source documentation

    Identity control transitions reduce exactly to fixed symbol substitution.

    theorem output_eq_flatMap {Q : Type} [Fintype Q]
    (emit : Q → Bool → List Bool) (q : Q) (input : List Bool) :
    MachineTransducer.output (fun state _ => state) emit q input =
      input.flatMap (emit q) := by
…
  33. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_append line 261
  34. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.affineEmit_replicate_true line 268
  35. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.affineEmit_word line 276

    Source documentation

    This includes zero scale and zero offset, with no positivity assumptions.

    theorem affineEmit_word (scale offset v : Nat) :
    (encodeWord v).flatMap (affineEmit scale offset) =
      encodeWord (offset + scale * v) := by
…
  36. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.affineEmit_word_append line 283
  37. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.affineEmit_words line 288
  38. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_word line 297

    Source documentation

    Exact symbolic context transform used by the shared clone-table machine.

    theorem output_word (triples : List (Nat × Nat × Nat))
    (c : Context triples.length) (v : Nat) :
    MachineTransducer.output (fun q _ => q) (emission triples) c (encodeWord v) =
      encodeWord (contextOffset triples c + contextScale c * v) := by
…
  39. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_word_append line 304
  40. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_words line 311
  41. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_header_variables line 318
  42. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_header_count line 324

    Source documentation

    The equation-count multiplier remains the arbitrary symbolic table length.

    theorem output_header_count (triples : List (Nat × Nat × Nat)) (v : Nat) :
    MachineTransducer.output (fun q _ => q) (emission triples) (.inl 1) (encodeWord v) =
      encodeWord (triples.length * v) := by
…
  43. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_field line 329
  44. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_first_field line 335
  45. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_second_field line 341
  46. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_third_field line 347
  47. theorem OAI.MaxCutGames.Explicit.MachineClone100Affine.output_rhs_field line 354

    Source documentation

    RHS words are copied exactly, including both legal Boolean values.

    theorem output_rhs_field (triples : List (Nat × Nat × Nat))
    (i : Fin triples.length) (v : Nat) :
    MachineTransducer.output (fun q _ => q) (emission triples) (.inr (i, 3)) (encodeWord v) =
      encodeWord v := by
…
  48. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.drainStep_cons line 373

    Source documentation

    The finite drain statement pops one symbol and retains the ambient control.

    theorem drainStep_cons (tape : Tape) (again next : Label D)
    (program : Label D → TM2.Stmt Alphabet (Label D) (State D))
    (atAgain : program again = drain tape again next)
    (base : Tape → List Bool) (bit : Bool) (input : List Bool)
    (control : Unit × Context D) (register : Option Bool) :
    TM2.step program
      ⟨some again, (control, register), Function.update base tape (bit :: input)⟩ =
      some ⟨some again, (control, some bit), Function.update base tape input⟩ := by
…
  49. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.drainStep_nil line 387

    Source documentation

    The exit transition observes the empty tape and resets the optional bit.

    theorem drainStep_nil (tape : Tape) (again next : Label D)
    (program : Label D → TM2.Stmt Alphabet (Label D) (State D))
    (atAgain : program again = drain tape again next)
    (base : Tape → List Bool) (control : Unit × Context D) (register : Option Bool) :
    TM2.step program
      ⟨some again, (control, register), Function.update base tape []⟩ =
      some ⟨some next, (control, none), Function.update base tape []⟩ := by
…
  50. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.drainTrace line 401

    Source documentation

    Direct list induction gives exactly one transition per symbol plus the empty-tape exit; no whole execution trace is assumed.

    theorem drainTrace (tape : Tape) (again next : Label D)
    (program : Label D → TM2.Stmt Alphabet (Label D) (State D))
    (atAgain : program again = drain tape again next)
    (base : Tape → List Bool) (input : List Bool)
    (control : Unit × Context D) (register : Option Bool) :
    (MachineComposition.advance (TM2.step program))^[input.length + 1]
      (some ⟨some again, (control, register), Function.update base tape input⟩) =
      some ⟨some next, (control, none), Function.update base tape []⟩ := by
…
  51. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.drainTrace_base line 422

    Source documentation

    Caller form: the selected tape's initial contents are read from the frame.

    theorem drainTrace_base (tape : Tape) (again next : Label D)
    (program : Label D → TM2.Stmt Alphabet (Label D) (State D))
    (atAgain : program again = drain tape again next)
    (base : Tape → List Bool) (control : Unit × Context D) (register : Option Bool) :
    (MachineComposition.advance (TM2.step program))^[(base tape).length + 1]
      (some ⟨some again, (control, register), base⟩) =
      some ⟨some next, (control, none), Function.update base tape []⟩ := by
…
  52. def OAI.MaxCutGames.Explicit.MachineClone100Cleanup.drainInTime line 432
  53. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearHeaderTrace line 446
  54. def OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearHeaderInTime line 454
  55. def OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields line 464

    Source documentation

    The four explicit updates made by the successive cleanup labels.

    def clearFields (base : Tape → List Bool) : Tape → List Bool :=
…
  56. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields_field line 468
  57. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields_other line 472
  58. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields_input line 476
  59. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields_header line 478
  60. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields_counter line 480
  61. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields_scratch line 482
  62. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields_reversed line 484
  63. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields_output line 486
  64. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields_eq_self line 489
  65. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields_idempotent line 494
  66. def OAI.MaxCutGames.Explicit.MachineClone100Cleanup.cleanupSteps line 498
  67. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.cleanupTrace line 502
  68. theorem OAI.MaxCutGames.Explicit.MachineClone100Cleanup.cleanupFourTrace line 513

    Source documentation

    All four field stacks are consumed by the actual cleanup program.

    theorem cleanupFourTrace (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
    (base : Tape → List Bool) (control : Unit × Context triples.length)
    (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program triples nonempty)))^[cleanupSteps base]
      (some ⟨some (.cleanup 0), (control, register), base⟩) =
      some ⟨some .guard, (control, none), clearFields base⟩ := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineClone100Cleanup.cleanupSteps, OAI.MaxCutGames.Explicit.MachineClone100Cleanup.clearFields

  69. def OAI.MaxCutGames.Explicit.MachineClone100Cleanup.cleanupFourInTime line 552
  70. def OAI.MaxCutGames.Explicit.MachineClone100Headers.parsedTapes line 576
  71. def OAI.MaxCutGames.Explicit.MachineClone100Headers.resultTapes line 585

    Source documentation

    Exact header-stage endpoint. The occurrence counter is retained for the body loop; generated output is accumulated in reverse.

    def resultTapes (triples : List (Nat × Nat × Nat)) (base : Tape → List Bool)
    (n m : Nat) (suffix : List Bool) : Tape → List Bool
  | .input => suffix
  | .header => []
  | .counter => encodeWord m
  | .reversed => (encodeWords [100 * n, triples.length * m]).reverse
  | tape => base tape
  72. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.resultTapes_input line 593
  73. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.resultTapes_header line 595
  74. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.resultTapes_counter line 597
  75. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.resultTapes_reversed line 599
  76. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.resultTapes_scratch line 602
  77. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.resultTapes_field line 604
  78. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.resultTapes_output line 606
  79. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.twoFieldsTapes_inline_MachineClone100Headers line 609
  80. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.firstContextTapes_inline_MachineClone100Headers line 618
  81. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.secondContextTapes_inline_MachineClone100Headers line 626
  82. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.clearHeaderTapes_inline_MachineClone100Headers line 636
  83. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.headersTrace line 645
  84. def OAI.MaxCutGames.Explicit.MachineClone100Headers.headersInTime line 721

    Source documentation

    The exact header trace packaged in the machine execution-time interface.

    def headersInTime (triples : List (Nat × Nat × Nat)) (hne : triples ≠ [])
    (base : Tape → List Bool) (n m : Nat) (suffix : List Bool)
    (hinput : base .input = encodeWords [n, m] ++ suffix)
    (hheader : base .header = []) (hcounter : base .counter = [])
    (hscratch : base .scratch = []) (hreversed : base .reversed = []) :
    StateTransition.EvalsToInTime (TM2.step (program triples hne))
      ⟨some (.headerStart 0), initialState triples.length, base⟩
      (some ⟨some .guard, initialState triples.length,
        resultTapes triples base n m suffix⟩) (5 * n + 4 * m + 18) where
…

    Mentions: OAI.MaxCutGames.Explicit.MachineClone100Headers.resultTapes

  85. theorem OAI.MaxCutGames.Explicit.MachineClone100Headers.headersTime_linear line 734