OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/DetectorPositive.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Each smooth stirring clock visits every phase of its finite prefix. The characteristic carrying the bump center then gives a velocity above the fixed detection threshold.

  1. theorem OAI.ForcedComputation.VelocityDetector.detectorPhase_hits line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.detectorBurst_detects line 24