ContactExtent.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The contact realization preserves polynomial coordinate extent.

def OAI.ContinuumCoulomb.contactGridAxis line 11
theorem OAI.ContinuumCoulomb.contactGridPoint_apply line 13
theorem OAI.ContinuumCoulomb.ContactGridEdge.strip_coordinate_bound line 19
Source documentation
Every internal strip remains within sixteen coordinate units of its canonical lower/left lattice endpoint.
```
theorem ContactGridEdge.strip_coordinate_bound (e : ContactGridEdge) (p : ContactStripSite)
    (i : Fin 2) :
    |e.place (contactPoint p.axial p.transverse) i - contactGridPoint e.anchor i| ≤ 16 := by
…
```
Mentions: OAI.ContinuumCoulomb.ContactGridEdge, OAI.ContinuumCoulomb.ContactStripSite, OAI.ContinuumCoulomb.contactPoint, OAI.ContinuumCoulomb.contactGridPoint

theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.contactEdge_anchor line 33

Source documentation

A source edge's canonical anchor is one of its two actual endpoints.

theorem SquareLatticeHeisenberg.contactEdge_anchor (d : SquareLatticeHeisenberg)
    (e : Fin d.edges) :
    (d.contactEdge e).anchor = d.coordinate (d.left e) ∨
      (d.contactEdge e).anchor = d.coordinate (d.right e) := by
…

Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg

theorem OAI.ContinuumCoulomb.ContactMediator.globalSite_card line 45
theorem OAI.ContinuumCoulomb.ContactMediator.globalEdge_card line 50
theorem OAI.ContinuumCoulomb.ContactMediator.abs_le_add_abs_sub line 55
theorem OAI.ContinuumCoulomb.ContactMediator.globalPosition_coordinate_bound line 61
Source documentation
Uniform coordinate bounds of the source control the full final graph, including all eighteen fresh sites per edge.
```
theorem globalPosition_coordinate_bound (d : SquareLatticeHeisenberg)
    (P : Fin d.edges → LocalSite → ContactPoint) {M : ℝ}
    (hcoord : ∀ j k, |(contactGridAxis (d.coordinate j) k : ℝ)| ≤ M)
    (hP : ∀ e x, dist (P e x)
      (contactBaseGadgetPosition (edgeNegative d.bonds e) (localToContact x)) < 1 / 20)
    (x : GlobalSite d) (i : Fin 2) :
    |globalPosition d P x i| ≤ 17 * M + 17 := by
…
```
Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.ContactMediator.LocalSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.contactGridAxis, OAI.ContinuumCoulomb.contactBaseGadgetPosition, OAI.ContinuumCoulomb.ContactMediator.edgeNegative, OAI.ContinuumCoulomb.ContactMediator.localToContact, OAI.ContinuumCoulomb.ContactMediator.GlobalSite, OAI.ContinuumCoulomb.ContactMediator.globalPosition
theorem OAI.ContinuumCoulomb.ContactMediator.logarithmic_extent_polynomial line 100
Source documentation
A fixed logarithmic spacing and polynomial source extent give an explicit polynomial bound for every realized coordinate.
```
theorem logarithmic_extent_polynomial (k s : ℕ) {N : ℝ} (hN : 2 ≤ N) :
    (k : ℝ) * Real.log N * (17 * N ^ s + 17) ≤ N ^ (k + s + 7) := by
…
```