OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRouteEnumeration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Only 140 explicit catalog routes need be tested for a physical edge: the seventy oriented routes in each endpoint cell. This supplies a fixed finite search space for the literal planar-route compiler.

  1. def OAI.ContinuumCoulomb.QMACellRouteBody.cell line 12
  2. def OAI.ContinuumCoulomb.qmaCellBodies line 18
  3. def OAI.ContinuumCoulomb.qmaCellRoutes line 25
  4. def OAI.ContinuumCoulomb.qmaRouteCandidates line 28
  5. theorem OAI.ContinuumCoulomb.qmaCellBodies_complete line 31
  6. theorem OAI.ContinuumCoulomb.qmaCellRoutes_complete line 38
  7. theorem OAI.ContinuumCoulomb.qmaCellBodies_length line 44
  8. theorem OAI.ContinuumCoulomb.qmaCellRoutes_length line 47
  9. theorem OAI.ContinuumCoulomb.qmaRouteCandidates_length line 50
  10. theorem OAI.ContinuumCoulomb.QMACellRouteBody.source_cell line 53
  11. theorem OAI.ContinuumCoulomb.qmaRouteCandidates_complete line 66