OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkInitial.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Odd subdivision gives every original incidence its own private fork port.

  1. def OAI.ContinuumCoulomb.qmaOriginalEndpoint line 12
  2. def OAI.ContinuumCoulomb.qmaOriginalPortCount line 15
  3. def OAI.ContinuumCoulomb.qmaOriginalPortEquiv line 18
  4. theorem OAI.ContinuumCoulomb.qmaOriginalPortCount_eq_degree line 24
  5. def OAI.ContinuumCoulomb.qmaSubdivisionPorts line 38
  6. def OAI.ContinuumCoulomb.qmaSubdivisionLeft line 47
  7. def OAI.ContinuumCoulomb.qmaSubdivisionRight line 48
  8. theorem OAI.ContinuumCoulomb.qmaSubdivision_distinct line 50
  9. theorem OAI.ContinuumCoulomb.qmaSubdivision_old_degree line 57
  10. theorem OAI.ContinuumCoulomb.qmaSubdivision_fresh_degree line 62
  11. def OAI.ContinuumCoulomb.qmaSubdivisionState line 73
  12. def OAI.ContinuumCoulomb.qmaSubdivisionNetwork line 95
  13. theorem OAI.ContinuumCoulomb.qmaSubdivision_degree_three line 101