OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEvenRoutePlacement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The even gadget places its interacting vertex at route point one and its second singlet spin at the reserved leaf. The remaining routes have odd length.

  1. def OAI.ContinuumCoulomb.QMAEvenRouteData.nextPoint line 15
  2. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.nextPoint_first line 22
  3. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.nextPoint_last line 38
  4. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.nextPoint_simple line 57
  5. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.nextPoint_step line 83
  6. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.nextPoint_avoids line 102
  7. theorem OAI.ContinuumCoulomb.QMAEvenRouteData.nextPoint_disjoint line 133
  8. def OAI.ContinuumCoulomb.QMAEvenRouteData.embedding line 177