The multi-star form of the explosion

The star union of a closed fragment is a multi-star: a family of pendant edges indexed by Fin (2m), each attached to a vertex by an assignment map. This is the bridge between the explosion machinery and the vertex-star factorization.

def RS.multiStar {V : Type} [Fintype V] {n : ℕ} (assign : Fin n → V) (c : ℕ) : Fragment (Fin n)

A multi-star: n pendant edges with a vertex assignment and a free-circle count.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.starFlagEnum (W : ClosedFragment) : W.Flag ≃ Fin (edgeCount W + edgeCount W)

The inner-flag enumeration of the star union: original flags through the star enumeration.

Equations

• RS.starFlagEnum W = (Equiv.subtypeUnivEquiv ⋯).symm.trans (RS.starEnum W)

noncomputable def RS.starAssign (W : ClosedFragment) : Fin (edgeCount W + edgeCount W) → W.Vertex

The vertex assignment of the star union: each slot's original flag sits at its vertex.

Equations

• RS.starAssign W i = W.vertexOf ((RS.starFlagEnum W).symm i)

noncomputable def RS.starUnionMultiStar (W : ClosedFragment) : (starUnion W).Equiv (multiStar (starAssign W) W.circles)

The star union is a multi-star: the explosion at the full cut, enumerated, is the family of pendant edges over the original flags with their vertex assignment.

Equations

• RS.starUnionMultiStar W = { flagEquiv := (RS.starFlagEnum W).sumCongr (RS.starEnum W), vertexEquiv := Equiv.refl W.Vertex, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }