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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The scalar threshold for the compiled planar processor is exactly halting, using integer-phase entry and all-phase nonhalting clearance.

  1. theorem OAI.ForcedComputation.VelocityDetector.detector_processor_observation line 17