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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The geometric branch implementing a machine step retains its source and target control states. These identities supply the all-time observer guard.

  1. theorem OAI.ForcedComputation.Recorder.Planar.step_branch line 12