OAI/Geometry/HyperbolicGroups/PlanarSubpairing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.PictureSwitch.joins_pairing line 16
  2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_edge line 36
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_sq line 51
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.complement_subpairing line 59
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.complement_support line 65
  6. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_euler line 79

    Source documentation

    Literal edge-subgraph planarity with retained vertex slots. Fixed points of q are unpaired stubs, so support/2 counts ONLY remaining edges. This Euler equation is proved for EVERY chosen subset of actual edges, and is the subgraph input needed in a recursive planar separator construction.

    theorem subpairing_euler (hG : M.GenusZero) :
    cycles M.vertex + cycles (M.vertex * q) - (q.support.card : ℤ) / 2 =
      2 * (Nat.card (Quotient (SameCycle.setoid M.vertex ⊔ SameCycle.setoid q)) : ℤ) := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles