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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The planar processor's full nonhalting corridor supplies the detector's torus clearance, including across the boundary of a fundamental square.

  1. theorem OAI.ForcedComputation.VelocityDetector.vertical_corridor_torus_separation line 13
  2. theorem OAI.ForcedComputation.VelocityDetector.processor_nonhalting_clearance line 36