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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The same finite recorder operates on any rational horizontal sheet. Only the chart height changes; all planar instructions are retained.

  1. def OAI.ForcedComputation.Recorder.recorderInputAtHeight line 12
  2. theorem OAI.ForcedComputation.Recorder.recorderInputAtHeight_valid line 15
  3. theorem OAI.ForcedComputation.Recorder.recorderInputAtHeight_height line 19
  4. theorem OAI.ForcedComputation.Recorder.recorderInputAtHeight_period line 25
  5. theorem OAI.ForcedComputation.Recorder.recorderInputAtHeight_halfWidth line 29
  6. theorem OAI.ForcedComputation.Recorder.Step.flow_oneAtHeight line 35
  7. theorem OAI.ForcedComputation.Recorder.Steps.flow_natAtHeight line 69
  8. theorem OAI.ForcedComputation.Recorder.Step.flow_safeAtHeight line 83
  9. theorem OAI.ForcedComputation.Recorder.recorder_flow_halting_iff_atHeight line 117