Path data across a closed glue

A closed glue never rewires: the cut edge is the single edge joining the two boundary flags, so a chain of the glued system transports to the unglued one on the nose. The three transports here say so — which flags are boundary after the glue, that the walk agrees step for step, and that the path matching is carried across unchanged.

Generic helpers

The closed path-data engine (either b)

theorem RS.EdgeSubset.mem_boundaryFlags_glueClosed {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (b : Bool) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) {f' : W.SurvivingFlag i j} : f' ∈ { flags := s', pairing_mem := hc' }.boundaryFlags ↔ ↑f' ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.boundaryFlags

Boundary-flag correspondence (closed case): a surviving flag is glued-boundary iff its value is lifted-boundary.

theorem RS.EdgeSubset.iterWalk_unglueClosed_val_all {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (b : Bool) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) (δ' : W.SurvivingFlag i j) (t : ℕ) : iterWalk (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ') (↑δ') t = ↑(iterWalk κ' δ' t)

Unconditional walk agreement (closed case): the closed glue never rewires, so the unglued walk from a surviving flag follows the glued walk valuewise, with no continuation hypothesis.

theorem RS.EdgeSubset.pathMatch_unglueClosed {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (b : Bool) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) {δ' : W.SurvivingFlag i j} (hδ' : δ' ∈ { flags := s', pairing_mem := hc' }.boundaryFlags) (hδl : ↑δ' ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.boundaryFlags) : (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ').pathMatch (↑δ') hδl = ↑(κ'.pathMatch δ' hδ')

pathMatch transport across the closed unglue: chains of surviving boundary flags transport on the nose, for either b.

The non-participating lift (b = false): chord diagram,

path sign, and the signed-value transport

The participating lift (b = true): the signed-value

transport with explicit sign weight

The assembled per-subset split