The boundary pairing of a glued system by chain following

For an open single-pair glue W' = W.gluePairOpen i j hij hopen and a transition system κ on the lifted edge subset, this file computes the pathMatch of the glued system RelTransitionSystem.glueOpen … κ on the glued boundary flags in terms of the pathMatch of κ:

• mem_boundaryFlags_glueOpen — a surviving flag is a boundary flag of the glued subset iff its value is a boundary flag of the lifted subset (the two cut flags are excluded automatically, being non-surviving).
• pathMatch_glueOpen_of_ne — when the κ-chain of δ' exits away from the two cut flags, the glued chain follows it exactly.
• pathMatch_glueOpen_hit_i / pathMatch_glueOpen_hit_j — when the κ-chain of δ' exits at a cut flag, the glued chain crosses the rewired interface and continues along the other cut flag's chain to its exit.
• glued_participation_iff — a glued boundary flag participates in the glued subset exactly when its value participates in the lifted one.

The open-gluing context

Boundary-flag correspondence

theorem RS.EdgeSubset.mem_boundaryFlags_glueOpen {α : Type} {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') {δ' : W.SurvivingFlag i j} : δ' ∈ { flags := s', pairing_mem := hc' }.boundaryFlags ↔ ↑δ' ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags

Boundary-flag correspondence (open case): a surviving flag is a boundary flag of the glued subset iff its value is a boundary flag of the lifted subset. (The two cut flags are not surviving, so this is the lifted boundary minus the cut flags.)

theorem RS.EdgeSubset.boundary_val_of_glueOpen {α : Type} {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') {δ' : W.SurvivingFlag i j} (hδ' : δ' ∈ { flags := s', pairing_mem := hc' }.boundaryFlags) : ↑δ' ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags

Forward direction of the correspondence, val form.

theorem RS.EdgeSubset.boundary_mk_of_glueOpen {α : Type} {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') {f : W.Flag} (hf : f ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (h1 : f ≠ W.boundaryFlag i) (h2 : f ≠ W.boundaryFlag j) : ⟨f, ⋯⟩ ∈ { flags := s', pairing_mem := hc' }.boundaryFlags

Backward direction of the correspondence, mk form.

The chord-diagram corollary

The pathMatch glue transport

The boundary-chain matching of a glued (open-cut) system at a surviving boundary flag: the original chain when it avoids the cut, and the through-composition with the far side's chain when it hits either cut end — the tower-side engine of the joint- matching invariant.

theorem RS.iterWalk_glueOpen_from {α : Type} {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') (κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem) {g' : W.SurvivingFlag i j} {g : W.Flag} (hg : ↑g' = g) (hgs : g' ∈ s') (n : ℕ) (hcont : ∀ m < n, W.pairing (EdgeSubset.iterWalk κ g m) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (k : ℕ) : k ≤ n → ↑(EdgeSubset.iterWalk (EdgeSubset.RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) g' k) = EdgeSubset.iterWalk κ g k ∧ EdgeSubset.iterWalk (EdgeSubset.RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) g' k ∈ s'

Walk agreement from a corresponding pair of starting flags: while the base walk's pairings stay internal, the glued walk projects to it and stays in the subset.

theorem RS.boundary_mk_of_glueOpen {α : Type} {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') {f' : W.SurvivingFlag i j} (hfs : f' ∈ s') (hbd : ↑f' ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) : f' ∈ { flags := s', pairing_mem := hc' }.boundaryFlags

A surviving flag over a lifted boundary flag is a glued boundary flag.

theorem RS.boundary_val_of_glueOpen {α : Type} {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') {f' : W.SurvivingFlag i j} (hbd : f' ∈ { flags := s', pairing_mem := hc' }.boundaryFlags) : ↑f' ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags

A glued boundary flag lies over a lifted boundary flag.

theorem RS.pathMatch_exit_unique {α' : Type} {W' : Fragment α'} {F : EdgeSubset W'} (κ : F.RelTransitionSystem) {b : W'.Flag} (hb : b ∈ F.boundaryFlags) (N : ℕ) (hcontN : ∀ m < N, W'.pairing (EdgeSubset.iterWalk κ b m) ∈ F.internalFlags) (htermN : W'.pairing (EdgeSubset.iterWalk κ b N) ∈ F.boundaryFlags) : κ.pathMatch b hb = W'.pairing (EdgeSubset.iterWalk κ b N)

Exit-time uniqueness: any explicitly exhibited chain walk computes the path matching — the chain's exit step is unique, so no fuel bookkeeping is needed.

theorem RS.pathMatch_glueOpen_of_ne {α : Type} {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') (κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem) {b' : W.SurvivingFlag i j} (hbg : b' ∈ { flags := s', pairing_mem := hc' }.boundaryFlags) (hbl : ↑b' ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (hni : κ.pathMatch (↑b') hbl ≠ W.boundaryFlag i) (hnj : κ.pathMatch (↑b') hbl ≠ W.boundaryFlag j) : ↑((EdgeSubset.RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).pathMatch b' hbg) = κ.pathMatch (↑b') hbl

pathMatch through an open glue, no cut hit: when the original chain's endpoint avoids both cut flags, the glued chain has the same endpoint.

theorem RS.pathMatch_glueOpen_hit_i {α : Type} {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') (κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem) {b' : W.SurvivingFlag i j} (hbg : b' ∈ { flags := s', pairing_mem := hc' }.boundaryFlags) (hbl : ↑b' ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (hbfj : W.boundaryFlag j ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (hhit : κ.pathMatch (↑b') hbl = W.boundaryFlag i) : ↑((EdgeSubset.RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).pathMatch b' hbg) = κ.pathMatch (W.boundaryFlag j) hbfj

pathMatch through an open glue, i-cut hit: when the original chain from a surviving boundary flag ends at the i-cut flag, the glued chain continues through the cut and ends at the j-side chain's endpoint.

theorem RS.pathMatch_glueOpen_hit_j {α : Type} {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') (κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem) {b' : W.SurvivingFlag i j} (hbg : b' ∈ { flags := s', pairing_mem := hc' }.boundaryFlags) (hbl : ↑b' ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (hbfi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (hhit : κ.pathMatch (↑b') hbl = W.boundaryFlag j) : ↑((EdgeSubset.RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).pathMatch b' hbg) = κ.pathMatch (W.boundaryFlag i) hbfi

pathMatch through an open glue, j-cut hit: when the original chain from a surviving boundary flag ends at the j-cut flag, the glued chain continues through the cut and ends at the i-side chain's endpoint.

theorem RS.glued_participation_iff {α : Type} {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') (l : Fragment.SurvivingLabel α i j) : (W.gluePairOpen i j hij hopen).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags ↔ W.boundaryFlag ↑l ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags

Participation transports through the open glue at label level.