OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumExchangeLanes.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Separated lanes for the actual spatial exchange family.

  1. def OAI.ContinuumCoulomb.qmaGridColorEquiv line 12
  2. theorem OAI.ContinuumCoulomb.qmaFineGridNat_injective line 16
  3. theorem OAI.ContinuumCoulomb.qmaFineRouteSites_nat line 23
  4. theorem OAI.ContinuumCoulomb.qmaLane_length line 36
  5. def OAI.ContinuumCoulomb.QMASpatialExchangeModel.laneColor line 43
  6. def OAI.ContinuumCoulomb.QMASpatialExchangeModel.laneSupport line 44
  7. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.lane_length line 47
  8. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.lane_color_disjoint line 53
  9. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.lane_intersection_colors line 74
  10. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.lane_intersection_not_vertex line 78