Canonical data across a relabel and a glue

Canonical data — a transition system with a path-canonical orientation — transport along a relabel, down across either branch of a single-pair glue, and back up from a closed lift.

Transport along a relabel

theorem RS.EdgeSubset.nonempty_canonData_relabelUp {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃o β) {W : Fragment α} (F : EdgeSubset W) : Nonempty (relabelUp e.toEquiv F).CanonData ↔ Nonempty F.CanonData

Canonical-data existence transports along a relabel.

Descent and the glued tower family (open cut)

The support data transfer across the open glue: Eulerian-ness on the nose, canonical data downward by unglue-and-repair, and the glued pinned family built bottom-up from a lifted family.

theorem RS.nonempty_canonData_unglueOpen {α : Type} [LinearOrder α] {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s') (hne : Nonempty { flags := s', pairing_mem := hc' }.CanonData) : Nonempty { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.CanonData

Canonical data descend across the open unglue.

The closed-cut step at the pinned sum

The mechanical mirror of for the circle-closing cut: support transfer across either lift, the true-lift tower family, and the (k − 2ℓ)-weighted per-subset split — the extra factor is the glued fragment's extra circle, absorbed against the prefactor in the tower.

theorem RS.nonempty_canonData_unglueClosed {α : Type} [LinearOrder α] {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (b : Bool) (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) (hne : Nonempty { flags := s', pairing_mem := hc' }.CanonData) : Nonempty { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.CanonData

Canonical data descend across either closed unglue.

Fibrewise absorption and the per-term relabel

The generic state-fibre regrouping (the 𝒲-form absorber), and the relabel transport at the level of a single pinned term.

theorem RS.nonempty_canonData_glueClosed {α : Type} [LinearOrder α] {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (b : Bool) (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) (hne : Nonempty { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.CanonData) : Nonempty { flags := s', pairing_mem := hc' }.CanonData

Canonical data ascend from either closed lift to the glued subset.