The chord matching across one glue

Gluing an interface pair identifies two labels. On the subset's chord matching — the involution carrying a used label to the far end of its chain — that identification is a contraction: the two labels are removed and the far ends of their chains become each other's partners.

This file carries the label bookkeeping across the glue. The used labels of the glued subset are the used labels of the lifted one with the two glued labels removed, and the glued chord matching is the contraction of the lifted one at those two labels.

The relabel step

glueInterface relabels after every glue, so the invariant has to survive a relabel. It does: the circuit count is unchanged, and the chord matching's pairing shifts along the relabel, so the number of components is unchanged too.

theorem RS.EdgeSubset.openCircuitCount_add_unionCount_relabel {α β : Type} {W : Fragment α} [LinearOrder α] [LinearOrder β] [Fintype α] [Fintype β] (e : α ≃o β) (F : EdgeSubset W) (κ : F.RelTransitionSystem) {M N : DirMatching { a : α // W.boundaryFlag a ∈ F.boundaryFlags }} {M' N' : DirMatching { b : β // (W.relabel e.toEquiv).boundaryFlag b ∈ (relabelUp e.toEquiv F).boundaryFlags }} (heM : (DirMatching.map (usedLabRelabelEquiv e F) M').edge = M.edge) (heN : (DirMatching.map (usedLabRelabelEquiv e F) N').edge = N.edge) : (relabelTransUp e.toEquiv F κ).openCircuitCount + M'.unionCount N' = κ.openCircuitCount + M.unionCount N

The relabel preserves the circuit count and the number of components.

noncomputable def RS.EdgeSubset.usedLabelGlueEquiv {α : 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') (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) : { l : Fragment.SurvivingLabel α i j // (W.gluePairOpen i j hij hopen).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags } ≃ DirMatching.Surviving ⟨i, hbi⟩ ⟨j, hbj⟩

The glued subset's used labels are the lifted subset's, less the two glued ones.

Equations

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

theorem RS.EdgeSubset.chordInv_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') [LinearOrder α] (κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem) (l : Fragment.SurvivingLabel α i j) (hlg : (W.gluePairOpen i j hij hopen).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags) (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) : ↑({ flags := s', pairing_mem := hc' }.chordInv (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) l) = if { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.chordInv κ ↑l = i then { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.chordInv κ j else if { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.chordInv κ ↑l = j then { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.chordInv κ i else { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.chordInv κ ↑l

The glued chord matching is the lifted one, contracted. A chain of the glued subset that avoids the cut is a chain of the lifted subset; one that reaches the cut continues out of the other glued label.

theorem RS.EdgeSubset.cutMatching_glueOpen_edge {α : 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') [LinearOrder α] (κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem) (o : κ.Orientation) (o' : (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).Orientation) (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) (y : DirMatching.Surviving ⟨i, hbi⟩ ⟨j, hbj⟩) : ↑↑((DirMatching.map (usedLabelGlueEquiv hij hopen s' hc' hc hbi hbj) (cutMatching { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) o')).edge y) = ↑((cutMatching { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } κ o).contractEdge ⟨i, hbi⟩ ⟨j, hbj⟩ ↑y)

The glued cut matching's pairing is the lifted one's, contracted. Only the pairing is compared: the glued object fixes its own directions, and the number of components does not see them.

theorem RS.EdgeSubset.interfaceLinked_iff_chordInv {α : 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) (hpi : Fragment.partnerSurvI hopen ∈ s') (hbi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags) : InterfaceLinked hij hopen s' hc' hc (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) hpi ↔ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.chordInv κ i = j

The interface is linked exactly when the two glued labels are chord partners. This is the case split of the glue: linked means the chain from one glued label ends at the other, so gluing closes it into a circuit.

The invariant across one glue

The circuit count and the number of components of the union move together: the interface is linked exactly when the two glued labels are chord partners, and in that case gluing closes a circuit and merges nothing, while otherwise it merges two chains and closes nothing. So their sum is unchanged.

theorem RS.EdgeSubset.openCircuitCount_add_unionCount_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') [LinearOrder α] [Fintype α] (κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem) (o : κ.Orientation) (o' : (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).Orientation) (hpi : Fragment.partnerSurvI hopen ∈ s') (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) {N : DirMatching { a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags }} (hNij : N.edge ⟨i, hbi⟩ = ⟨j, hbj⟩) {Ng : DirMatching { l : Fragment.SurvivingLabel α i j // (W.gluePairOpen i j hij hopen).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }} (hNg : (DirMatching.map (usedLabelGlueEquiv hij hopen s' hc' hc hbi hbj) Ng).edge = (N.restrict hNij).edge) : (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).openCircuitCount + (cutMatching { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) o').unionCount Ng = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } κ o).unionCount N

One glue step preserves c-hat + c — RS21's circuit-count bookkeeping, in the form that needs neither an ordering of the interface nor the Eulerian position: only the two pairings.

One stage of the interface recursion

glueInterface glues the top pair and then relabels. Composing the two steps gives the recursion's stage: the circuit count plus the number of components is unchanged across it.

theorem RS.EdgeSubset.openCircuitCount_add_unionCount_stage {α : 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') [LinearOrder α] [Fintype α] {γ : Type} [LinearOrder γ] [Fintype γ] (e : Fragment.SurvivingLabel α i j ≃o γ) (κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem) (o : κ.Orientation) (o' : (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).Orientation) (hpi : Fragment.partnerSurvI hopen ∈ s') (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) {N : DirMatching { a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags }} (hNij : N.edge ⟨i, hbi⟩ = ⟨j, hbj⟩) {Ng : DirMatching { l : Fragment.SurvivingLabel α i j // (W.gluePairOpen i j hij hopen).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }} (hNg : (DirMatching.map (usedLabelGlueEquiv hij hopen s' hc' hc hbi hbj) Ng).edge = (N.restrict hNij).edge) {Mr Nr : DirMatching { b : γ // ((W.gluePairOpen i j hij hopen).relabel e.toEquiv).boundaryFlag b ∈ (relabelUp e.toEquiv { flags := s', pairing_mem := hc' }).boundaryFlags }} (heM : (DirMatching.map (usedLabRelabelEquiv e { flags := s', pairing_mem := hc' }) Mr).edge = (cutMatching { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) o').edge) (heN : (DirMatching.map (usedLabRelabelEquiv e { flags := s', pairing_mem := hc' }) Nr).edge = Ng.edge) : (relabelTransUp e.toEquiv { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ)).openCircuitCount + Mr.unionCount Nr = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } κ o).unionCount N

One stage of the interface recursion preserves c-hat + c.

Which of the base's subsets the glue reaches

The lift and the drop are mutually inverse where they are used, but the two closure conditions do not match: the drop of a pairing-closed subset need not be closed under the rewire. It is closed exactly when the two glued boundary flags are used together, which is the condition that the glued edge is either in the subset or out of it. So the glued fragment's subsets correspond to that subfamily of the base's, not to all of them.

def RS.EdgeSubset.AgreeingSubset {α : Type} {W : Fragment α} (i j : α) (s : Finset W.Flag) : Prop

The base's subsets the glue reaches: pairing-closed, and using the two glued boundary flags together.

Equations

• RS.EdgeSubset.AgreeingSubset i j s = ((∀ f ∈ s, W.pairing f ∈ s) ∧ (W.boundaryFlag i ∈ s ↔ W.boundaryFlag j ∈ s))

theorem RS.EdgeSubset.dropSubset_rewire_closed {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s : Finset W.Flag) (hs : AgreeingSubset i j s) (f : W.SurvivingFlag i j) : f ∈ W.dropSubset i j s → Fragment.rewire hopen f ∈ W.dropSubset i j s

The drop of a subfamily member is closed under the rewire.

The closed glue

When the two glued labels bound a common edge, gluing closes that edge into a free circle. No chain of a surviving label reaches the cut, so the chord matching simply restricts; and when the closed-off edge is in the subset, its two labels were chord partners, so a component of the union disappears — into the free circle rather than into a circuit.

theorem RS.EdgeSubset.chordInv_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) (l : Fragment.SurvivingLabel α i j) (hlg : (W.gluePairClosed i j hclosed).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags) : ↑({ flags := s', pairing_mem := hc' }.chordInv κ' l) = { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.chordInv (RelTransitionSystem.unglueClosed hclosed b s' hc' hc κ') ↑l

The chord matching restricts across a closed glue.

theorem RS.EdgeSubset.chordInv_closed_pair {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (hcT : ∀ f ∈ Fragment.liftSubsetClosed s' true, W.pairing f ∈ Fragment.liftSubsetClosed s' true) (κ : { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.RelTransitionSystem) (hbi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags) : { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.chordInv κ i = j

The two glued labels are chord partners when the closed-off edge lies in the subset: the chain from one is the edge itself.

noncomputable def RS.EdgeSubset.usedLabelGlueClosedEquiv {α : Type} {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') (hcT : ∀ f ∈ Fragment.liftSubsetClosed s' true, W.pairing f ∈ Fragment.liftSubsetClosed s' true) (hbi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags) (hbj : W.boundaryFlag j ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags) : { l : Fragment.SurvivingLabel α i j // (W.gluePairClosed i j hclosed).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags } ≃ DirMatching.Surviving ⟨i, hbi⟩ ⟨j, hbj⟩

The glued subset's used labels across a closed glue whose edge lies in the subset: the lifted ones, less the two glued.

Equations

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

theorem RS.EdgeSubset.unionCount_glueClosed {α : Type} {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') (hcT : ∀ f ∈ Fragment.liftSubsetClosed s' true, W.pairing f ∈ Fragment.liftSubsetClosed s' true) [LinearOrder α] [Fintype α] (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) (o' : κ'.Orientation) (o : (RelTransitionSystem.unglueClosed hclosed true s' hc' hcT κ').Orientation) (hbi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags) (hbj : W.boundaryFlag j ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags) {N : DirMatching { a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags }} (hNij : N.edge ⟨i, hbi⟩ = ⟨j, hbj⟩) {Ng : DirMatching { l : Fragment.SurvivingLabel α i j // (W.gluePairClosed i j hclosed).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }} (hNg : (DirMatching.map (usedLabelGlueClosedEquiv hclosed s' hc' hcT hbi hbj) Ng).edge = (N.restrict hNij).edge) : (cutMatching { flags := s', pairing_mem := hc' } κ' o').unionCount Ng + 1 = (cutMatching { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT } (RelTransitionSystem.unglueClosed hclosed true s' hc' hcT κ') o).unionCount N

A closed glue drops one component. The chord matching restricts, and the two glued labels were partners, so the component they formed disappears — into the free circle the glue creates.

theorem RS.EdgeSubset.openCircuitCount_add_unionCount_glueClosed {α : Type} {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') (hcT : ∀ f ∈ Fragment.liftSubsetClosed s' true, W.pairing f ∈ Fragment.liftSubsetClosed s' true) [LinearOrder α] [Fintype α] (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) (o' : κ'.Orientation) (o : (RelTransitionSystem.unglueClosed hclosed true s' hc' hcT κ').Orientation) (hbi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags) (hbj : W.boundaryFlag j ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags) {N : DirMatching { a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags }} (hNij : N.edge ⟨i, hbi⟩ = ⟨j, hbj⟩) {Ng : DirMatching { l : Fragment.SurvivingLabel α i j // (W.gluePairClosed i j hclosed).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }} (hNg : (DirMatching.map (usedLabelGlueClosedEquiv hclosed s' hc' hcT hbi hbj) Ng).edge = (N.restrict hNij).edge) : κ'.openCircuitCount + (cutMatching { flags := s', pairing_mem := hc' } κ' o').unionCount Ng + 1 = (RelTransitionSystem.unglueClosed hclosed true s' hc' hcT κ').openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT } (RelTransitionSystem.unglueClosed hclosed true s' hc' hcT κ') o).unionCount N

The closed glue's ledger: the circuit count is unchanged and one component disappears, the free circle the glue creates taking its place.