OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumBufferedSharedEdge.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Different routes do not share lattice edges, including at buffered endpoint cells.

  1. theorem OAI.ContinuumCoulomb.qmaSquareGrid_not_eightfold line 12
  2. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.spaced_incident_support line 23
  3. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.arm_lane_not_grid line 35
  4. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.spaced_unit_direction line 44
  5. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.endpointArm_lane_no_edge line 65
  6. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.bufferedPath_edge_piece line 105
  7. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.bufferedPath_no_shared_edge line 123
  8. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.bufferedPath_edge_disjoint line 141