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

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Iterating the seven-row recorder from its actual initialized tape.

  1. structure OAI.ForcedComputation.Recorder.WorkConfiguration line 13
  2. def OAI.ForcedComputation.Recorder.workNext line 18
  3. def OAI.ForcedComputation.Recorder.workAt line 23
  4. theorem OAI.ForcedComputation.Recorder.workAt_zero line 26
  5. theorem OAI.ForcedComputation.Recorder.workAt_succ line 29
  6. theorem OAI.ForcedComputation.Recorder.workAt_head_bounds line 33
  7. def OAI.ForcedComputation.Recorder.historyRun line 45

    Source documentation

    The history track retains every recorded instruction.

    def historyRun (g₀ : ℤ) (r : ℕ → Record Q A) : ℕ → ℤ → History Q A :=
…

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

  8. theorem OAI.ForcedComputation.Recorder.historyRun_frontier line 51
  9. theorem OAI.ForcedComputation.Recorder.historyRun_before line 57
  10. theorem OAI.ForcedComputation.Recorder.historyRun_after line 69
  11. def OAI.ForcedComputation.Recorder.workRecord line 79
  12. def OAI.ForcedComputation.Recorder.checkpointAt line 82
  13. theorem OAI.ForcedComputation.Recorder.checkpointAt_zero line 87
  14. theorem OAI.ForcedComputation.Recorder.checkpoint_successor line 92
  15. theorem OAI.ForcedComputation.Recorder.simulate_prefix line 125

    Source documentation

    Every finite nonhalting prefix of the original machine has a finite recorder execution reaching exactly its work configuration.

    theorem simulate_prefix (M : Machine Q A) (q : Q) (w : ℤ → A)
    (g₀ : ℤ) (hg₀ : 2 ≤ g₀) (n : ℕ)
    (hn : ∀ i < n, M.halting (workAt M q w i).state = false) :
    ∃ m : ℕ, Steps M m (checkpointAt M q w g₀ 0) (checkpointAt M q w g₀ n) := by
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Recorder.workAt, OAI.ForcedComputation.Recorder.Steps, OAI.ForcedComputation.Recorder.checkpointAt

  16. theorem OAI.ForcedComputation.Recorder.simulate_prefix_length line 136
  17. theorem OAI.ForcedComputation.Recorder.Step.successor_unique line 149
  18. theorem OAI.ForcedComputation.Recorder.Steps.head line 157
  19. theorem OAI.ForcedComputation.Recorder.Steps.prefix_has_successor line 172
  20. def OAI.ForcedComputation.Recorder.haltingControl line 194
  21. theorem OAI.ForcedComputation.Recorder.LocalStep.source_nonhalting line 198
  22. theorem OAI.ForcedComputation.Recorder.halted_no_step line 203
  23. theorem OAI.ForcedComputation.Recorder.halting_checkpoint_iff line 212

    Source documentation

    Starting with the actual finite-history initialization, a recorder reaches a halting checkpoint exactly when the original machine halts.

    theorem halting_checkpoint_iff [DecidableEq Q] [DecidableEq A]
    (M : Machine Q A) (q : Q) (w : ℤ → A) (g₀ : ℤ) (hg₀ : 2 ≤ g₀) :
    (∃ m C q', Steps M m (checkpointAt M q w g₀ 0) C ∧
      C.control = checkpoint q' ∧ M.halting q' = true) ↔
      ∃ n, M.halting (workAt M q w n).state = true := by
…

    Mentions: OAI.ForcedComputation.Recorder.Machine, OAI.ForcedComputation.Recorder.Steps, OAI.ForcedComputation.Recorder.checkpointAt, OAI.ForcedComputation.Recorder.workAt