ContactStrips.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform separation of contacts from different lattice edges. The estimates use only fixed strip bounds, so the lattice size never enters their constants.

structure OAI.ContinuumCoulomb.ContactStripSite line 13
Source documentation
Coordinates of an internal site in an oriented length-17 lattice edge. Off-axis sites stay farther from both original endpoints.
```
structure ContactStripSite where
…
```
def OAI.ContinuumCoulomb.horizontalContact line 23
def OAI.ContinuumCoulomb.verticalContact line 26
theorem OAI.ContinuumCoulomb.contact_interval_lattice_distance line 29
theorem OAI.ContinuumCoulomb.contactPoint_coordinate_le_dist line 38
theorem OAI.ContinuumCoulomb.perpendicularContact_separation line 51
Source documentation
Perpendicular gadgets retain the paper's 1.4 nonlink margin.
```
theorem perpendicularContact_separation (a b c d : ℤ) (p q : ContactStripSite) :
    7 / 5 < dist (horizontalContact a b p) (verticalContact c d q) := by
…
```
Mentions: OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.horizontalContact, OAI.ContinuumCoulomb.verticalContact

theorem OAI.ContinuumCoulomb.contact_interval_separation line 119

Source documentation

Internal points from distinct collinear length-17 intervals are at least 2 apart in their axial projection.

theorem contact_interval_separation (a c : ℤ) (hne : a ≠ c) {x y : ℝ}
    (hx : 1 ≤ x) (hx' : x ≤ 16) (hy : 1 ≤ y) (hy' : y ≤ 16) :
    2 ≤ |17 * (a : ℝ) + x - (17 * c + y)| := by
…

theorem OAI.ContinuumCoulomb.contact_parallel_line_separation line 128
theorem OAI.ContinuumCoulomb.horizontalContact_separation line 138
Source documentation
Parallel gadgets from distinct oriented lattice edges do not interfere.
```
theorem horizontalContact_separation (a b c d : ℤ)
    (hne : (a, b) ≠ (c, d)) (p q : ContactStripSite) :
    7 / 5 < dist (horizontalContact a b p) (horizontalContact c d q) := by
…
```
Mentions: OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.horizontalContact