Transport of transition data across a single-pair glue

For W' := W.gluePair i j hij (in either the open or the closed case) the internal flags of a glued edge subset EdgeSubset.mk s' correspond to the internal flags of the lifted edge subset (liftSubsetOpen / liftSubsetClosed) via Subtype.val: gluing touches only the two boundary flags, and internal flags are attached to vertices.

Along this correspondence we transport boundary-relative transition systems (RelTransitionSystem.unglueOpen/glueOpen, unglueClosed/glueClosed) and their orientations in both directions, prove the round trips on match_ pointwise at internal flags, relate the walk steps (iterWalk-style match_ ∘ pairing) away from the glued interface, record the exact rewired step at the interface (what the circuit-count delta of GlueCircuitDelta.lean reads), and prove that openCircuitCount is stable under the transport when the glued edge's flags do not participate.

Rewire evaluation lemmas

theorem RS.Fragment.rewire_val_of_ne {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f : W.SurvivingFlag i j) (h1 : W.pairing ↑f ≠ W.boundaryFlag i) (h2 : W.pairing ↑f ≠ W.boundaryFlag j) : ↑(rewire hopen f) = W.pairing ↑f

Away from the glued interface, rewire agrees with the original pairing.

theorem RS.Fragment.rewire_eq_partnerSurvJ {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f : W.SurvivingFlag i j) (h : W.pairing ↑f = W.boundaryFlag i) : rewire hopen f = partnerSurvJ hopen

At the i-side of the interface, rewire jumps to the far end of the j-edge.

theorem RS.Fragment.rewire_eq_partnerSurvI {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f : W.SurvivingFlag i j) (hne : W.pairing ↑f ≠ W.boundaryFlag i) (h : W.pairing ↑f = W.boundaryFlag j) : rewire hopen f = partnerSurvI hopen

At the j-side of the interface, rewire jumps to the far end of the i-edge.

theorem RS.Fragment.eq_partnerSurvI_of_pairing {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f : W.SurvivingFlag i j) (h : W.pairing ↑f = W.boundaryFlag i) : f = partnerSurvI hopen

A surviving flag whose pairing is the i-boundary flag is the far end of the i-edge.

theorem RS.Fragment.eq_partnerSurvJ_of_pairing {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f : W.SurvivingFlag i j) (h : W.pairing ↑f = W.boundaryFlag j) : f = partnerSurvJ hopen

A surviving flag whose pairing is the j-boundary flag is the far end of the j-edge.

Generic transport helpers

theorem RS.EdgeSubset.internal_surviving {α : Type} {W : Fragment α} (i j : α) {F : EdgeSubset W} {f : W.Flag} (hf : f ∈ F.internalFlags) : f ≠ W.boundaryFlag i ∧ f ≠ W.boundaryFlag j

An internal flag of any edge subset of W survives a glue at {i, j}: it is attached to a vertex, hence is no boundary flag.

noncomputable def RS.EdgeSubset.unglueMatch {α : Type} {W : Fragment α} {i j : α} (m : W.SurvivingFlag i j → W.SurvivingFlag i j) (f : W.Flag) : W.Flag

Extend a surviving-flag self-map to all of W.Flag: apply it through the subtype on surviving flags, identity elsewhere.

Equations

• RS.EdgeSubset.unglueMatch m f = if h : f ≠ W.boundaryFlag i ∧ f ≠ W.boundaryFlag j then ↑(m ⟨f, h⟩) else f

theorem RS.EdgeSubset.unglueMatch_of_surviving {α : Type} {W : Fragment α} {i j : α} (m : W.SurvivingFlag i j → W.SurvivingFlag i j) (f : W.Flag) (h : f ≠ W.boundaryFlag i ∧ f ≠ W.boundaryFlag j) : unglueMatch m f = ↑(m ⟨f, h⟩)

The unglued matching at a surviving flag is the glued matching read through Subtype.val.

theorem RS.EdgeSubset.unglueMatch_val {α : Type} {W : Fragment α} {i j : α} (m : W.SurvivingFlag i j → W.SurvivingFlag i j) (g : W.SurvivingFlag i j) : unglueMatch m ↑g = ↑(m g)

The same, stated on a surviving flag's underlying flag.

noncomputable def RS.EdgeSubset.glueMatch {α : Type} {W : Fragment α} {i j : α} (m : W.Flag → W.Flag) (P : Finset (W.SurvivingFlag i j)) (hP : ∀ f' ∈ P, m ↑f' ≠ W.boundaryFlag i ∧ m ↑f' ≠ W.boundaryFlag j) (f' : W.SurvivingFlag i j) : W.SurvivingFlag i j

Restrict a flag self-map of W to the surviving flags on a given internal-flag set: apply it through Subtype.val there (with a supplied surviving-ness certificate), identity elsewhere.

Equations

• RS.EdgeSubset.glueMatch m P hP f' = if h : f' ∈ P then ⟨m ↑f', ⋯⟩ else f'

theorem RS.EdgeSubset.glueMatch_val_of_mem {α : Type} {W : Fragment α} {i j : α} (m : W.Flag → W.Flag) (P : Finset (W.SurvivingFlag i j)) (hP : ∀ f' ∈ P, m ↑f' ≠ W.boundaryFlag i ∧ m ↑f' ≠ W.boundaryFlag j) {f' : W.SurvivingFlag i j} (h : f' ∈ P) : ↑(glueMatch m P hP f') = m ↑f'

The glued matching on the flags it is defined at agrees with the matching it came from.

noncomputable def RS.EdgeSubset.unglueIsOut {α : Type} {W : Fragment α} {i j : α} (b : W.SurvivingFlag i j → Bool) (f : W.Flag) : Bool

Extend a surviving-flag orientation to all of W.Flag: through the subtype on surviving flags, false elsewhere.

Equations

• RS.EdgeSubset.unglueIsOut b f = if h : f ≠ W.boundaryFlag i ∧ f ≠ W.boundaryFlag j then b ⟨f, h⟩ else false

theorem RS.EdgeSubset.unglueIsOut_of_surviving {α : Type} {W : Fragment α} {i j : α} (b : W.SurvivingFlag i j → Bool) (f : W.Flag) (h : f ≠ W.boundaryFlag i ∧ f ≠ W.boundaryFlag j) : unglueIsOut b f = b ⟨f, h⟩

The unglued orientation at a surviving flag.

theorem RS.EdgeSubset.unglueIsOut_val {α : Type} {W : Fragment α} {i j : α} (b : W.SurvivingFlag i j → Bool) (g : W.SurvivingFlag i j) : unglueIsOut b ↑g = b g

The same, stated on a surviving flag's underlying flag.

The open case

Internal-flag correspondence (open case)

theorem RS.EdgeSubset.mem_internalFlags_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} : f' ∈ { flags := s', pairing_mem := hc' }.internalFlags ↔ ↑f' ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags

Internal-flag correspondence (open case): the internal flags of the glued subset and of the lifted subset correspond via Subtype.val.

theorem RS.EdgeSubset.internal_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} (hf' : f' ∈ { flags := s', pairing_mem := hc' }.internalFlags) : ↑f' ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags

Forward direction of the correspondence, val form.

theorem RS.EdgeSubset.internal_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 }.internalFlags) (h1 : f ≠ W.boundaryFlag i) (h2 : f ≠ W.boundaryFlag j) : ⟨f, ⋯⟩ ∈ { flags := s', pairing_mem := hc' }.internalFlags

Backward direction of the correspondence, mk form.

Transition transport (open case)

noncomputable def RS.EdgeSubset.RelTransitionSystem.unglueOpen {α : 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 := s', pairing_mem := hc' }.RelTransitionSystem) : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem

Unglue (open case): transport a transition system on the glued subset to the lifted subset. The matching acts through the surviving-flag subtype; identity junk at the two glued boundary flags.

Equations

• RS.EdgeSubset.RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ' = { match_ := RS.EdgeSubset.unglueMatch κ'.match_, match_invol := ⋯, match_ne := ⋯, match_mem := ⋯, match_vertex := ⋯ }

theorem RS.EdgeSubset.unglueOpen_match_of_surviving {α : 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 := s', pairing_mem := hc' }.RelTransitionSystem) (f : W.Flag) (h : f ≠ W.boundaryFlag i ∧ f ≠ W.boundaryFlag j) : (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').match_ f = ↑(κ'.match_ ⟨f, h⟩)

The open ungluing's matching at a surviving flag.

theorem RS.EdgeSubset.unglueOpen_match_val {α : 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 := s', pairing_mem := hc' }.RelTransitionSystem) (g : W.SurvivingFlag i j) : (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').match_ ↑g = ↑(κ'.match_ g)

The same on a surviving flag's underlying flag.

theorem RS.EdgeSubset.glueOpen_cert {α : 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) (f' : (W.gluePairOpen i j hij hopen).Flag) : f' ∈ { flags := s', pairing_mem := hc' }.internalFlags → κ.match_ ↑f' ≠ W.boundaryFlag i ∧ κ.match_ ↑f' ≠ W.boundaryFlag j

The surviving-ness certificate for restricting a lifted-side matching to the glued subset.

noncomputable def RS.EdgeSubset.RelTransitionSystem.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') (κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem) : { flags := s', pairing_mem := hc' }.RelTransitionSystem

Glue (open case): restrict a transition system on the lifted subset to the glued subset.

Equations

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

theorem RS.EdgeSubset.glueOpen_match_val {α : 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) {f' : W.SurvivingFlag i j} (hf' : f' ∈ { flags := s', pairing_mem := hc' }.internalFlags) : ↑((RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).match_ f') = κ.match_ ↑f'

The open gluing's matching at an internal flag: the round trip agrees with the system it started from.

Round trips (open case)

theorem RS.EdgeSubset.unglueOpen_glueOpen_match {α : 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) {f : W.Flag} (hf : f ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) : (RelTransitionSystem.unglueOpen hij hopen s' hc' hc (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ)).match_ f = κ.match_ f

Round trip lifted → glued → lifted: match_ agrees pointwise at internal flags.

Orientation transport (open case)

noncomputable def RS.EdgeSubset.unglueOrientationOpen {α : 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 := s', pairing_mem := hc' }.RelTransitionSystem) (o' : κ'.Orientation) : (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').Orientation

Unglue an orientation (open case): through the subtype on surviving flags, false junk at the two glued boundary flags (which are never internal, so the structure fields do not constrain them).

Equations

• RS.EdgeSubset.unglueOrientationOpen hij hopen s' hc' hc κ' o' = { isOut := RS.EdgeSubset.unglueIsOut o'.isOut, match_flip := ⋯, pairing_flip := ⋯ }

noncomputable def RS.EdgeSubset.glueOrientationOpen {α : 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) (o : κ.Orientation) (hcompat : o.isOut (W.pairing (W.boundaryFlag j)) = !o.isOut (W.pairing (W.boundaryFlag i))) : (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).Orientation

Glue an orientation (open case): through Subtype.val. The rewired pairing crosses the interface, so a flip-compatibility hypothesis between the two far ends is required (it is vacuous when the interface edges do not participate).

Equations

• RS.EdgeSubset.glueOrientationOpen hij hopen s' hc' hc κ o hcompat = { isOut := fun (f' : (W.gluePairOpen i j hij hopen).Flag) => o.isOut ↑f', match_flip := ⋯, pairing_flip := ⋯ }

Walk-step agreement (open case)

theorem RS.EdgeSubset.gluePairOpen_pairing_val_of_ne {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f' : W.SurvivingFlag i j) (h1 : W.pairing ↑f' ≠ W.boundaryFlag i) (h2 : W.pairing ↑f' ≠ W.boundaryFlag j) : ↑((W.gluePairOpen i j hij hopen).pairing f') = W.pairing ↑f'

The glued pairing at projection level, away from the interface.

theorem RS.EdgeSubset.glueOpen_step_agrees {α : 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) (f' : W.SurvivingFlag i j) (hp : W.pairing ↑f' ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) : ↑((RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).match_ ((W.gluePairOpen i j hij hopen).pairing f')) = κ.match_ (W.pairing ↑f')

Walk-step agreement (open case, glue direction): when the lifted pairing target is internal, the glued walk step projects to the lifted walk step.

The interface (open case): the rewired step

theorem RS.EdgeSubset.gluePairOpen_pairing_interface_i {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f' : W.SurvivingFlag i j) (h : W.pairing ↑f' = W.boundaryFlag i) : (W.gluePairOpen i j hij hopen).pairing f' = Fragment.partnerSurvJ hopen

The glued pairing at the i-side of the interface, projection level.

theorem RS.EdgeSubset.gluePairOpen_pairing_interface_j {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (f' : W.SurvivingFlag i j) (hne : W.pairing ↑f' ≠ W.boundaryFlag i) (h : W.pairing ↑f' = W.boundaryFlag j) : (W.gluePairOpen i j hij hopen).pairing f' = Fragment.partnerSurvI hopen

The glued pairing at the j-side of the interface, projection level.

openCircuitCount stability (open case, interface not in

the subset)

theorem RS.EdgeSubset.partnerSurvJ_notMem_of {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') : Fragment.partnerSurvJ hopen ∉ s'

When the far end of the i-edge is absent, so is the far end of the j-edge (by closure under the glued pairing).

theorem RS.EdgeSubset.gluePairOpen_pairing_val_of_notMem_interface {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') {g : W.SurvivingFlag i j} (hg : g ∈ s') : ↑((W.gluePairOpen i j hij hopen).pairing g) = W.pairing ↑g

When the interface is not in the subset, the glued pairing agrees with the W-pairing on all subset flags.

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

Walk correspondence (glued-side continuation data): the lifted walk is the projection of the glued walk, and the glued iterates stay internal.

theorem RS.EdgeSubset.iterWalk_unglueOpen_rev {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) {g : W.SurvivingFlag i j} (hg : g ∈ { flags := s', pairing_mem := hc' }.internalFlags) (n : ℕ) (hcontW : ∀ m < n, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (↑g) m) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (k : ℕ) : k ≤ n → iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (↑g) k = ↑(iterWalk κ' g k) ∧ iterWalk κ' g k ∈ { flags := s', pairing_mem := hc' }.internalFlags ∧ (k < n → (W.gluePairOpen i j hij hopen).pairing (iterWalk κ' g k) ∈ { flags := s', pairing_mem := hc' }.internalFlags)

Walk correspondence (lifted-side continuation data): the converse bookkeeping, with the glued pairing-internality reconstructed step by step.

theorem RS.EdgeSubset.periodicFlags_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') (hni : Fragment.partnerSurvI hopen ∉ s') (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) {g : W.SurvivingFlag i j} (hg : g ∈ κ'.periodicFlags) : ↑g ∈ (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').periodicFlags

Periodic flags project forward along the unglue transport.

theorem RS.EdgeSubset.periodicFlags_of_val_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') (hni : Fragment.partnerSurvI hopen ∉ s') (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) {g : W.SurvivingFlag i j} (hf : ↑g ∈ (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').periodicFlags) : g ∈ κ'.periodicFlags

Periodic flags lift backward along the unglue transport.

noncomputable def RS.EdgeSubset.periodicEquivGlueOpen {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) : ↥(RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').periodicFlags ≃ ↥κ'.periodicFlags

The val-bijection between the periodic flags of the two sides.

Equations

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

theorem RS.EdgeSubset.walkPermPeriodic_unglueOpen {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) : (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').walkPermPeriodic = (periodicEquivGlueOpen hij hopen s' hc' hc hni κ').symm.permCongr κ'.walkPermPeriodic

The walk permutations on periodic flags agree under the val-bijection.

theorem RS.EdgeSubset.openCircuitCount_unglueOpen {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) : (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').openCircuitCount = κ'.openCircuitCount

openCircuitCount stability (open case): when the glued edge's flags are not in the subset, the open circuit count is unchanged by the unglue transport.

The closed case

theorem RS.EdgeSubset.pairing_val_surviving_closed {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (f' : W.SurvivingFlag i j) : W.pairing ↑f' ≠ W.boundaryFlag i ∧ W.pairing ↑f' ≠ W.boundaryFlag j

In the closed case the pairing of a surviving flag is itself surviving: the closed-off edge pairs its two boundary flags with each other.

theorem RS.EdgeSubset.gluePairClosed_pairing_val {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (f' : W.SurvivingFlag i j) : ↑((W.gluePairClosed i j hclosed).pairing f') = W.pairing ↑f'

In the closed case the glued pairing agrees with the W-pairing on all surviving flags, at projection level.

Internal-flag correspondence (closed case)

theorem RS.EdgeSubset.mem_internalFlags_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' }.internalFlags ↔ ↑f' ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.internalFlags

Internal-flag correspondence (closed case).

theorem RS.EdgeSubset.internal_val_of_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} (hf' : f' ∈ { flags := s', pairing_mem := hc' }.internalFlags) : ↑f' ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.internalFlags

Forward direction of the correspondence, val form.

theorem RS.EdgeSubset.internal_mk_of_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.Flag} (hf : f ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.internalFlags) (h1 : f ≠ W.boundaryFlag i) (h2 : f ≠ W.boundaryFlag j) : ⟨f, ⋯⟩ ∈ { flags := s', pairing_mem := hc' }.internalFlags

Backward direction of the correspondence, mk form.

Transition transport (closed case)

noncomputable def RS.EdgeSubset.RelTransitionSystem.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) : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.RelTransitionSystem

Unglue (closed case): transport a transition system on the glued subset to the lifted subset.

Equations

• RS.EdgeSubset.RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ' = { match_ := RS.EdgeSubset.unglueMatch κ'.match_, match_invol := ⋯, match_ne := ⋯, match_mem := ⋯, match_vertex := ⋯ }

theorem RS.EdgeSubset.unglueClosed_match_of_surviving {α : 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) (f : W.Flag) (h : f ≠ W.boundaryFlag i ∧ f ≠ W.boundaryFlag j) : (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ').match_ f = ↑(κ'.match_ ⟨f, h⟩)

The closed ungluing's matching at a surviving flag.

theorem RS.EdgeSubset.unglueClosed_match_val {α : 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) (g : W.SurvivingFlag i j) : (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ').match_ ↑g = ↑(κ'.match_ g)

The same on a surviving flag's underlying flag.

theorem RS.EdgeSubset.glueClosed_cert {α : 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 := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.RelTransitionSystem) (f' : (W.gluePairClosed i j hclosed).Flag) : f' ∈ { flags := s', pairing_mem := hc' }.internalFlags → κ.match_ ↑f' ≠ W.boundaryFlag i ∧ κ.match_ ↑f' ≠ W.boundaryFlag j

The surviving-ness certificate for restricting a lifted-side matching to the glued subset (closed case).

noncomputable def RS.EdgeSubset.RelTransitionSystem.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) (κ : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.RelTransitionSystem) : { flags := s', pairing_mem := hc' }.RelTransitionSystem

Glue (closed case): restrict a transition system on the lifted subset to the glued subset.

Equations

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

theorem RS.EdgeSubset.glueClosed_match_val {α : 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 := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.RelTransitionSystem) {f' : W.SurvivingFlag i j} (hf' : f' ∈ { flags := s', pairing_mem := hc' }.internalFlags) : ↑((RelTransitionSystem.glueClosed hclosed b s' hc' hc κ).match_ f') = κ.match_ ↑f'

The closed gluing's matching at an internal flag: the round trip again agrees.

Round trips (closed case)

theorem RS.EdgeSubset.unglueClosed_glueClosed_match {α : 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 := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.RelTransitionSystem) {f : W.Flag} (hf : f ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.internalFlags) : (RelTransitionSystem.unglueClosed hclosed b s' hc' hc (RelTransitionSystem.glueClosed hclosed b s' hc' hc κ)).match_ f = κ.match_ f

Round trip lifted → glued → lifted: match_ agrees pointwise at internal flags.

Orientation transport (closed case)

noncomputable def RS.EdgeSubset.unglueOrientationClosed {α : 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) (o' : κ'.Orientation) : (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ').Orientation

Unglue an orientation (closed case): through the subtype, false junk at the two glued boundary flags.

Equations

• RS.EdgeSubset.unglueOrientationClosed hclosed b s' hc' hc κ' o' = { isOut := RS.EdgeSubset.unglueIsOut o'.isOut, match_flip := ⋯, pairing_flip := ⋯ }

noncomputable def RS.EdgeSubset.glueOrientationClosed {α : 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 := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.RelTransitionSystem) (o : κ.Orientation) : (RelTransitionSystem.glueClosed hclosed b s' hc' hc κ).Orientation

Glue an orientation (closed case): through Subtype.val. Unconditional: the closed glued pairing agrees with the W-pairing on surviving flags.

Equations

• RS.EdgeSubset.glueOrientationClosed hclosed b s' hc' hc κ o = { isOut := fun (f' : (W.gluePairClosed i j hclosed).Flag) => o.isOut ↑f', match_flip := ⋯, pairing_flip := ⋯ }

openCircuitCount stability (closed case)

theorem RS.EdgeSubset.iterWalk_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) {g : W.SurvivingFlag i j} (hg : g ∈ { flags := s', pairing_mem := hc' }.internalFlags) (n : ℕ) (hcont : ∀ m < n, (W.gluePairClosed i j hclosed).pairing (iterWalk κ' g m) ∈ { flags := s', pairing_mem := hc' }.internalFlags) (k : ℕ) : k ≤ n → iterWalk (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ') (↑g) k = ↑(iterWalk κ' g k) ∧ iterWalk κ' g k ∈ { flags := s', pairing_mem := hc' }.internalFlags

Walk correspondence (glued-side continuation data), closed case.

theorem RS.EdgeSubset.iterWalk_unglueClosed_rev {α : 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) {g : W.SurvivingFlag i j} (hg : g ∈ { flags := s', pairing_mem := hc' }.internalFlags) (n : ℕ) (hcontW : ∀ m < n, W.pairing (iterWalk (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ') (↑g) m) ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.internalFlags) (k : ℕ) : k ≤ n → iterWalk (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ') (↑g) k = ↑(iterWalk κ' g k) ∧ iterWalk κ' g k ∈ { flags := s', pairing_mem := hc' }.internalFlags ∧ (k < n → (W.gluePairClosed i j hclosed).pairing (iterWalk κ' g k) ∈ { flags := s', pairing_mem := hc' }.internalFlags)

Walk correspondence (lifted-side continuation data), closed case.

theorem RS.EdgeSubset.periodicFlags_val_of_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) (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) {g : W.SurvivingFlag i j} (hg : g ∈ κ'.periodicFlags) : ↑g ∈ (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ').periodicFlags

Periodic flags project forward along the unglue transport (closed case).

theorem RS.EdgeSubset.periodicFlags_of_val_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) (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) {g : W.SurvivingFlag i j} (hf : ↑g ∈ (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ').periodicFlags) : g ∈ κ'.periodicFlags

Periodic flags lift backward along the unglue transport (closed case).

noncomputable def RS.EdgeSubset.periodicEquivGlueClosed {α : 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) : ↥(RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ').periodicFlags ≃ ↥κ'.periodicFlags

The val-bijection between the periodic flags of the two sides (closed case).

Equations

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

theorem RS.EdgeSubset.walkPermPeriodic_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) : (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ').walkPermPeriodic = (periodicEquivGlueClosed hclosed b s' hc' hc κ').symm.permCongr κ'.walkPermPeriodic

The walk permutations on periodic flags agree under the val-bijection (closed case).

theorem RS.EdgeSubset.openCircuitCount_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) : (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ').openCircuitCount = κ'.openCircuitCount

openCircuitCount stability (closed case): the open circuit count is unchanged by the unglue transport, for either value of b (the closed-off circle-edge is boundary-attached in W and never periodic).