Circuit-count delta across a participating glued interface

GlueRelTransport proved openCircuitCount stability for the open single-pair glue when the glued edge's flags do not participate in the edge subset. This file treats the participating case: the lifted subset contains both boundary flags bf_i, bf_j of W, which are boundary flags of the lifted edge subset, so the W-side walks terminate there, while the glued walk continues through the rewire.

Main results

• pairing_iterWalk_ne — the master collision lemma: along any walk with internal pairings, W.pairing (iterWalk κ b m) never equals iterWalk κ b l (a parity argument on the alternating chain); specialised to pathMatch_ne_self (the path matching has no fixed points).
• InterfaceLinked — the two interface chains splice into a closed circuit: pathMatch of bf_i is bf_j.
• openCircuitCount_linked_chain, openCircuitCount_glueOpen_participating — the circuit-count delta: gluing adds exactly one circuit when the interface is linked and none otherwise.

Permutation counting helpers: sumCongr

theorem RS.finRotate_orbit_count (k : ℕ) (hk : 1 ≤ k) : (finRotate k).cycleType.card + Fintype.card ↑(Function.fixedPoints ⇑(finRotate k)) = 1

A rotation of length k ≥ 1 contributes exactly one orbit: one nontrivial cycle when k ≥ 2, one fixed point when k = 1.

Generic walk lemmas

theorem RS.EdgeSubset.periodicFlag_iterWalk {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : κ.PeriodicFlag f) (m : ℕ) : κ.PeriodicFlag (iterWalk κ f m)

Iterates of a periodic flag are periodic.

theorem RS.EdgeSubset.iterWalk_mod {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} {n : ℕ} (hper : iterWalk κ f n = f) (a : ℕ) : iterWalk κ f a = iterWalk κ f (a % n)

Reduce a walk index modulo a period.

theorem RS.EdgeSubset.pairing_iterWalk_ne {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} {k : ℕ} (hcont : ∀ t < k, W.pairing (iterWalk κ b t) ∈ F.internalFlags) {m l : ℕ} (hm : m ≤ k) (hl : l ≤ k) : W.pairing (iterWalk κ b m) ≠ iterWalk κ b l

Master collision lemma: along a walk whose pairings up to step k are internal, the pairing of an iterate never equals an iterate (parity argument on the alternating chain: a collision would force a fixed point of the edge pairing or of the matching).

theorem RS.EdgeSubset.RelTransitionSystem.pathMatch_ne_self {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) : κ.pathMatch b hb ≠ b

The path matching has no fixed points.

theorem RS.EdgeSubset.RelTransitionSystem.pathMatch_congr {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b b' : W.Flag} (h : b = b') (hb : b ∈ F.boundaryFlags) (hb' : b' ∈ F.boundaryFlags) : κ.pathMatch b hb = κ.pathMatch b' hb'

Congruence for pathMatch in its base point.

theorem RS.EdgeSubset.not_periodic_of_chain_segment {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} {k : ℕ} (hcont : ∀ t < k, W.pairing (iterWalk κ b t) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ b k) ∈ F.boundaryFlags) {m : ℕ} (hmk : m ≤ k) : ¬κ.PeriodicFlag (iterWalk κ b m)

Flags along a boundary-terminated chain segment are not periodic.

The participating open glue

Interface membership

theorem RS.EdgeSubset.partnerSurvJ_mem_of_mem {α : 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') (hpi : Fragment.partnerSurvI hopen ∈ s') : Fragment.partnerSurvJ hopen ∈ s'

Participation propagates to the far end of the j-edge.

theorem RS.EdgeSubset.boundaryFlagI_mem_boundaryFlags {α : 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 ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s') (hpi : Fragment.partnerSurvI hopen ∈ s') : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags

With participation, bf_i is a boundary flag of the lift.

theorem RS.EdgeSubset.boundaryFlagJ_mem_boundaryFlags {α : 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') (hpi : Fragment.partnerSurvI hopen ∈ s') : W.boundaryFlag j ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags

With participation, bf_j is a boundary flag of the lift.

Walk correspondence

theorem RS.EdgeSubset.iterWalk_val_of_glued_avoids {α : 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) (n : ℕ) (hav : ∀ t < n, iterWalk κ' g t ≠ Fragment.partnerSurvI hopen ∧ iterWalk κ' g t ≠ Fragment.partnerSurvJ hopen) (m : ℕ) : m ≤ n → iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (↑g) m = ↑(iterWalk κ' g m)

Walk correspondence from glued-side interface avoidance.

theorem RS.EdgeSubset.iterWalk_val_of_internal {α : 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) (n : ℕ) (hcontW : ∀ t < n, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (↑g) t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (m : ℕ) : m ≤ n → iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (↑g) m = ↑(iterWalk κ' g m)

Walk correspondence from lifted-side internality data.

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

Under lifted-side internality, the glued pairings along the walk are internal.

Periodic-flag transport

theorem RS.EdgeSubset.mem_periodicFlags_glued_of_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} (hg : ↑g ∈ (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').periodicFlags) : g ∈ κ'.periodicFlags

Periodic flags lift backward along the unglue transport (participating case: internality of the lifted-side pairings keeps the walk away from the interface).

theorem RS.EdgeSubset.periodicFlag_val_or_orbit {α : 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} (hg : g ∈ κ'.periodicFlags) : ↑g ∈ (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').periodicFlags ∨ (κ'.PeriodicFlag (Fragment.partnerSurvI hopen) ∧ ∃ (c : ℕ), iterWalk κ' (Fragment.partnerSurvI hopen) c = g) ∨ κ'.PeriodicFlag (Fragment.partnerSurvJ hopen) ∧ ∃ (c : ℕ), iterWalk κ' (Fragment.partnerSurvJ hopen) c = g

Classification of glued periodic flags: either the value is periodic on the lifted side, or the flag lies on the orbit of one of the two interface far ends.

Exit forced to the interface

theorem RS.EdgeSubset.pathMatch_mem_interface_of_glued_internal {α : 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) {b : W.Flag} (hb : b ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (h1 : W.pairing b ≠ W.boundaryFlag i) (h2 : W.pairing b ≠ W.boundaryFlag j) (h0 : ⟨W.pairing b, ⋯⟩ ∈ { flags := s', pairing_mem := hc' }.internalFlags) (hz : ∀ (t : ℕ), (W.gluePairOpen i j hij hopen).pairing (iterWalk κ' (κ'.match_ ⟨W.pairing b, ⋯⟩) t) ∈ { flags := s', pairing_mem := hc' }.internalFlags) : (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').pathMatch b hb = W.boundaryFlag i ∨ (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').pathMatch b hb = W.boundaryFlag j

If the glued walk entering the chain of a boundary flag b has all its pairings internal, the W-side chain from b must exit at the glued interface.

The link condition

def RS.EdgeSubset.InterfaceLinked {α : 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) (hpi : Fragment.partnerSurvI hopen ∈ s') : Prop

The interface link condition: the W-side chain from bf_i (under the unglued transition data) exits at bf_j. When it holds, gluing splices the two interface chains into one new closed circuit; otherwise it concatenates two boundary paths.

Equations

• RS.EdgeSubset.InterfaceLinked hij hopen s' hc' hc κ' hpi = ((RS.EdgeSubset.RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').pathMatch (W.boundaryFlag i) ⋯ = W.boundaryFlag j)

theorem RS.EdgeSubset.interfaceLinked_iff_pathMatch {α : 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) (hpi : Fragment.partnerSurvI hopen ∈ s') : InterfaceLinked hij hopen s' hc' hc κ' hpi ↔ (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').pathMatch (W.boundaryFlag i) ⋯ = W.boundaryFlag j

Feed-forward form of the link condition: it is literally the pathMatch pairing of the two interface boundary flags.

theorem RS.EdgeSubset.interfaceLinked_of_periodicI {α : 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) (hpi : Fragment.partnerSurvI hopen ∈ s') (hper : κ'.PeriodicFlag (Fragment.partnerSurvI hopen)) : InterfaceLinked hij hopen s' hc' hc κ' hpi

If the far end of the i-edge is periodic in the glued system, the interface is linked.

theorem RS.EdgeSubset.interfaceLinked_of_periodicJ {α : 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) (hpi : Fragment.partnerSurvI hopen ∈ s') (hper : κ'.PeriodicFlag (Fragment.partnerSurvJ hopen)) : InterfaceLinked hij hopen s' hc' hc κ' hpi

If the far end of the j-edge is periodic in the glued system, the interface is linked.

The unlinked case: counts agree

noncomputable def RS.EdgeSubset.periodicEquivNotLinked {α : 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) (hpi : Fragment.partnerSurvI hopen ∈ s') (hnl : ¬InterfaceLinked hij hopen s' hc' hc κ' hpi) : ↥(RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').periodicFlags ≃ ↥κ'.periodicFlags

The periodic-flag bijection in the unlinked participating case.

Equations

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

theorem RS.EdgeSubset.walkPermPeriodic_notLinked {α : 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) (hpi : Fragment.partnerSurvI hopen ∈ s') (hnl : ¬InterfaceLinked hij hopen s' hc' hc κ' hpi) : (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').walkPermPeriodic = (periodicEquivNotLinked hij hopen s' hc' hc κ' hpi hnl).symm.permCongr κ'.walkPermPeriodic

The walk permutations agree under the bijection (unlinked case).

theorem RS.EdgeSubset.openCircuitCount_notLinked {α : 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) (hpi : Fragment.partnerSurvI hopen ∈ s') (hnl : ¬InterfaceLinked hij hopen s' hc' hc κ' hpi) : (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').openCircuitCount = κ'.openCircuitCount

Count stability in the unlinked case.

The spliced interface cycle

theorem RS.EdgeSubset.splice_x_internal {α : 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) (x : W.SurvivingFlag i j) (b : W.Flag) (hxb : ↑x = W.pairing b) (k : ℕ) (hk1 : 1 ≤ k) (hcont : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) : x ∈ { flags := s', pairing_mem := hc' }.internalFlags

The near end of the entry edge is internal in the glued subset.

theorem RS.EdgeSubset.splice_entry_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) (x : W.SurvivingFlag i j) (b : W.Flag) (hxb : ↑x = W.pairing b) : ↑(κ'.match_ x) = (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').match_ (W.pairing b)

The entry value of the spliced walk.

theorem RS.EdgeSubset.splice_walk_valW {α : 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) (x : W.SurvivingFlag i j) (b : W.Flag) (hxb : ↑x = W.pairing b) (t : ℕ) : iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (↑(κ'.match_ x)) t = iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b (t + 1)

The lifted walk from the entry point is the shifted chain.

theorem RS.EdgeSubset.splice_contW {α : 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) (x : W.SurvivingFlag i j) (b : W.Flag) (hxb : ↑x = W.pairing b) (k : ℕ) (hcont : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (t : ℕ) : t < k - 1 → W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (↑(κ'.match_ x)) t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags

The lifted pairings along the shifted chain stay internal.

theorem RS.EdgeSubset.splice_walk_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) (x : W.SurvivingFlag i j) (b : W.Flag) (hxb : ↑x = W.pairing b) (k : ℕ) (hk1 : 1 ≤ k) (hcont : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (t : ℕ) : t < k → ↑(iterWalk κ' (κ'.match_ x) t) = iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b (t + 1)

Cycle values: the glued walk from the entry point follows the W-side chain from b.

theorem RS.EdgeSubset.splice_last {α : 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) (x y : W.SurvivingFlag i j) (b bo : W.Flag) (hxb : ↑x = W.pairing b) (hyo : ↑y = W.pairing bo) (k : ℕ) (hk1 : 1 ≤ k) (hcont : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (hterm : W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b k) = bo) : iterWalk κ' (κ'.match_ x) (k - 1) = y

Exit flag: at step k - 1 the glued walk sits at the far end of the exit edge.

theorem RS.EdgeSubset.splice_period {α : 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) (x y : W.SurvivingFlag i j) (b bo : W.Flag) (hxb : ↑x = W.pairing b) (hyo : ↑y = W.pairing bo) (hryx : (W.gluePairOpen i j hij hopen).pairing y = x) (k : ℕ) (hk1 : 1 ≤ k) (hcont : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (hterm : W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b k) = bo) : iterWalk κ' (κ'.match_ x) k = κ'.match_ x

The wrap: the glued walk closes up with period k.

theorem RS.EdgeSubset.splice_pairing_internal {α : 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) (x y : W.SurvivingFlag i j) (b bo : W.Flag) (hxb : ↑x = W.pairing b) (hyo : ↑y = W.pairing bo) (hryx : (W.gluePairOpen i j hij hopen).pairing y = x) (k : ℕ) (hk1 : 1 ≤ k) (hcont : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (hterm : W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b k) = bo) (t : ℕ) : t < k → (W.gluePairOpen i j hij hopen).pairing (iterWalk κ' (κ'.match_ x) t) ∈ { flags := s', pairing_mem := hc' }.internalFlags

The glued pairings along the spliced cycle are internal.

theorem RS.EdgeSubset.splice_periodicFlag {α : 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) (x y : W.SurvivingFlag i j) (b bo : W.Flag) (hxb : ↑x = W.pairing b) (hyo : ↑y = W.pairing bo) (hryx : (W.gluePairOpen i j hij hopen).pairing y = x) (k : ℕ) (hk1 : 1 ≤ k) (hcont : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (hterm : W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b k) = bo) : κ'.PeriodicFlag (κ'.match_ x)

The spliced cycle is periodic in the glued system.

theorem RS.EdgeSubset.splice_val_not_periodic {α : 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) (x : W.SurvivingFlag i j) (b bo : W.Flag) (hbo : bo ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (hxb : ↑x = W.pairing b) (k : ℕ) (hk1 : 1 ≤ k) (hcont : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (hterm : W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b k) = bo) (t : ℕ) : t < k → ↑(iterWalk κ' (κ'.match_ x) t) ∉ (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').periodicFlags

Cycle values are not periodic on the lifted side.

theorem RS.EdgeSubset.splice_inj {α : 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) (x : W.SurvivingFlag i j) (b : W.Flag) (hb : b ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (hxb : ↑x = W.pairing b) (k : ℕ) (hk1 : 1 ≤ k) (hcont : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (t₁ t₂ : ℕ) : t₁ < k → t₂ < k → iterWalk κ' (κ'.match_ x) t₁ = iterWalk κ' (κ'.match_ x) t₂ → t₁ = t₂

Distinctness along the spliced cycle.

theorem RS.EdgeSubset.splice_mod {α : 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) (x y : W.SurvivingFlag i j) (b bo : W.Flag) (hxb : ↑x = W.pairing b) (hyo : ↑y = W.pairing bo) (hryx : (W.gluePairOpen i j hij hopen).pairing y = x) (k : ℕ) (hk1 : 1 ≤ k) (hcont : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (hterm : W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') b k) = bo) (c : ℕ) : iterWalk κ' (κ'.match_ x) c = iterWalk κ' (κ'.match_ x) (c % k)

Index reduction along the spliced cycle.

The linked case: the counting bijection

noncomputable def RS.EdgeSubset.liftPeriodic {α : 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 : ↥(RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').periodicFlags) : ↥κ'.periodicFlags

Forward-map component: a lifted periodic flag, as a glued periodic flag.

Equations

• RS.EdgeSubset.liftPeriodic hij hopen s' hc' hc κ' f = ⟨⟨↑f, ⋯⟩, ⋯⟩

noncomputable def RS.EdgeSubset.spliceFlag {α : 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') (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) (x : W.SurvivingFlag i j) (hper : κ'.PeriodicFlag (κ'.match_ x)) (t : ℕ) : ↥κ'.periodicFlags

Forward-map component: a flag on a spliced cycle.

Equations

• RS.EdgeSubset.spliceFlag hij hopen s' hc' κ' x hper t = ⟨RS.EdgeSubset.iterWalk κ' (κ'.match_ x) t, ⋯⟩

theorem RS.EdgeSubset.exists_walkPerm_linked {α : 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) (hbi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (hbj : W.boundaryFlag j ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (k : ℕ) (hk1 : 1 ≤ k) (hcontA : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (W.boundaryFlag i) t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (htermA : W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (W.boundaryFlag i) k) = W.boundaryFlag j) : ∃ (e : ↥(RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').periodicFlags ⊕ Fin k ⊕ Fin k ≃ ↥κ'.periodicFlags), κ'.walkPermPeriodic = e.permCongr (Equiv.sumCongr (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').walkPermPeriodic (Equiv.sumCongr (finRotate k) (finRotate k)))

The linked-case conjugation: when the chain from bf_i exits at bf_j, the glued walk permutation is, up to a bijection, the lifted walk permutation plus two k-rotations (the two directions of the spliced circuit).

The circuit-count delta

theorem RS.EdgeSubset.openCircuitCount_linked_chain {α : 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) (hbi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (hbj : W.boundaryFlag j ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) (k : ℕ) (hk1 : 1 ≤ k) (hcontA : ∀ t < k, W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (W.boundaryFlag i) t) ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags) (htermA : W.pairing (iterWalk (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ') (W.boundaryFlag i) k) = W.boundaryFlag j) : κ'.openCircuitCount = (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').openCircuitCount + 1

Count delta in the linked case: the splice closes exactly one new circuit (two new walk orbits).

theorem RS.EdgeSubset.openCircuitCount_glueOpen_participating {α : 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) (hpi : Fragment.partnerSurvI hopen ∈ s') : κ'.openCircuitCount = (RelTransitionSystem.unglueOpen hij hopen s' hc' hc κ').openCircuitCount + if InterfaceLinked hij hopen s' hc' hc κ' hpi then 1 else 0

The circuit-count delta of a participating open glue: the glued count exceeds the unglued count by 1 exactly when the interface is linked.