FiveComponentSelection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.FiveComponentGeometry.second_selects_four_of_excluded_charts line 15

Source documentation

The actual symmetric two-graph contact relation yields the exact selector needed by the final construction. Graph-wide outer exclusions are supplied by CoulombSupportExistence.exists_separated_shrink; the final central ball can be any subset of the excluded central neighborhood.

theorem second_selects_four_of_excluded_charts
    (C₁ : ChartsAt (CenterCertificate.point 1))
    (C₂ : ChartsAt (CenterCertificate.point 3))
    {B V : Set E3} (hB : B ⊆ V)
    (houter₁ : ∀ s ∈ C₁.charts.central.source, s ∉ V ∧ C₁.charts.opposite s ∉ V)
    (houter₂ : ∀ s ∈ C₂.charts.central.source, s ∉ V ∧ C₂.charts.opposite s ∉ V)
    {x y z : E3} (hx : x ∈ B) (hc : branchContact C₁ C₂ (x, (y, z))) :
    ∃ i : Fin 4, y = CommonBranches.four
      ![C₁.charts.central, C₂.charts.central]
      ![C₁.charts.opposite, C₂.charts.opposite] i x := by
…

Mentions: OAI.Problem356.FiveComponentGeometry.ChartsAt, OAI.Problem356.CenterCertificate.point, OAI.Problem356.E3, OAI.Problem356.FiveComponentGeometry.branchContact, OAI.Problem356.CommonBranches.four