The star union with a Fin-boundary

The explosion at the full cut, enumerated representatives-first: each edge orbit contributes its canonical representative among the first m boundary labels and its partner among the last m. Under this enumeration the canonical matching becomes the straight matching i ↔ m + i, so the star decomposition says that gluing the straight matching in the star union restores the fragment — the shape the trace calculus closes against the strand bundle.

@[reducible, inline]

noncomputable abbrev RS.edgeCount (W : ClosedFragment) : ℕ

The number of edges: one canonical representative per orbit.

Equations

• RS.edgeCount W = (RS.canonicalReps W).length

theorem RS.canonicalReps_nodup (W : ClosedFragment) : (canonicalReps W).Nodup

The representatives are pairwise distinct: one per edge orbit.

theorem RS.pairing_notMem_canonicalReps (W : ClosedFragment) {f : W.Flag} (h : f ∈ canonicalReps W) : W.pairing f ∉ canonicalReps W

The partner of a representative is not a representative.

theorem RS.mem_or_pairing_mem (W : ClosedFragment) (f : W.Flag) : f ∈ canonicalReps W ∨ W.pairing f ∈ canonicalReps W

Every flag is a representative or the partner of one.

noncomputable def RS.repSplitFun (W : ClosedFragment) (f : W.Flag) : { x : W.Flag // x ∈ canonicalReps W } ⊕ { x : W.Flag // x ∈ canonicalReps W }

The splitting map: a flag to its orbit representative, tagged by which side of the orbit it sits on.

Equations

• RS.repSplitFun W f = if h : f ∈ RS.canonicalReps W then Sum.inl ⟨f, h⟩ else Sum.inr ⟨W.pairing f, ⋯⟩

def RS.repSplitInv (W : ClosedFragment) : { x : W.Flag // x ∈ canonicalReps W } ⊕ { x : W.Flag // x ∈ canonicalReps W } → W.Flag

The inverse splitting map.

Equations

• RS.repSplitInv W (Sum.inl x_1) = ↑x_1
• RS.repSplitInv W (Sum.inr x_1) = W.pairing ↑x_1

noncomputable def RS.repSplitEquiv (W : ClosedFragment) : W.Flag ≃ { x : W.Flag // x ∈ canonicalReps W } ⊕ { x : W.Flag // x ∈ canonicalReps W }

The orbit split: a flag is a representative or a partner.

Equations

• RS.repSplitEquiv W = { toFun := RS.repSplitFun W, invFun := RS.repSplitInv W, left_inv := ⋯, right_inv := ⋯ }

noncomputable def RS.repIndexEquiv (W : ClosedFragment) : { x : W.Flag // x ∈ canonicalReps W } ≃ Fin (edgeCount W)

The list-position equivalence of the representatives.

Equations

• RS.repIndexEquiv W = (List.Nodup.getEquiv (RS.canonicalReps W) ⋯).symm

noncomputable def RS.starEnum (W : ClosedFragment) : ↥Finset.univ ≃ Fin (edgeCount W + edgeCount W)

The star enumeration: representatives on the low labels, partners on the high labels, in list order.

Equations

• RS.starEnum W = ((Equiv.subtypeUnivEquiv ⋯).trans (RS.repSplitEquiv W)).trans (((RS.repIndexEquiv W).sumCongr (RS.repIndexEquiv W)).trans finSumFinEquiv)

noncomputable def RS.starUnion (W : ClosedFragment) : Fragment (Fin (edgeCount W + edgeCount W))

The star union: the explosion at the full cut with the representatives-first boundary enumeration.

Equations

• RS.starUnion W = (RS.explodeAt W Finset.univ ⋯).relabel (RS.starEnum W)

def RS.matchPairs (m : ℕ) : List (Fin (m + m) × Fin (m + m))

The straight matching pairs i ↔ m + i.

Equations

• RS.matchPairs m = List.map (fun (j : Fin m) => (Fin.castAdd m j, Fin.natAdd m j)) (List.finRange m)

theorem RS.matchPairs_length (m : ℕ) : (matchPairs m).length = m

The straight matching has one pair per edge.

theorem RS.matchPairs_getElem (m j : ℕ) (hj : j < (matchPairs m).length) (hj' : j < m) : (matchPairs m)[j] = (Fin.castAdd m ⟨j, hj'⟩, Fin.natAdd m ⟨j, hj'⟩)

Its jth pair is (j, m + j).

theorem RS.mapPairs_length {α β : Type} (e : α ≃ β) (ps : List (α × α)) : (Fragment.mapPairs e ps).length = ps.length

Transporting a pair list along an equivalence keeps its length.

theorem RS.mapPairs_getElem {α β : Type} (e : α ≃ β) (ps : List (α × α)) (j : ℕ) (hj : j < (Fragment.mapPairs e ps).length) (hj' : j < ps.length) : (Fragment.mapPairs e ps)[j] = (e ps[j].1, e ps[j].2)

And moves each pair componentwise.

The enumeration sends the canonical matching to the

straight matching

theorem RS.starEnum_rep (W : ClosedFragment) (j : ℕ) (hj : j < (canonicalReps W).length) : (starEnum W) ⟨(canonicalReps W)[j], ⋯⟩ = Fin.castAdd (edgeCount W) ⟨j, hj⟩

The jth representative gets the low label j.

theorem RS.starEnum_partner (W : ClosedFragment) (j : ℕ) (hj : j < (canonicalReps W).length) : (starEnum W) ⟨W.pairing (canonicalReps W)[j], ⋯⟩ = Fin.natAdd (edgeCount W) ⟨j, hj⟩

Its partner gets the high label m + j — so the canonical matching becomes the straight one.

theorem RS.repPairs_length (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (l : List W.Flag) (h : ∀ x ∈ l, x ∈ C) : (repPairs W C hC l h).length = l.length

The representative pair list has one pair per listed flag.

theorem RS.repPairs_getElem (W : ClosedFragment) (C : Finset W.Flag) (hC : CutClosed W C) (l : List W.Flag) (h : ∀ x ∈ l, x ∈ C) (j : ℕ) (hj : j < (repPairs W C hC l h).length) (hj' : j < l.length) : (repPairs W C hC l h)[j] = (⟨l[j], ⋯⟩, ⟨W.pairing l[j], ⋯⟩)

And its jth pair is that flag with its partner.

theorem RS.mapPairs_repPairs (W : ClosedFragment) : Fragment.mapPairs (starEnum W) (repPairs W Finset.univ ⋯ (canonicalReps W) ⋯) = matchPairs (edgeCount W)

The enumerated canonical matching is the straight matching.

The transported star decomposition

theorem RS.matchPairs_wf_star (W : ClosedFragment) : Fragment.PairsWF (matchPairs (edgeCount W))

The straight matching is a well-formed gluing list on the star union: it is the transported canonical list.

theorem RS.starUnion_surv_isEmpty (W : ClosedFragment) : IsEmpty (Fragment.FoldSurviving (Fin (edgeCount W + edgeCount W)) (matchPairs (edgeCount W)))

Gluing the straight matching in the star union leaves no surviving label: the fold consumes the whole boundary, which is what makes the decomposition restore the fragment.

theorem RS.starUnion_reglue (W : ClosedFragment) : Nonempty (((starUnion W).glueList (matchPairs (edgeCount W)) ⋯).Equiv (Fragment.relabel W (Equiv.equivOfIsEmpty (Fin 0) (Fragment.FoldSurviving (Fin (edgeCount W + edgeCount W)) (matchPairs (edgeCount W))))))

The star union self-glue: gluing the straight matching in the star union restores the fragment.