BlockOrbitSubtype.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.blockEdgeOrbit_touches line 10
Source documentation
The supported permutation orbit of a free edge consists only of free edges.
```
theorem blockEdgeOrbit_touches {n : ℕ} {B : Finset (Fin n)}
    {e d : GraphEdge n} (he : EdgeTouches B e) (hd : d ∈ blockEdgeOrbit B e) :
    EdgeTouches B d := by
…
```
Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.EdgeTouches, OAI.Problem313.blockEdgeOrbit
theorem OAI.Problem313.exists_freeEdge_orbit_family line 19
Source documentation
A free edge has at least B.card free-edge orbit mates, with explicit supported-permutation witnesses. This is the finite-coordinate interface for conditional influence bounds.
```
theorem exists_freeEdge_orbit_family {n : ℕ} (B : Finset (Fin n))
    (hB : 3 ≤ B.card) (e : {e : GraphEdge n // EdgeTouches B e}) :
    ∃ S : Finset {d : GraphEdge n // EdgeTouches B d},
      B.card ≤ S.card ∧ ∀ d ∈ S, ∃ π : Equiv.Perm (Fin n),
        SupportedOnBlock B π ∧ permEdge π e.val = d.val := by
…
```
Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.EdgeTouches, OAI.Problem313.SupportedOnBlock, OAI.Problem313.permEdge