ContactGrid.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Rigid placements of the fixed contact strip on the square lattice. Reversing an original edge reflects its axial coordinate; this keeps its internal points in the same canonical strip.

def OAI.ContinuumCoulomb.contactGridPoint line 13
Source documentation
The original square-lattice vertices are spaced seventeen units apart.
```
def contactGridPoint (a : ℤ × ℤ) : ContactPoint :=
…
```
Mentions: OAI.ContinuumCoulomb.ContactPoint
def OAI.ContinuumCoulomb.contactReflect line 16
def OAI.ContinuumCoulomb.contactHorizontal line 18
def OAI.ContinuumCoulomb.contactVertical line 21
theorem OAI.ContinuumCoulomb.contact_dist_eq_of_sq_eq line 24
theorem OAI.ContinuumCoulomb.contactReflect_dist line 28
theorem OAI.ContinuumCoulomb.contactHorizontal_dist line 36
theorem OAI.ContinuumCoulomb.contactVertical_dist line 44
def OAI.ContinuumCoulomb.ContactStripSite.reflect line 52
theorem OAI.ContinuumCoulomb.contactReflect_strip line 62
structure OAI.ContinuumCoulomb.ContactGridEdge line 68
Source documentation
The canonical key of a lattice edge consists of its direction and its lower/left endpoint. The final Boolean records the input orientation.
```
structure ContactGridEdge where
…
```
def OAI.ContinuumCoulomb.ContactGridEdge.key line 74
def OAI.ContinuumCoulomb.ContactGridEdge.upper line 76
def OAI.ContinuumCoulomb.ContactGridEdge.left line 79
def OAI.ContinuumCoulomb.ContactGridEdge.right line 82
def OAI.ContinuumCoulomb.ContactGridEdge.place line 85
theorem OAI.ContinuumCoulomb.ContactGridEdge.place_dist line 89
theorem OAI.ContinuumCoulomb.ContactGridEdge.place_zero line 96
theorem OAI.ContinuumCoulomb.ContactGridEdge.place_end line 103
theorem OAI.ContinuumCoulomb.ContactGridEdge.place_strip line 111
Source documentation
The orientation flag does not alter the strip containing an internal site.
```
theorem ContactGridEdge.place_strip (e : ContactGridEdge) (p : ContactStripSite) :
    ∃ q : ContactStripSite, e.place (contactPoint p.axial p.transverse) =
      if e.vertical then verticalContact e.anchor.1 e.anchor.2 q
      else horizontalContact e.anchor.1 e.anchor.2 q := by
…
```
Mentions: OAI.ContinuumCoulomb.ContactGridEdge, OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.contactPoint, OAI.ContinuumCoulomb.verticalContact, OAI.ContinuumCoulomb.horizontalContact
theorem OAI.ContinuumCoulomb.verticalContact_separation line 121
Source documentation
Vertical parallel strips have the same separation as horizontal ones.
```
theorem verticalContact_separation (a b c d : ℤ)
    (hne : (a, b) ≠ (c, d)) (p q : ContactStripSite) :
    7 / 5 < dist (verticalContact a b p) (verticalContact c d q) := by
…
```
Mentions: OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.verticalContact
theorem OAI.ContinuumCoulomb.ContactGridEdge.distinct_strip_separation line 139

theorem OAI.ContinuumCoulomb.ContactGridEdge.distinct_perturbed_separation line 158

Source documentation

Perturbed internal nodes of distinct original edges remain noncontacts.

theorem ContactGridEdge.distinct_perturbed_separation (e f : ContactGridEdge)
    (hne : e.key ≠ f.key) (p q : ContactStripSite) (x y : ContactPoint)
    (hx : dist (e.place (contactPoint p.axial p.transverse)) x ≤ 1 / 20)
    (hy : dist (f.place (contactPoint q.axial q.transverse)) y ≤ 1 / 20) :
    6 / 5 < dist x y :=
…

Mentions: OAI.ContinuumCoulomb.ContactGridEdge, OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.contactPoint

theorem OAI.ContinuumCoulomb.int_abs_difference_one line 165
theorem OAI.ContinuumCoulomb.contactGridPoint_separation line 173
theorem OAI.ContinuumCoulomb.horizontalContact_external_vertex line 190
Source documentation
A lattice vertex outside the two endpoints is far from the entire horizontal internal strip, before any adjustment.
```
theorem horizontalContact_external_vertex (a c : ℤ × ℤ) (p : ContactStripSite)
    (h₀ : c ≠ a) (h₁ : c ≠ (a.1 + 1, a.2)) :
    7 / 5 < dist (horizontalContact a.1 a.2 p) (contactGridPoint c) := by
…
```
Mentions: OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.horizontalContact, OAI.ContinuumCoulomb.contactGridPoint
theorem OAI.ContinuumCoulomb.verticalContact_external_vertex line 218
theorem OAI.ContinuumCoulomb.ContactGridEdge.external_vertex_separation line 241