OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOddPathGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The odd subdivision gadget splits a routed edge into two unit edges and its reversed remaining tail. The two fresh vertices are the first two route points.

  1. def OAI.ContinuumCoulomb.qmaOddSplitLength line 10
  2. def OAI.ContinuumCoulomb.qmaOddSplitIndex line 11
  3. theorem OAI.ContinuumCoulomb.qmaOddSplitIndex_bounds line 14
  4. theorem OAI.ContinuumCoulomb.qmaOddSplitIndex_zero line 18
  5. theorem OAI.ContinuumCoulomb.qmaOddSplitIndex_last line 23
  6. theorem OAI.ContinuumCoulomb.qmaOddSplitIndex_injective line 29
  7. theorem OAI.ContinuumCoulomb.qmaOddSplitIndex_interior line 34
  8. theorem OAI.ContinuumCoulomb.qmaOddSplitIndex_separated line 39
  9. theorem OAI.ContinuumCoulomb.qmaOddSplitIndex_step line 46
  10. theorem OAI.ContinuumCoulomb.qmaOddSplitPoint_step line 53