OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingPatch.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A concrete square-grid subdivision of the nine-edge crossing gadget. Its four terminals lie on the boundary with their outward directions free.

  1. def OAI.ContinuumCoulomb.qmaCrossingPatchVertex line 12
  2. def OAI.ContinuumCoulomb.qmaCrossingPatchLeft line 13
  3. def OAI.ContinuumCoulomb.qmaCrossingPatchRight line 14
  4. def OAI.ContinuumCoulomb.qmaCrossingPatchPath line 15
  5. theorem OAI.ContinuumCoulomb.qmaCrossingPatch_endpoints line 26
  6. theorem OAI.ContinuumCoulomb.qmaCrossingPatch_chain line 31
  7. theorem OAI.ContinuumCoulomb.qmaCrossingPatch_simple line 36
  8. theorem OAI.ContinuumCoulomb.qmaCrossingPatch_bounded line 39
  9. theorem OAI.ContinuumCoulomb.qmaCrossingPatch_length line 43
  10. theorem OAI.ContinuumCoulomb.qmaCrossingPatch_disjoint line 46
  11. theorem OAI.ContinuumCoulomb.qmaCrossingPatch_vertices line 51
  12. def OAI.ContinuumCoulomb.qmaCrossingPatchInt line 53
  13. def OAI.ContinuumCoulomb.qmaCrossingPatchPort line 54
  14. theorem OAI.ContinuumCoulomb.qmaCrossingPatch_port_step line 56
  15. theorem OAI.ContinuumCoulomb.qmaCrossingPatch_port_unused line 63
  16. theorem OAI.ContinuumCoulomb.qmaCrossingPatch_interior_fresh line 67