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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The three motions of the expanding address array are separated by source columns, private rows, then target columns. Nonterminal transport stays below the observation half-plane throughout every motion.

  1. def OAI.ForcedComputation.ExpandingDetector.gateCenter line 13
  2. theorem OAI.ForcedComputation.ExpandingDetector.natural_spacing line 19
  3. theorem OAI.ForcedComputation.ExpandingDetector.gateCenter_initial line 29
  4. theorem OAI.ForcedComputation.ExpandingDetector.gateCenter_final line 33
  5. theorem OAI.ForcedComputation.ExpandingDetector.gateCenter_separated line 38
  6. theorem OAI.ForcedComputation.ExpandingDetector.nonterminal_gate_below line 67