SubpairingTree.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.card_quotient_top_one line 23
theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_isTree line 39
Source documentation
A literal one-boundary spanning subpairing of a connected genus-zero map is a tree on the actual rotation vertices. This also rules out retained loops and duplicate edges: the edge-count bound and connectivity force equality.
```
theorem subpairing_isTree (hG : M.GenusZero) (q : Perm D)
    (hsub : ∀ x, q x = x ∨ q x = M.edge x)
    (hspan : SameCycle.setoid M.vertex ⊔ SameCycle.setoid q = ⊤)
    (hboundary : cycles (M.vertex*q) = 1) :
    (M.subpairingGraph q (M.subpairing_sq q hsub)).IsTree := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles

theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.connected_tree_cotree line 67

Source documentation

Complementary primal and dual TREE graphs, obtained from the real side-pairing and exact genus-zero equation. No abstract drawing or tree interface has been substituted for the rotation system.

theorem connected_tree_cotree (hG : M.GenusZero) (hconn : M.components = ⊤) :
    ∃ q : Perm D, ∃ hq : ∀ x, q x = x ∨ q x = M.edge x,
      (M.subpairingGraph q (M.subpairing_sq q hq)).IsTree ∧
      (M.dual.subpairingGraph (q*M.edge)
        (M.subpairing_sq (q*M.edge) (M.complement_subpairing q hq))).IsTree := by
…