TreeHull.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PlanarRecursion.tree_closer_neighbor_mem_path line 15
lemma OAI.HyperbolicObstruction.PlanarRecursion.tree_closer_neighbor_unique line 26
def OAI.HyperbolicObstruction.PlanarRecursion.RootClosed line 37
Source documentation
Root closure is the exact property satisfied by a union of root paths. It says every predecessor of a protected vertex is protected.
```
def RootClosed (G : SimpleGraph V) (root : V) (S : Set V) : Prop :=
…
```
theorem OAI.HyperbolicObstruction.PlanarRecursion.tree_boundary_in_hull line 46
Source documentation
Any finite boundary supported on a tree must lie in a root-closed hull of its possible ends. The hypothesis outside the hull asks for two DISTINCT boundary neighbors; the proof uses a furthest unprotected boundary vertex. This is a tree theorem, not a planar separator assumed by an interface.
```
theorem tree_boundary_in_hull {G : SimpleGraph V} (hG : G.IsTree)
    (root : V) (S : Set V) (hS : RootClosed G root S) (B : V → Prop)
    (hB : ∀ v, B v → v ∉ S → ∃ a b, a ≠ b ∧ G.Adj v a ∧ G.Adj v b ∧ B a ∧ B b) :
    ∀ v, B v → v ∈ S := by
…
```
Mentions: OAI.HyperbolicObstruction.PlanarRecursion.RootClosed