ContactCommonBranches.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Extract the canonical four-branch selector from an original contact graph.

theorem OAI.Problem356.ContactSelection.second_selects_common_four line 17
Source documentation
A permuted original contact graph with its first coordinate central selects one of the four inverse-reparametrized branches, in the canonical ordering Y₁,W₁,Y₂,W₂. Only the two displayed outer points need lie outside B.
```
theorem second_selects_common_four
    (X Z : Fin 2 → OpenPartialHomeomorph E E)
    {B : Set E} {x y z s : E} {k : Fin 2}
    (hperm : List.Perm [x, y, z] [X k s, s, Z k s])
    (hx : x ∈ B) (hs : s ∈ (X k).source)
    (hsB : s ∉ B) (hzB : Z k s ∉ B) :
    ∃ i : Fin 4, y = CommonBranches.four X Z i x := by
…
```
Mentions: OAI.Problem356.CommonBranches.four