FiveComponentCanonical.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.FiveComponentGeometry.exists_canonical_neighborhoods line 16
Source documentation
Common component neighborhoods on which both canonical Coulomb certificates hold, including their one-way symmetric contact localization.
```
theorem exists_canonical_neighborhoods
    (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3)) :
    ∃ W : Fin 5 → Set E3,
      (∀ i, W i ∈ nhds (point i)) ∧
      LocalTypeCertificate W (potentials C₁ C₂) (branchContact C₁ C₂) 0 1 2 ∧
      LocalTypeCertificate W (potentials C₁ C₂) (branchContact C₁ C₂) 0 3 4 := by
…
```
Mentions: OAI.Problem356.FiveComponentGeometry.ChartsAt, OAI.Problem356.E3, OAI.Problem356.FiveComponentGeometry.potentials, OAI.Problem356.FiveComponentGeometry.branchContact

theorem OAI.Problem356.FiveComponentGeometry.eventually_good_certificate line 95

Source documentation

The actual chart pair supplies the neighborhood hypothesis for every good component type in the finite global gluing theorem.

theorem eventually_good_certificate
    (C₁ : ChartsAt (point 1)) (C₂ : ChartsAt (point 3))
    (i j k : Fin 5) (hg : Good i j k) :
    ∀ᶠ t : Triple in nhds (point i, (point j, point k)),
      ENNReal.ofReal (potentials C₁ C₂ i t.1 + potentials C₁ C₂ j t.2.1 +
        potentials C₁ C₂ k t.2.2) ≤ coulombCost t ∧
      (ENNReal.ofReal (potentials C₁ C₂ i t.1 + potentials C₁ C₂ j t.2.1 +
        potentials C₁ C₂ k t.2.2) = coulombCost t → branchContact C₁ C₂ t) := by
…

Mentions: OAI.Problem356.FiveComponentGeometry.ChartsAt, OAI.Problem356.Triple, OAI.Problem356.FiveComponentGeometry.potentials, OAI.Problem356.coulombCost, OAI.Problem356.FiveComponentGeometry.branchContact