ContactSelection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The combinatorial step from a permuted contact triple to branch selection.

theorem OAI.Problem356.ContactSelection.first_eq_of_perm line 16
Source documentation
If precisely the first source entry belongs to the central set, any permutation whose first target entry is central has the same first entry.
```
theorem first_eq_of_perm
    {B : Set α} {x y z p q r : α}
    (hperm : List.Perm [x, y, z] [p, q, r])
    (hx : x ∈ B) (hq : q ∉ B) (hr : r ∉ B) : x = p := by
…
```
theorem OAI.Problem356.ContactSelection.second_eq_or_third_of_perm line 29
Source documentation
After identifying the central entry, each remaining entry is one of the other two entries of the contact triple.
```
theorem second_eq_or_third_of_perm
    {B : Set α} {x y z p q r : α}
    (hperm : List.Perm [x, y, z] [p, q, r])
    (hx : x ∈ B) (hq : q ∉ B) (hr : r ∉ B) : y = q ∨ y = r := by
…
```

theorem OAI.Problem356.ContactSelection.second_selects_inverse_branch line 41

Source documentation

A contact triple parameterized by s, with central branch X, selects either Y x or W x once Y inverts X on the parameter domain.

theorem second_selects_inverse_branch
    {B P : Set α} {X Z Y W : α → α} {x y z s : α}
    (hperm : List.Perm [x, y, z] [X s, s, Z s])
    (hx : x ∈ B) (hs : s ∈ P)
    (hOuter : ∀ a ∈ P, a ∉ B ∧ Z a ∉ B)
    (hInverse : ∀ a ∈ P, Y (X a) = a)
    (hW : ∀ a ∈ B, W a = Z (Y a)) : y = Y x ∨ y = W x := by
…