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

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

The seven-row reversible recording table in Section 2 of Finite Instructions and Solenoidal Shear Flows (2026), Lemma lem:recorder.

The inverse below is valid on the entire guarded domain, including tapes that do not satisfy the checkpoint invariant. The record is the pair consisting of the original state and the symbol read, as in Bennett, Logical reversibility of computation (1973), equations (9)--(11); the concrete seven-row construction and its proof are supplied here rather than assumed from that reference.

  1. structure OAI.ForcedComputation.Recorder.Machine line 20
  2. abbrev OAI.ForcedComputation.Recorder.Record line 27
  3. inductive OAI.ForcedComputation.Recorder.History line 29
  4. inductive OAI.ForcedComputation.Recorder.Control line 35
  5. abbrev OAI.ForcedComputation.Recorder.Symbol line 43
  6. inductive OAI.ForcedComputation.Recorder.LocalStep line 48

    Source documentation

    Exactly the seven rows of the manuscript's guarded local table.

    inductive LocalStep (M : Machine Q A) :
    Control Q A → Symbol Q A → Control Q A → Symbol Q A → ℤ → Prop
  | work (q : Q) (a : A) (l : History Q A)
      (hq : M.halting q = false) (hl : l ≠ frontier) :
      LocalStep M (checkpoint q) (a, l, false)
        (mark (q, a)) (M.write q a, l, false) (M.move q a)
  | setMark (r : Record Q A) (c : A) (l : History Q A) (hl : l ≠ frontier) :
      LocalStep M (mark r) (c, l, false) (scanRight r) (c, l, true) 1
  | right (r : Record Q A) (c : A) (l : History Q A) (hl : l ≠ frontier) :
      LocalStep M (scanRight r) (c, l, false) (scanRight r) (c, l, false) 1
  | record (r : Record Q A) (c : A) :
      LocalStep M (scanRight r) (c, frontier, false)
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Recorder.Control, OAI.ForcedComputation.Recorder.Symbol, OAI.ForcedComputation.Recorder.History, OAI.ForcedComputation.Recorder.Record

  7. def OAI.ForcedComputation.Recorder.incoming line 69
  8. theorem OAI.ForcedComputation.Recorder.LocalStep.incoming_eq line 76
  9. def OAI.ForcedComputation.Recorder.undoLocal line 83

    Source documentation

    Reconstruct the preceding control and read symbol from the new control and the complete symbol that was written. No checkpoint invariant is consulted.

    def undoLocal : Control Q A → Symbol Q A → Option (Control Q A × Symbol Q A)
  | checkpoint q, (c, l, _) => some (scanLeft q, (c, l, true))
  | mark r, (_, l, _) => some (checkpoint r.1, (r.2, l, false))
  | scanRight r, (c, l, true) => some (mark r, (c, l, false))
  | scanRight r, (c, l, false) => some (scanRight r, (c, l, false))
  | advance _, (c, History.record r, _) => some (scanRight r, (c, frontier, false))
  | advance _, _ => none
  | scanLeft q, (c, History.frontier, _) => some (advance q, (c, empty, false))
  | scanLeft q, (c, l, _) => some (scanLeft q, (c, l, false))

    Mentions: OAI.ForcedComputation.Recorder.Control, OAI.ForcedComputation.Recorder.Symbol

  10. theorem OAI.ForcedComputation.Recorder.LocalStep.undo line 93
  11. theorem OAI.ForcedComputation.Recorder.LocalStep.predecessor_unique line 105
  12. def OAI.ForcedComputation.Recorder.evalLocal line 114

    Source documentation

    A terminating local interpreter for the finite table.

    def evalLocal [DecidableEq Q] [DecidableEq A] (M : Machine Q A)
    (q : Control Q A) (s : Symbol Q A) : Option (Control Q A × Symbol Q A × ℤ) :=
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Recorder.Control, OAI.ForcedComputation.Recorder.Symbol

  13. theorem OAI.ForcedComputation.Recorder.LocalStep.eval line 133
  14. theorem OAI.ForcedComputation.Recorder.LocalStep.successor_unique line 138
  15. structure OAI.ForcedComputation.Recorder.Configuration line 145
  16. def OAI.ForcedComputation.Recorder.Step line 150
  17. def OAI.ForcedComputation.Recorder.undo line 154
  18. theorem OAI.ForcedComputation.Recorder.Step.undo line 160

    Source documentation

    The entire predecessor tape, head, and control are recovered.

    theorem Step.undo {M : Machine Q A} {C D : Configuration Q A} (h : Step M C D) :
    undo M D = some C := by
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Recorder.Configuration, OAI.ForcedComputation.Recorder.Step

  19. theorem OAI.ForcedComputation.Recorder.Step.predecessor_unique line 179
  20. theorem OAI.ForcedComputation.Recorder.Step.scan_right line 183
  21. theorem OAI.ForcedComputation.Recorder.Step.scan_left line 192
  22. inductive OAI.ForcedComputation.Recorder.Steps line 203

    Source documentation

    Execution with an exact finite number of local transitions.

    inductive Steps (M : Machine Q A) : ℕ → Configuration Q A → Configuration Q A → Prop
  | zero (C) : Steps M 0 C C
  | next {n C D E} : Steps M n C D → Step M D E → Steps M (n + 1) C E

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Recorder.Configuration, OAI.ForcedComputation.Recorder.Step

  23. theorem OAI.ForcedComputation.Recorder.Steps.trans line 207
  24. theorem OAI.ForcedComputation.Recorder.scan_right_steps line 213
  25. theorem OAI.ForcedComputation.Recorder.scan_left_steps line 226
  26. def OAI.ForcedComputation.Recorder.tracks line 239
  27. theorem OAI.ForcedComputation.Recorder.tracks_update_work line 242
  28. theorem OAI.ForcedComputation.Recorder.tracks_update_history line 249
  29. theorem OAI.ForcedComputation.Recorder.tracks_update_mark line 256
  30. theorem OAI.ForcedComputation.Recorder.checkpoint_cycle line 266

    Source documentation

    A complete recorder cycle. There are k right-scan steps and k + 1 left-scan steps, in addition to the five non-scan transitions. The hypotheses describe the actual work/history tracks, not a pre-assumed simulation.

    theorem checkpoint_cycle (M : Machine Q A) (q : Q) (w : ℤ → A)
    (history : ℤ → History Q A) (head : ℤ) (k : ℕ)
    (hq : M.halting q = false)
    (hhead : history head ≠ frontier)
    (hbefore : ∀ j < head + M.move q (w head) + (k : ℤ) + 1,
      history j ≠ frontier)
    (hfront : history (head + M.move q (w head) + (k : ℤ) + 1) = frontier)
    (hempty : history (head + M.move q (w head) + (k : ℤ) + 1 + 1) = empty) :
    let r : Record Q A := (q, w head)
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Recorder.History, OAI.ForcedComputation.Recorder.Record