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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Continuous-time observation of the genuine recorder orbit. Safe steps remain inside the nonterminal strip throughout all seven shear stages.

  1. theorem OAI.ForcedComputation.Recorder.codedPoint_first line 14
  2. theorem OAI.ForcedComputation.Recorder.codedPoint_observation_iff line 25
  3. theorem OAI.ForcedComputation.Recorder.Step.flow_safe line 57
  4. theorem OAI.ForcedComputation.Recorder.recorder_flow_halting_iff line 91