OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactMediatorLinks.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The contact adjacency is exactly the edge relation of the actual nineteen-link gadget, including the signed central attachment.

  1. def OAI.ContinuumCoulomb.ContactMediator.samePair line 11
  2. theorem OAI.ContinuumCoulomb.ContactMediator.samePair_swap_target line 14
  3. theorem OAI.ContinuumCoulomb.ContactMediator.samePair_trans line 17
  4. theorem OAI.ContinuumCoulomb.ContactMediator.samePair_map line 23
  5. def OAI.ContinuumCoulomb.ContactMediator.contactPair line 27
  6. theorem OAI.ContinuumCoulomb.ContactMediator.leftEdge_pair line 31
  7. theorem OAI.ContinuumCoulomb.ContactMediator.rightEdge_pair line 37
  8. theorem OAI.ContinuumCoulomb.ContactMediator.adjacent_indices line 44
  9. theorem OAI.ContinuumCoulomb.ContactMediator.left_adjacent_exists line 53
  10. theorem OAI.ContinuumCoulomb.ContactMediator.right_nodes line 62
  11. theorem OAI.ContinuumCoulomb.ContactMediator.right_adjacent_exists line 69
  12. theorem OAI.ContinuumCoulomb.ContactMediator.contactLinked_exists line 83
  13. theorem OAI.ContinuumCoulomb.ContactMediator.contactLinked_symm line 118
  14. theorem OAI.ContinuumCoulomb.ContactMediator.contactLinked_iff line 123
  15. theorem OAI.ContinuumCoulomb.ContactMediator.finalGraph_nonedge_contactNonlink line 139

    Source documentation

    A contact link is an edge of the actual full graph. Consequently a nonedge of that graph cannot be an unaccounted local contact.

    theorem finalGraph_nonedge_contactNonlink {n r : ℕ} (F : Bonds n r) (W G : ℕ)
    (e : Fin r) (x y : LocalSite)
    (h : ¬∃ a, samePair ((finalGraph F W G).left a) ((finalGraph F W G).right a)
      (localVertex (F.left e) (F.right e) e x) (localVertex (F.left e) (F.right e) e y)) :
    ¬contactGadgetLinked (edgeNegative F e) (localToContact x) (localToContact y) := by
…

    Mentions: OAI.ContinuumCoulomb.ContactMediator.LocalSite, OAI.ContinuumCoulomb.ContactMediator.samePair, OAI.ContinuumCoulomb.ContactMediator.localVertex, OAI.ContinuumCoulomb.contactGadgetLinked, OAI.ContinuumCoulomb.ContactMediator.edgeNegative, OAI.ContinuumCoulomb.ContactMediator.localToContact

  16. theorem OAI.ContinuumCoulomb.ContactMediator.exists_finalGraph_gadget_geometry line 152