OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/BalancedCycle.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite sweeps in the balanced recorder. The preparatory cycle restores both work tapes and moves exactly one blank onto the history stack.

  1. abbrev OAI.ForcedComputation.Balanced.push line 13
  2. abbrev OAI.ForcedComputation.Balanced.word line 14
  3. def OAI.ForcedComputation.Balanced.triple line 16
  4. theorem OAI.ForcedComputation.Balanced.prefixConfiguration_three line 19
  5. inductive OAI.ForcedComputation.Balanced.Steps line 28
  6. theorem OAI.ForcedComputation.Balanced.Step.steps line 33
  7. theorem OAI.ForcedComputation.Balanced.Steps.trans line 37
  8. theorem OAI.ForcedComputation.Balanced.enter_step line 45
  9. theorem OAI.ForcedComputation.Balanced.outward_step line 53
  10. theorem OAI.ForcedComputation.Balanced.supply_step line 61
  11. theorem OAI.ForcedComputation.Balanced.inward_step line 69
  12. theorem OAI.ForcedComputation.Balanced.restore_step line 77
  13. theorem OAI.ForcedComputation.Balanced.word_append line 85
  14. abbrev OAI.ForcedComputation.Balanced.workWord line 91
  15. theorem OAI.ForcedComputation.Balanced.outward_sweep line 93
  16. theorem OAI.ForcedComputation.Balanced.inward_sweep line 105
  17. theorem OAI.ForcedComputation.Balanced.preparation line 119

    Source documentation

    On arbitrary independent tails, preparation removes one right-tail blank and adds that same blank to history, leaving the finite work window unchanged.

    theorem preparation (M : Recorder.Machine Q A) (blank : A) (q : Q) (a : A)
    (hq : M.halting q = false) (w : List A) (l r h : Stack Q A) :
    Steps M blank (2 * w.length + 3)
      (triple (.checkpoint q) l
        (push (work a) (word (workWord w) (push .boundary (push (work blank) r)))) h)
      (triple (.dispatch q) l
        (push (work a) (word (workWord w) (push .boundary r))) (push (work blank) h)) := by
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Balanced.Stack, OAI.ForcedComputation.Balanced.Steps, OAI.ForcedComputation.Balanced.triple, OAI.ForcedComputation.Balanced.push, OAI.ForcedComputation.Balanced.word, OAI.ForcedComputation.Balanced.workWord

  18. theorem OAI.ForcedComputation.Balanced.stay_step line 140
  19. theorem OAI.ForcedComputation.Balanced.left_step line 149
  20. theorem OAI.ForcedComputation.Balanced.right_step line 159
  21. theorem OAI.ForcedComputation.Balanced.boundary_step line 169
  22. theorem OAI.ForcedComputation.Balanced.stay_cycle line 179
  23. theorem OAI.ForcedComputation.Balanced.left_cycle line 191
  24. theorem OAI.ForcedComputation.Balanced.right_cycle line 203
  25. theorem OAI.ForcedComputation.Balanced.boundary_cycle line 220

    Source documentation

    A right move at the boundary creates a new blank work cell while retaining one boundary and the same infinite blank filler.

    theorem boundary_cycle (M : Recorder.Machine Q A) (blank : A) (q : Q) (a : A)
    (hq : M.halting q = false) (hm : M.move q a = 1) (l h : Stack Q A) :
    Steps M blank 4
      (triple (.checkpoint q) l
        (push (work a) (push .boundary (fun _ => work blank))) h)
      (triple (.checkpoint (M.next q a)) (push (work (M.write q a)) l)
        (push (work blank) (push .boundary (fun _ => work blank)))
        (push (record (.boundary q a)) h)) := by
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Balanced.Stack, OAI.ForcedComputation.Balanced.Steps, OAI.ForcedComputation.Balanced.triple, OAI.ForcedComputation.Balanced.push