OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkPatch.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A concrete planar lattice subdivision of the rational fork gadget.

  1. def OAI.ContinuumCoulomb.qmaForkPatchVertex line 11
  2. def OAI.ContinuumCoulomb.qmaForkPatchLeft line 12
  3. def OAI.ContinuumCoulomb.qmaForkPatchRight line 13
  4. def OAI.ContinuumCoulomb.qmaForkPatchPath line 14
  5. theorem OAI.ContinuumCoulomb.qmaForkPatch_endpoints line 21
  6. theorem OAI.ContinuumCoulomb.qmaForkPatch_chain line 26
  7. theorem OAI.ContinuumCoulomb.qmaForkPatch_simple line 30
  8. theorem OAI.ContinuumCoulomb.qmaForkPatch_bounded line 33
  9. theorem OAI.ContinuumCoulomb.qmaForkPatch_length line 36
  10. theorem OAI.ContinuumCoulomb.qmaForkPatch_disjoint line 39
  11. theorem OAI.ContinuumCoulomb.qmaForkPatch_vertices line 43