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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact machine steps and all-time nonhalting exclusion for the actual normalized autonomous suspension. All geometric obligations are proved from the finite compiler; no routing hypothesis remains in these statements.

  1. theorem OAI.ForcedComputation.Recorder.Planar.normalized_suspension_step line 16
  2. theorem OAI.ForcedComputation.Recorder.Planar.normalized_suspension_step_safe line 30
  3. theorem OAI.ForcedComputation.Recorder.Planar.stationary_suspension_observation line 45