OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRetainedGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual retained interactions are source rays, noncrossing cell pairs, or external corridors. All endpoint positions incorporate the inward move.

  1. def OAI.ContinuumCoulomb.qmaMovedPort line 14
  2. def OAI.ContinuumCoulomb.QMAPortRouteData.RetainedGeometry line 21
  3. theorem OAI.ContinuumCoulomb.QMAPortRouteData.retained_geometry line 32