ContactRealization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A geometric realization of the exact final mediator graph, with independently prescribed near-unit edge lengths and uniform nonedge gaps.

theorem OAI.ContinuumCoulomb.ContactMediator.exists_finalGraph_realization line 15

Source documentation

No graph isomorphism or extra geometric premise is assumed: the output is indexed by the actual finalGraph vertices and edges.

theorem exists_finalGraph_realization (d : SquareLatticeHeisenberg) (W G : ℕ)
    (ℓ : GlobalEdge d → ℝ)
    (hℓ : ∀ a, ℓ a ∈ Set.Icc (1 - contactLengthTolerance) (1 + contactLengthTolerance)) :
    ∃ Q : GlobalSite d → ContactPoint,
      (∀ i, Q (siteEquiv d.vertices d.edges (Sum.inl i)) = contactGridPoint (d.coordinate i)) ∧
      (∀ a, dist (Q ((finalGraph d.bonds W G).left a))
        (Q ((finalGraph d.bonds W G).right a)) = ℓ a) ∧
      (∀ x y, x ≠ y → Nonedge d W G x y → 6 / 5 < dist (Q x) (Q y)) ∧
      (∀ x y, x ≠ y → 1 - contactLengthTolerance ≤ dist (Q x) (Q y)) ∧
      (∀ M : ℝ, (∀ j i, |(contactGridAxis (d.coordinate j) i : ℝ)| ≤ M) →
        ∀ x i, |Q x i| ≤ 17 * M + 17) := by
…

Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.ContactMediator.GlobalEdge, OAI.ContinuumCoulomb.contactLengthTolerance, OAI.ContinuumCoulomb.ContactMediator.GlobalSite, OAI.ContinuumCoulomb.ContactPoint, OAI.ContinuumCoulomb.ContactMediator.siteEquiv, OAI.ContinuumCoulomb.contactGridPoint, OAI.ContinuumCoulomb.ContactMediator.Nonedge, OAI.ContinuumCoulomb.contactGridAxis

theorem OAI.ContinuumCoulomb.ContactMediator.dist_real_smul line 44

theorem OAI.ContinuumCoulomb.ContactMediator.exists_scaled_finalGraph_realization line 50

Source documentation

Multiplication by the chosen physical spacing preserves every exact edge length and gives the required strict nonedge separation.

theorem exists_scaled_finalGraph_realization (d : SquareLatticeHeisenberg) (W G : ℕ)
    (D : ℝ) (hD : 0 < D) (ℓ : GlobalEdge d → ℝ)
    (hℓ : ∀ a, ℓ a ∈ Set.Icc (1 - contactLengthTolerance) (1 + contactLengthTolerance)) :
    ∃ Q : GlobalSite d → ContactPoint,
      (∀ a, dist (Q ((finalGraph d.bonds W G).left a))
        (Q ((finalGraph d.bonds W G).right a)) = D * ℓ a) ∧
      (∀ x y, x ≠ y → Nonedge d W G x y → (6 / 5) * D < dist (Q x) (Q y)) ∧
      (∀ x y, x ≠ y → (1 - contactLengthTolerance) * D ≤ dist (Q x) (Q y)) ∧
      Function.Injective Q ∧
      (∀ M : ℝ, (∀ j i, |(contactGridAxis (d.coordinate j) i : ℝ)| ≤ M) →
        ∀ x i, |Q x i| ≤ D * (17 * M + 17)) := by
…