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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Iterating a spatial suspension: a completed processor period advances the vertical lift by one while implementing the next recorder step.

  1. def OAI.ForcedComputation.verticalInteger line 13
  2. theorem OAI.ForcedComputation.atHeight_add_verticalInteger line 15
  3. theorem OAI.ForcedComputation.suspension_one_at_integer line 20
  4. theorem OAI.ForcedComputation.suspension_recorder_steps line 32