OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactGlobalSeparation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContinuumCoulomb.ContactMediator.localVertex_old_zero line 11
2. theorem OAI.ContinuumCoulomb.ContactMediator.localVertex_old_one line 15
3. theorem OAI.ContinuumCoulomb.ContactMediator.localVertex_internal line 19
4. def OAI.ContinuumCoulomb.ContactMediator.Nonedge line 22
5. theorem OAI.ContinuumCoulomb.ContactMediator.Nonedge.symm line 25
6. theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_local_nonedge line 30
7. theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_nonedge line 48

   Source documentation

   Combining the local nonedge theorem with distinct-strip and external vertex estimates gives the fixed margin on every nonedge of finalGraph.

   theorem globalPosition_nonedge (d : SquareLatticeHeisenberg) (W G : ℕ)
       (P : Fin d.edges → LocalSite → ContactPoint)
       (h₀ : ∀ e, P e (localOld 0) = contactPoint 0 0)
       (h₁ : ∀ e, P e (localOld 1) = contactPoint 17 0)
       (hsep : ∀ e x y, x ≠ y → Nonedge d W G
         (localVertex (d.left e) (d.right e) e x)
         (localVertex (d.left e) (d.right e) e y) → 6 / 5 < dist (P e x) (P e y))
       (hP : ∀ e x, dist (P e x)
         (contactBaseGadgetPosition (edgeNegative d.bonds e) (localToContact x)) < 1 / 20)
       (x y : GlobalSite d) (hne : x ≠ y) (hn : Nonedge d W G x y) :
       6 / 5 < dist (globalPosition d P x) (globalPosition d P y) := by
   …

   Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.ContactMediator.LocalSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.ContactMediator.localOld, OAI.ContinuumCoulomb.contactPoint, OAI.ContinuumCoulomb.ContactMediator.Nonedge, OAI.ContinuumCoulomb.ContactMediator.localVertex, OAI.ContinuumCoulomb.contactBaseGadgetPosition, OAI.ContinuumCoulomb.ContactMediator.edgeNegative, OAI.ContinuumCoulomb.ContactMediator.localToContact, OAI.ContinuumCoulomb.ContactMediator.GlobalSite, OAI.ContinuumCoulomb.ContactMediator.globalPosition

8. theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_separation line 110

   Source documentation

   With the prescribed local lengths, all distinct sites have at least the smallest permitted edge length, whether or not they are adjacent.

   theorem globalPosition_separation (d : SquareLatticeHeisenberg) (W G : ℕ)
       (P : Fin d.edges → LocalSite → ContactPoint)
       (h₀ : ∀ e, P e (localOld 0) = contactPoint 0 0)
       (h₁ : ∀ e, P e (localOld 1) = contactPoint 17 0)
       (ℓ : GlobalEdge d → ℝ)
       (hlen : ∀ e a, dist (P e (localLeft (member (d.coefficient e)) a))
         (P e (localRight a)) = ℓ (encodeEdge d.edges e a))
       (hℓ : ∀ a, 1 - contactLengthTolerance ≤ ℓ a)
       (hsep : ∀ x y, x ≠ y → Nonedge d W G x y →
         6 / 5 < dist (globalPosition d P x) (globalPosition d P y))
       (x y : GlobalSite d) (hne : x ≠ y) :
       1 - contactLengthTolerance ≤ dist (globalPosition d P x) (globalPosition d P y) := by
   …

   Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.ContactMediator.LocalSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.ContactMediator.localOld, OAI.ContinuumCoulomb.contactPoint, OAI.ContinuumCoulomb.ContactMediator.GlobalEdge, OAI.ContinuumCoulomb.ContactMediator.localLeft, OAI.ContinuumCoulomb.ContactMediator.localRight, OAI.ContinuumCoulomb.ContactMediator.encodeEdge, OAI.ContinuumCoulomb.contactLengthTolerance, OAI.ContinuumCoulomb.ContactMediator.Nonedge, OAI.ContinuumCoulomb.ContactMediator.globalPosition, OAI.ContinuumCoulomb.ContactMediator.GlobalSite