The star decomposition

Regluing the explosion along the matching restores the fragment (explode_reglue): an induction over a list of orbit representatives, each step being explodeAtGluePair, threaded through glueList_cons. Taking the representatives to be the canonical ones gives starDecomposition, the accompanying paper's "stars and closed graphs" (§3.2): every closed fragment is its star union glued along the edge matching.

def RS.repPairs (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (l : List W.Flag) : (∀ x ∈ l, x ∈ C) → List (↥C × ↥C)

The matching pairs of a representative list, as labels of the explosion at C.

Equations

• RS.repPairs W C hC [] x_2 = []
• RS.repPairs W C hC (x_2 :: l) h = (⟨x_2, ⋯⟩, ⟨W.pairing x_2, ⋯⟩) :: RS.repPairs W C hC l ⋯

def RS.Covers (W : ClosedFragment) (C : Finset W.Flag) (l : List W.Flag) : Prop

Coverage: the orbits of the list exhaust the cut set.

Equations

• RS.Covers W C l = ∀ g ∈ C, ∃ x ∈ l, g = x ∨ g = W.pairing x

theorem RS.covers_tail (W : ClosedFragment) {C : Finset W.Flag} {x : W.Flag} {l : List W.Flag} (hcov : Covers W C (x :: l)) (hdisj : ∀ y ∈ l, y ≠ x ∧ y ≠ W.pairing x ∧ W.pairing y ≠ x ∧ W.pairing y ≠ W.pairing x) : Covers W (cutErase W C x) l

The tail of a representative list covers the shrunken cut set, provided the head's orbit is disjoint from the tail's pairs (from well-formedness).

theorem RS.mem_repPairs_flat (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (l : List W.Flag) (h : ∀ x ∈ l, x ∈ C) (z : ↥C) : z ∈ List.flatMap (fun (p : ↥C × ↥C) => [p.1, p.2]) (repPairs W C hC l h) ↔ ∃ y ∈ l, ↑z = y ∨ ↑z = W.pairing y

Membership in the flattened matching pairs: the orbits of the list.

theorem RS.repPairs_surv_isEmpty (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (l : List W.Flag) (h : ∀ x ∈ l, x ∈ C) (hcov : Covers W C l) : IsEmpty (Fragment.FoldSurviving (↥C) (repPairs W C hC l h))

No label survives a covering matching.

theorem RS.coerce_repPairs (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (x : W.Flag) (hx : x ∈ C) (l : List W.Flag) (h : ∀ y ∈ l, y ∈ C) (h' : ∀ y ∈ l, y ∈ cutErase W C x) (hsep : Fragment.PairsSep (stepLabelI W C x hx) (stepLabelJ W C hC x hx) (repPairs W C hC l h)) : Fragment.coercePairsList (stepLabelI W C x hx) (stepLabelJ W C hC x hx) (repPairs W C hC l h) hsep = Fragment.mapPairs (stepLabelEquiv W C hC x hx) (repPairs W (cutErase W C x) ⋯ l h')

The coerced matching tail is the matching of the shrunken cut set, through the step label equivalence.

theorem RS.repPairs_mem (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (l : List W.Flag) (h : ∀ x ∈ l, x ∈ C) {y : W.Flag} (hy : y ∈ l) : (⟨y, ⋯⟩, ⟨W.pairing y, ⋯⟩) ∈ repPairs W C hC l h

The pair of a list member is in the matching.

theorem RS.repPairs_head_disj (W : ClosedFragment) {C : Finset W.Flag} {hC : CutClosed W C} {x : W.Flag} {l : List W.Flag} {h : ∀ y ∈ x :: l, y ∈ C} (wf : Fragment.PairsWF (repPairs W C hC (x :: l) h)) (y : W.Flag) : y ∈ l → y ≠ x ∧ y ≠ W.pairing x ∧ W.pairing y ≠ x ∧ W.pairing y ≠ W.pairing x

The head-orbit disjointness facts, from well-formedness.

theorem RS.mapPairs_wf_of {α β : Type} (e : α ≃ β) {ps : List (α × α)} (h : Fragment.PairsWF (Fragment.mapPairs e ps)) : Fragment.PairsWF ps

Well-formedness transports along mapped pairs.

noncomputable def RS.explodeAtNotMem (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (hne : ∀ (f : W.Flag), f ∉ C) (e0 : Fin 0 ≃ ↥C) : (Fragment.relabel W e0).Equiv (explodeAt W C hC)

The explosion at a memberless cut set is the fragment, generalized over the cut set.

Equations

• RS.explodeAtNotMem W C hC hne e0 = { flagEquiv := (Equiv.sumEmpty W.Flag ↥C).symm, vertexEquiv := Equiv.refl W.Vertex, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

theorem RS.explode_reglue (W : ClosedFragment) (l : List W.Flag) (C : Finset W.Flag) (hC : CutClosed W C) (h : ∀ x ∈ l, x ∈ C) (_hcov : Covers W C l) (wf : Fragment.PairsWF (repPairs W C hC l h)) (e : Fin 0 ≃ Fragment.FoldSurviving (↥C) (repPairs W C hC l h)) : Nonempty (((explodeAt W C hC).glueList (repPairs W C hC l h) wf).Equiv (Fragment.relabel W e))

The regluing induction: gluing the covering matching in the explosion restores the fragment.

theorem RS.repPairs_wf_of (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (l : List W.Flag) (h : ∀ x ∈ l, x ∈ C) : l.Nodup → (∀ x ∈ l, ∀ y ∈ l, x ≠ y → x ≠ W.pairing y) → Fragment.PairsWF (repPairs W C hC l h)

Well-formedness of the matching from list distinctness and orbit disjointness.

noncomputable def RS.canonicalReps (W : ClosedFragment) : List W.Flag

The canonical orbit representatives: flags enumerated below their partners.

Equations

• RS.canonicalReps W = {f : W.Flag | ↑((Fintype.equivFin W.Flag) f) < ↑((Fintype.equivFin W.Flag) (W.pairing f))}.toList

theorem RS.mem_canonicalReps (W : ClosedFragment) {f : W.Flag} : f ∈ canonicalReps W ↔ ↑((Fintype.equivFin W.Flag) f) < ↑((Fintype.equivFin W.Flag) (W.pairing f))

A flag represents its edge exactly when it is the lower of the two under the enumeration.

theorem RS.canonicalReps_covers (W : ClosedFragment) : Covers W Finset.univ (canonicalReps W)

The canonical representatives cover everything.

theorem RS.canonicalReps_disj (W : ClosedFragment) (x : W.Flag) : x ∈ canonicalReps W → ∀ y ∈ canonicalReps W, x ≠ y → x ≠ W.pairing y

The canonical representatives are orbit-disjoint.

theorem RS.fullCut_closed (W : ClosedFragment) : CutClosed W Finset.univ

The full cut is pairing-closed.

theorem RS.canonicalReps_wf (W : ClosedFragment) : Fragment.PairsWF (repPairs W Finset.univ ⋯ (canonicalReps W) ⋯)

The canonical matching is well-formed.

instance RS.canonical_surv_isEmpty (W : ClosedFragment) : IsEmpty (Fragment.FoldSurviving (↥Finset.univ) (repPairs W Finset.univ ⋯ (canonicalReps W) ⋯))

Regluing the whole matching leaves no surviving label: the decomposition closes the fragment.

theorem RS.starDecomposition (W : ClosedFragment) : Nonempty (((explodeAt W Finset.univ ⋯).glueList (repPairs W Finset.univ ⋯ (canonicalReps W) ⋯) ⋯).Equiv (Fragment.relabel W (Equiv.equivOfIsEmpty (Fin 0) (Fragment.FoldSurviving (↥Finset.univ) (repPairs W Finset.univ ⋯ (canonicalReps W) ⋯)))))

The star decomposition (accompanying paper §3.2, "stars and closed graphs"): every closed fragment is its star union, reglued along the canonical edge matching.