ContactLattice.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual gadget sites fit the common lattice strips. Together with ContactStrips, this separates distinct edges without a size-dependent loss.

theorem OAI.ContinuumCoulomb.contactPoint_eta line 11
theorem OAI.ContinuumCoulomb.contactBaseGadget_internal_strip line 17
Source documentation
Every base-gadget site other than the two original vertices belongs to the uniform internal strip.
```
theorem contactBaseGadget_internal_strip (negative : Bool) (x : ContactGadgetSite)
    (hleft : x ≠ Sum.inl 0) (hright : x ≠ contactGadgetRightNode negative 9) :
    ∃ p : ContactStripSite,
      contactBaseGadgetPosition negative x = contactPoint p.axial p.transverse := by
…
```
Mentions: OAI.ContinuumCoulomb.ContactGadgetSite, OAI.ContinuumCoulomb.contactGadgetRightNode, OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.contactBaseGadgetPosition, OAI.ContinuumCoulomb.contactPoint
theorem OAI.ContinuumCoulomb.perpendicularContact_perturbed_separation line 71
Source documentation
Perpendicular-edge separation persists for the actual adjusted nodes.
```
theorem perpendicularContact_perturbed_separation (a b c d : ℤ) (p q : ContactStripSite)
    (x y : ContactPoint) (hx : dist (horizontalContact a b p) x ≤ 1 / 20)
    (hy : dist (verticalContact c d q) y ≤ 1 / 20) : 6 / 5 < dist x y :=
…
```
Mentions: OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.horizontalContact, OAI.ContinuumCoulomb.verticalContact

theorem OAI.ContinuumCoulomb.horizontalContact_perturbed_separation line 77

Source documentation

Parallel-edge separation persists with the same fixed margin.

theorem horizontalContact_perturbed_separation (a b c d : ℤ)
    (hne : (a, b) ≠ (c, d)) (p q : ContactStripSite)
    (x y : ContactPoint) (hx : dist (horizontalContact a b p) x ≤ 1 / 20)
    (hy : dist (horizontalContact c d q) y ≤ 1 / 20) : 6 / 5 < dist x y :=
…

Mentions: OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.horizontalContact