OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactTemplates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The two fixed nine-link contact templates used after spin subdivision. Coordinates use the Euclidean plane. The link lengths and separation bounds are stable under small movements of the sites.

  1. abbrev OAI.ContinuumCoulomb.ContactPoint line 15
  2. def OAI.ContinuumCoulomb.contactPoint line 17
  3. theorem OAI.ContinuumCoulomb.contactPoint_zero line 19
  4. theorem OAI.ContinuumCoulomb.contactPoint_one line 20
  5. theorem OAI.ContinuumCoulomb.contactPoint_dist_sq line 22
  6. def OAI.ContinuumCoulomb.contactSlopeHeight line 28
  7. def OAI.ContinuumCoulomb.contactStepX line 30
  8. def OAI.ContinuumCoulomb.contactStepY line 33
  9. def OAI.ContinuumCoulomb.contactPathVertex line 37
  10. theorem OAI.ContinuumCoulomb.contactSlopeHeight_sq line 41
  11. theorem OAI.ContinuumCoulomb.contactPathVertex_start line 46
  12. theorem OAI.ContinuumCoulomb.contactPathVertex_end line 49
  13. theorem OAI.ContinuumCoulomb.contactPath_link_length line 58

    Source documentation

    Every specified link of either template has length exactly one.

    theorem contactPath_link_length {c : ℝ} (hc : -1 ≤ c) (hc' : c ≤ 1) (k : ℕ) :
    dist (contactPathVertex c (k + 1)) (contactPathVertex c k) = 1 := by
…

    Mentions: OAI.ContinuumCoulomb.contactPathVertex

  14. theorem OAI.ContinuumCoulomb.contactStepX_lower line 69
  15. theorem OAI.ContinuumCoulomb.contactPath_horizontal_lower line 74

    Source documentation

    Horizontal projection accumulates a uniform positive amount per step.

    theorem contactPath_horizontal_lower {c : ℝ} (hc : c ≤ 1) {i j : ℕ} (hij : i ≤ j) :
    c * (j - i : ℕ) ≤ contactPathVertex c j 0 - contactPathVertex c i 0 := by
…

    Mentions: OAI.ContinuumCoulomb.contactPathVertex

  16. theorem OAI.ContinuumCoulomb.contactPath_nonlink_separation line 84

    Source documentation

    Nonconsecutive vertices on a backbone are separated by at least 1.5.

    theorem contactPath_nonlink_separation {c : ℝ} (hc : 3 / 4 ≤ c) (hc' : c ≤ 1)
    {i j : ℕ} (hij : i + 2 ≤ j) :
    3 / 2 ≤ dist (contactPathVertex c j) (contactPathVertex c i) := by
…

    Mentions: OAI.ContinuumCoulomb.contactPathVertex

  17. theorem OAI.ContinuumCoulomb.contactTemplate_span_eight line 100
  18. theorem OAI.ContinuumCoulomb.contactTemplate_span_eight_half line 104
  19. theorem OAI.ContinuumCoulomb.contact_separation_stable line 110

    Source documentation

    The paper's nonlink margin survives independent small movements.

    theorem contact_separation_stable (x y x' y' : ContactPoint)
    (hsep : 7 / 5 ≤ dist x y) (hx : dist x x' ≤ 1 / 20) (hy : dist y y' ≤ 1 / 20) :
    6 / 5 < dist x' y' := by
…

    Mentions: OAI.ContinuumCoulomb.ContactPoint