PlanarEdgeOrdering.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.joins_append line 20
lemma OAI.HyperbolicObstruction.PictureSwitch.swaps_append line 27

lemma OAI.HyperbolicObstruction.PictureSwitch.potential_prefix_eq line 33

Source documentation

Equality in the Euler potential propagates to every initial segment. It therefore rules out a hidden handle in every sub-pairing, not only in the fully glued surface.

lemma potential_prefix_eq {p : Perm D} {s : Setoid D}
    (hp : SameCycle.setoid p ≤ s) (l r : List (D × D))
    (he : cycles (p * swaps (l ++ r)) - 2 * (Nat.card (Quotient (joins s (l ++ r))) : ℤ) =
      cycles p - 2 * (Nat.card (Quotient s) : ℤ) + (l ++ r).length) :
    cycles (p * swaps l) - 2 * (Nat.card (Quotient (joins s l)) : ℤ) =
      cycles p - 2 * (Nat.card (Quotient s) : ℤ) + l.length := by
…

Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles, OAI.HyperbolicObstruction.PictureSwitch.swaps, OAI.HyperbolicObstruction.PictureSwitch.joins

lemma OAI.HyperbolicObstruction.PictureSwitch.potential_step_sameCycle line 47
Source documentation
At an Euler-equality step, an edge already in a connected component MUST split a boundary cycle. Merging two boundary cycles within that component would create a handle and strictly lose two units of Euler potential.
```
lemma potential_step_sameCycle {p : Perm D} {s : Setoid D}
    (hp : SameCycle.setoid p ≤ s) (a b : D)
    (he : cycles (p * swap a b) - 2 * (Nat.card (Quotient (glue s a b)) : ℤ) =
      cycles p - 2 * (Nat.card (Quotient s) : ℤ) + 1) :
    p.SameCycle a b ↔ s a b := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles, OAI.HyperbolicObstruction.PictureSwitch.glue
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.paired_joins line 62
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.paired_potential_eq line 79
theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.planar_pairing_order line 97
Source documentation
Every actual genus-zero side pairing admits an edge ordering in which EVERY partial gluing is maximally planar. This is a finite-permutation consequence of the actual Euler definition, not a planarity assumption.
```
theorem planar_pairing_order (hG : M.GenusZero) :
    ∃ l : List (D × D), swaps l = M.edge ∧ 2 * l.length = Fintype.card D ∧
      (∀ ab ∈ l, ab.1 ≠ ab.2 ∧ M.edge ab.1 = ab.2) ∧
      ∀ (r t : List (D × D)) (a b : D), l = r ++ (a,b)::t →
        ((M.vertex * swaps r).SameCycle a b ↔ joins (SameCycle.setoid M.vertex) r a b) := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.swaps, OAI.HyperbolicObstruction.PictureSwitch.joins