OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumScaledEdge.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Eightfold unit-edge corridors leave the diagonal leaf sites free.

  1. theorem OAI.ContinuumCoulomb.qmaLeafCenter_length line 11
  2. theorem OAI.ContinuumCoulomb.qmaLeafCenter_adj_length line 15
  3. theorem OAI.ContinuumCoulomb.qmaLeafCenter_point_gridline line 21
  4. theorem OAI.ContinuumCoulomb.qmaRouteLeaf_avoids_corridor line 34
  5. theorem OAI.ContinuumCoulomb.qmaLeafCenter_point_one line 39
  6. theorem OAI.ContinuumCoulomb.qmaLeafCenter_point_first line 46