OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarRecorder.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

A finite rational planar recorder program with the stationary-suspension paper's horizontal initial corridor and low vertical halting observer.

  1. def OAI.ForcedComputation.Recorder.Planar.compression line 17

    Source documentation

    Horizontal compression accounts for the number of parking columns.

    def compression (M : Alternating.Machine) (hM : M.WellFormed) : ℚ :=
…

    Mentions: OAI.Alternating.Machine

  2. theorem OAI.ForcedComputation.Recorder.Planar.compression_pos line 20
  3. theorem OAI.ForcedComputation.Recorder.Planar.compression_le line 23
  4. def OAI.ForcedComputation.Recorder.Planar.shift line 30
  5. def OAI.ForcedComputation.Recorder.Planar.coordinateMap line 33
  6. def OAI.ForcedComputation.Recorder.Planar.instruction line 36
  7. def OAI.ForcedComputation.Recorder.Planar.program line 41
  8. def OAI.ForcedComputation.Recorder.Planar.point line 44
  9. def OAI.ForcedComputation.Recorder.Planar.observer line 48
  10. def OAI.ForcedComputation.Recorder.Planar.initialPoint line 55

    Source documentation

    The input-dependent loading endpoint is a finite rational expression.

    def initialPoint (I : Alternating.MachineInput) (hI : Alternating.ValidInput I) : Fin 2 → ℚ :=
…

    Mentions: OAI.Alternating.MachineInput, OAI.Alternating.ValidInput

  11. theorem OAI.ForcedComputation.Recorder.Planar.initialPoint_spec line 60
  12. theorem OAI.ForcedComputation.Recorder.Planar.instruction_mem line 66
  13. theorem OAI.ForcedComputation.Recorder.Planar.instruction_source_positive line 71
  14. theorem OAI.ForcedComputation.Recorder.Planar.instruction_target_positive line 76
  15. theorem OAI.ForcedComputation.Recorder.Planar.instruction_factor_pos line 81
  16. theorem OAI.ForcedComputation.Recorder.Planar.instruction_image line 85
  17. theorem OAI.ForcedComputation.Recorder.Planar.instruction_source_separation line 92
  18. theorem OAI.ForcedComputation.Recorder.Planar.instruction_target_separation line 102
  19. theorem OAI.ForcedComputation.Recorder.Planar.instruction_halfWidths line 112
  20. theorem OAI.ForcedComputation.Recorder.Planar.coordinateMap_bounds line 134
  21. theorem OAI.ForcedComputation.Recorder.Planar.instruction_source_bounds line 143
  22. theorem OAI.ForcedComputation.Recorder.Planar.instruction_target_bounds line 152
  23. theorem OAI.ForcedComputation.Recorder.Planar.step_realized line 161
  24. theorem OAI.ForcedComputation.Recorder.Planar.point_second line 185
  25. theorem OAI.ForcedComputation.Recorder.Planar.point_observer_iff line 197
  26. theorem OAI.ForcedComputation.Recorder.Planar.run_observer_iff line 229