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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The complete finite recorder graph drives one array of disjoint moving gates. No selected computation is used to choose the gates.

  1. abbrev OAI.ForcedComputation.ExpandingDetector.StageWire line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.StageWire.source_injective line 19
  3. theorem OAI.ForcedComputation.ExpandingDetector.StageWire.target_injective line 29
  4. def OAI.ForcedComputation.ExpandingDetector.wireCurve line 39
  5. theorem OAI.ForcedComputation.ExpandingDetector.wireCurve_smooth line 45
  6. theorem OAI.ForcedComputation.ExpandingDetector.wireCurve_separated line 51
  7. def OAI.ForcedComputation.ExpandingDetector.recorderStageField line 64
  8. theorem OAI.ForcedComputation.ExpandingDetector.recorderStageField_smooth line 69
  9. theorem OAI.ForcedComputation.ExpandingDetector.recorderStageField_tracks line 74