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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Three explicit smooth transition clocks leave collars between the vertical, horizontal, and final vertical motions of each address gate.

  1. def OAI.ForcedComputation.ExpandingDetector.firstWeight line 14
  2. def OAI.ForcedComputation.ExpandingDetector.secondWeight line 15
  3. def OAI.ForcedComputation.ExpandingDetector.thirdWeight line 16
  4. theorem OAI.ForcedComputation.ExpandingDetector.weights_smooth line 18
  5. theorem OAI.ForcedComputation.ExpandingDetector.weights_slots line 23
  6. theorem OAI.ForcedComputation.ExpandingDetector.thirdWeight_le_firstWeight line 41
  7. def OAI.ForcedComputation.ExpandingDetector.scheduledCenter line 51
  8. theorem OAI.ForcedComputation.ExpandingDetector.scheduledCenter_smooth line 55
  9. theorem OAI.ForcedComputation.ExpandingDetector.scheduledCenter_initial line 69
  10. theorem OAI.ForcedComputation.ExpandingDetector.scheduledCenter_final line 77
  11. theorem OAI.ForcedComputation.ExpandingDetector.scheduledCenter_separated line 86
  12. theorem OAI.ForcedComputation.ExpandingDetector.scheduledCenter_nonterminal line 93