OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactGlobal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Gluing the independently adjusted nineteen-link gadgets along the actual original lattice vertices. All fresh sites retain their source-edge label under the explicit final-graph permutation.

  1. abbrev OAI.ContinuumCoulomb.ContactMediator.GlobalSite line 15
  2. abbrev OAI.ContinuumCoulomb.ContactMediator.GlobalEdge line 18
  3. def OAI.ContinuumCoulomb.ContactMediator.joinedPosition line 21
  4. def OAI.ContinuumCoulomb.ContactMediator.globalPosition line 27
  5. theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_old line 31
  6. theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_internal line 37
  7. theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_local line 45

    Source documentation

    Anchoring a local gadget at zero and seventeen makes its two old vertices agree with the unique global positions of the original spins.

    theorem globalPosition_local (d : SquareLatticeHeisenberg)
    (P : Fin d.edges → LocalSite → ContactPoint)
    (h₀ : ∀ e, P e (localOld 0) = contactPoint 0 0)
    (h₁ : ∀ e, P e (localOld 1) = contactPoint 17 0)
    (e : Fin d.edges) (x : LocalSite) :
    globalPosition d P (localVertex (d.left e) (d.right e) e x) =
      (d.contactEdge e).place (P e x) := by
…

    Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.ContactMediator.LocalSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.ContactMediator.localOld, OAI.ContinuumCoulomb.contactPoint, OAI.ContinuumCoulomb.ContactMediator.globalPosition, OAI.ContinuumCoulomb.ContactMediator.localVertex

  8. theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_link_lengths line 65

    Source documentation

    The exact edge lengths of the local gadgets are the lengths of every edge in the actual final mediator enumeration.

    theorem globalPosition_link_lengths (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 → ℝ)
    (hℓ : ∀ e a, dist (P e (localLeft (member (d.coefficient e)) a))
      (P e (localRight a)) = ℓ (encodeEdge d.edges e a)) (a : GlobalEdge d) :
    dist (globalPosition d P ((finalGraph d.bonds W G).left a))
      (globalPosition d P ((finalGraph d.bonds W G).right a)) = ℓ a := 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.ContactMediator.globalPosition

  9. theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_internal_near_strip line 87

    Source documentation

    The independent local adjustments stay close to points in the exact canonical strip belonging to their original source edge.

    theorem globalPosition_internal_near_strip (d : SquareLatticeHeisenberg)
    (P : Fin d.edges → LocalSite → ContactPoint)
    (hP : ∀ e x, dist (P e x)
      (contactBaseGadgetPosition (edgeNegative d.bonds e) (localToContact x)) < 1 / 20)
    (e : Fin d.edges) (u : LocalInternal) :
    ∃ p : ContactStripSite, dist ((d.contactEdge e).place
      (contactPoint p.axial p.transverse))
      (globalPosition d P (siteEquiv d.vertices d.edges (Sum.inr (e, u)))) < 1 / 20 := by
…

    Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.ContactMediator.LocalSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.contactBaseGadgetPosition, OAI.ContinuumCoulomb.ContactMediator.edgeNegative, OAI.ContinuumCoulomb.ContactMediator.localToContact, OAI.ContinuumCoulomb.ContactMediator.LocalInternal, OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.contactPoint, OAI.ContinuumCoulomb.ContactMediator.globalPosition, OAI.ContinuumCoulomb.ContactMediator.siteEquiv

  10. theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_distinct_gadgets line 115

    Source documentation

    All fresh sites belonging to distinct original edges have the fixed nonedge margin, uniformly in the size of the original lattice graph.

    theorem globalPosition_distinct_gadgets (d : SquareLatticeHeisenberg)
    (P : Fin d.edges → LocalSite → ContactPoint)
    (hP : ∀ e x, dist (P e x)
      (contactBaseGadgetPosition (edgeNegative d.bonds e) (localToContact x)) < 1 / 20)
    (e f : Fin d.edges) (hef : e ≠ f) (u v : LocalInternal) :
    6 / 5 < dist (globalPosition d P (siteEquiv d.vertices d.edges (Sum.inr (e, u))))
      (globalPosition d P (siteEquiv d.vertices d.edges (Sum.inr (f, v)))) := by
…

    Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.ContactMediator.LocalSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.contactBaseGadgetPosition, OAI.ContinuumCoulomb.ContactMediator.edgeNegative, OAI.ContinuumCoulomb.ContactMediator.localToContact, OAI.ContinuumCoulomb.ContactMediator.LocalInternal, OAI.ContinuumCoulomb.ContactMediator.globalPosition, OAI.ContinuumCoulomb.ContactMediator.siteEquiv

  11. theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_nonincident line 129

    Source documentation

    A nonincident original spin is separated from every fresh site of a gadget, including after its independent contact-length adjustment.

    theorem globalPosition_nonincident (d : SquareLatticeHeisenberg)
    (P : Fin d.edges → LocalSite → ContactPoint)
    (hP : ∀ e x, dist (P e x)
      (contactBaseGadgetPosition (edgeNegative d.bonds e) (localToContact x)) < 1 / 20)
    (i : Fin d.vertices) (e : Fin d.edges) (hi₀ : i ≠ d.left e) (hi₁ : i ≠ d.right e)
    (u : LocalInternal) :
    6 / 5 < dist (globalPosition d P (siteEquiv d.vertices d.edges (Sum.inr (e, u))))
      (globalPosition d P (siteEquiv d.vertices d.edges (Sum.inl i))) := by
…

    Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.ContactMediator.LocalSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.contactBaseGadgetPosition, OAI.ContinuumCoulomb.ContactMediator.edgeNegative, OAI.ContinuumCoulomb.ContactMediator.localToContact, OAI.ContinuumCoulomb.ContactMediator.LocalInternal, OAI.ContinuumCoulomb.ContactMediator.globalPosition, OAI.ContinuumCoulomb.ContactMediator.siteEquiv