OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHalfCorridor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Each external corridor splits into two paths contained in their own cells, joined by one unit edge. These paths meet the internal templates only at ports.

  1. def OAI.ContinuumCoulomb.qmaHalfCorridorPath line 11
  2. def OAI.ContinuumCoulomb.qmaLocalPatchPath line 22
  3. def OAI.ContinuumCoulomb.qmaCellBoundary line 25
  4. def OAI.ContinuumCoulomb.qmaLocalPort line 27
  5. theorem OAI.ContinuumCoulomb.qmaHalfCorridor_endpoints line 30
  6. theorem OAI.ContinuumCoulomb.qmaHalfCorridor_length line 35
  7. theorem OAI.ContinuumCoulomb.qmaHalfCorridor_chain line 39
  8. theorem OAI.ContinuumCoulomb.qmaHalfCorridor_simple line 44
  9. theorem OAI.ContinuumCoulomb.qmaHalfCorridor_bounded line 48
  10. theorem OAI.ContinuumCoulomb.qmaHalfCorridor_disjoint line 52
  11. theorem OAI.ContinuumCoulomb.qmaHalfCorridor_pair line 56
  12. theorem OAI.ContinuumCoulomb.qmaHalfCorridor_ray line 60
  13. theorem OAI.ContinuumCoulomb.qmaHalfCorridor_patch line 64