TreeSubpairingLift.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.lift_spanning_tree line 25
Source documentation
Every spanning tree of the actual underlying graph lifts to a genuine one-boundary dart subpairing. Kruskal is applied ONLY to actual copies of its own edges; connectedness then forces equality with the selected tree. This permits a shortest-path tree, rather than an arbitrary-radius tree.
```
theorem lift_spanning_tree (T : SimpleGraph M.GraphVertex)
    (hle : T ≤ M.underlyingGraph) (hT : T.IsTree) :
    ∃ q : Perm D, ∃ hq : ∀ x, q x = x ∨ q x = M.edge x,
      SameCycle.setoid M.vertex ⊔ SameCycle.setoid q = ⊤ ∧
      cycles (M.vertex*q) = 1 ∧
      M.subpairingGraph q (M.subpairing_sq q hq) = T := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles