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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The full orbit clauses for the planar processor: every simulated step, the common corridor, nonhalting safety, and an integer-time halting margin.

  1. def OAI.ForcedComputation.Recorder.Planar.normalizedPoint line 13
  2. def OAI.ForcedComputation.Recorder.Planar.normalizedInitial line 18
  3. theorem OAI.ForcedComputation.Recorder.Planar.normalizedPoint_initial line 21
  4. theorem OAI.ForcedComputation.Recorder.Planar.normalized_steps_realized line 25
  5. theorem OAI.ForcedComputation.Recorder.Planar.normalized_step_corridor line 34
  6. theorem OAI.ForcedComputation.Recorder.Planar.normalized_step_safe line 46
  7. theorem OAI.ForcedComputation.Recorder.Planar.finite_work_nonhalting line 60
  8. theorem OAI.ForcedComputation.Recorder.Planar.normalized_nonhalting_corridor line 73
  9. theorem OAI.ForcedComputation.Recorder.Planar.normalized_halting_clearance line 108