OAI/Computability/UniqueGames/Machines/MachineClone100TableLemmas.lean

GitHub source file

78 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.UniqueGamesTheorem.Explicit.MachineClone100Table.cloneEquationWords line 22
  2. inductive OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.Tape line 41
  3. abbrev OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.Context line 45
  4. abbrev OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.State line 46
  5. abbrev OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.Alphabet line 47
  6. inductive OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.Label line 49
  7. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.defaultControl line 65
  8. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.initialState line 66
  9. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.headerTape line 68
  10. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.contextSource line 70
  11. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.contextScale line 74
  12. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.tripleField line 78
  13. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.contextOffset line 85
  14. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.affineEmit line 89
  15. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.emission line 93
  16. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.contextNext line 96
  17. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.cleanupNext line 103
  18. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.drain line 106
  19. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.program line 113
  20. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Model.machine line 136
  21. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_eq_flatMap line 161

    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
…
  22. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_append line 170
  23. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.affineEmit_replicate_true line 177
  24. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.affineEmit_word line 185

    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
…
  25. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.affineEmit_word_append line 192
  26. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.affineEmit_words line 197
  27. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_word line 206

    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
…
  28. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_word_append line 213
  29. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_words line 220
  30. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_header_variables line 227
  31. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_header_count line 233

    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
…
  32. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_field line 238
  33. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_first_field line 244
  34. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_second_field line 250
  35. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_third_field line 256
  36. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Affine.output_rhs_field line 263

    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
…
  37. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.drainStep_cons line 286

    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
…
  38. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.drainStep_nil line 300

    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
…
  39. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.drainTrace line 314

    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
…
  40. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.drainTrace_base line 335

    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
…
  41. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.drainInTime line 345
  42. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearHeaderTrace line 359
  43. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearHeaderInTime line 367
  44. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields line 377

    Source documentation

    The four explicit updates made by the successive cleanup labels.

    def clearFields (base : Tape → List Bool) : Tape → List Bool :=
…
  45. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields_field line 381
  46. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields_other line 385
  47. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields_input line 389
  48. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields_header line 391
  49. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields_counter line 393
  50. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields_scratch line 395
  51. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields_reversed line 397
  52. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields_output line 399
  53. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields_eq_self line 402
  54. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields_idempotent line 407
  55. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.cleanupSteps line 411
  56. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.cleanupTrace line 415
  57. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.cleanupFourTrace line 426

    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.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.cleanupSteps, OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.clearFields

  58. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Cleanup.cleanupFourInTime line 465
  59. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.contextSource_ne_scratch line 492
  60. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.contextSource_ne_reversed line 500
  61. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.contextTapes line 508
  62. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.contextTapes_reversed line 514
  63. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.contextTapes_other line 521
  64. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.contextTapes_source line 527
  65. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.contextTapes_scratch line 532
  66. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.setupStep line 538

    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
  67. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.contextTrace line 544
  68. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.contextInTime line 568

    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.UniqueGamesTheorem.Explicit.MachineClone100Context.contextTapes

  69. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Context.contextInTime_steps line 579
  70. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Finish.finishTapes line 599
  71. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Finish.finishTapes_counter line 603
  72. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Finish.finishTapes_reversed line 606
  73. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Finish.finishTapes_output line 609
  74. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Finish.finishTapes_other line 613
  75. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Finish.counterStep line 618
  76. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Finish.finishTrace line 625
  77. def OAI.UniqueGamesTheorem.Explicit.MachineClone100Finish.finishInTime line 649
  78. theorem OAI.UniqueGamesTheorem.Explicit.MachineClone100Finish.finish_eq_haltList line 658