OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCellPathTemplates.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The six possible ordinary-cell connections and four source rays. The two opposite pairs are the only disjoint-port pair whose paths cross.

  1. def OAI.ContinuumCoulomb.qmaCellPairLeft line 11
  2. def OAI.ContinuumCoulomb.qmaCellPairRight line 12
  3. def OAI.ContinuumCoulomb.qmaCellPairPath line 13
  4. def OAI.ContinuumCoulomb.qmaCellRayPath line 21
  5. def OAI.ContinuumCoulomb.qmaCellPort line 27
  6. theorem OAI.ContinuumCoulomb.qmaCellPair_distinct line 29
  7. theorem OAI.ContinuumCoulomb.qmaCellPair_complete line 32
  8. theorem OAI.ContinuumCoulomb.qmaCellPair_endpoints line 37
  9. theorem OAI.ContinuumCoulomb.qmaCellPair_length line 42
  10. theorem OAI.ContinuumCoulomb.qmaCellPair_chain line 45
  11. theorem OAI.ContinuumCoulomb.qmaCellPair_simple line 49
  12. theorem OAI.ContinuumCoulomb.qmaCellPair_bounded line 52
  13. theorem OAI.ContinuumCoulomb.qmaCellPair_ports line 56
  14. theorem OAI.ContinuumCoulomb.qmaCellPair_disjoint line 61
  15. theorem OAI.ContinuumCoulomb.qmaCellRay_endpoints line 73
  16. theorem OAI.ContinuumCoulomb.qmaCellRay_length line 78
  17. theorem OAI.ContinuumCoulomb.qmaCellRay_chain line 81
  18. theorem OAI.ContinuumCoulomb.qmaCellRay_simple line 85
  19. theorem OAI.ContinuumCoulomb.qmaCellRay_disjoint line 88
  20. theorem OAI.ContinuumCoulomb.qmaCellRay_bounded line 92