OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLocalPathClearance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact endpoint clearance inside one cell. These finite facts separate external corridors from the rays, ordinary pairs and nine gadget paths.

  1. def OAI.ContinuumCoulomb.qmaLocalPhysicalSites line 10
  2. theorem OAI.ContinuumCoulomb.qmaHalfCorridor_sites line 14
  3. theorem OAI.ContinuumCoulomb.qmaCellRay_sites line 18
  4. theorem OAI.ContinuumCoulomb.qmaLocalPatch_sites line 22
  5. theorem OAI.ContinuumCoulomb.qmaCellPair_half line 26
  6. theorem OAI.ContinuumCoulomb.qmaCellRay_half line 30
  7. theorem OAI.ContinuumCoulomb.qmaLocalPatch_half line 34
  8. theorem OAI.ContinuumCoulomb.qmaLocalPatch_bounded line 38