OAI/Geometry/RecorderBoxes/Placement.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Separated state-square placement of recorder controls.

  1. def OAI.Solenoidal.Bridge.terminalControl line 11
  2. abbrev OAI.Solenoidal.Bridge.controlCount line 15
  3. def OAI.Solenoidal.Bridge.controlIndex line 19
  4. theorem OAI.Solenoidal.Bridge.controlCount_pos line 22
  5. def OAI.Solenoidal.Bridge.kappa line 25
  6. theorem OAI.Solenoidal.Bridge.kappa_pos line 27
  7. theorem OAI.Solenoidal.Bridge.kappa_le line 30
  8. def OAI.Solenoidal.Bridge.origin line 35
  9. theorem OAI.Solenoidal.Bridge.state_extent line 40
  10. theorem OAI.Solenoidal.Bridge.state_gap line 60
  11. def OAI.Solenoidal.Bridge.place line 97
  12. def OAI.Solenoidal.Bridge.unplace line 100
  13. theorem OAI.Solenoidal.Bridge.unplace_place line 103
  14. theorem OAI.Solenoidal.Bridge.place_unplace line 107
  15. def OAI.Solenoidal.Bridge.physicalBox line 111
  16. theorem OAI.Solenoidal.Bridge.physicalBox_carrier line 115
  17. theorem OAI.Solenoidal.Bridge.physical_gap_same line 142
  18. theorem OAI.Solenoidal.Bridge.physical_gap_different line 152