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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

All-time observation of the actual planar processor. Nonhalting excludes the entire continuous trajectory, while a halt is witnessed at an integer.

  1. theorem OAI.ForcedComputation.Recorder.Planar.shifted_planar_observation line 13
  2. theorem OAI.ForcedComputation.Recorder.Planar.normalized_planar_observation line 78