The interface matching on a fragment's used labels

RS21 pairs the chord matching M(ω,κ) with the matching that identifies the two fragments' labels, and counts the components of their union. In the flag model that second matching lives on the labels of a single fragment whose boundary index is a sum: the left half is one side's labels, the right half the other's, and an identification of the two halves says which label is glued to which.

Only the labels the subset uses carry chords, so the interface matching has to be read there — which asks that the subset use the two halves of every interface pair together. That is exactly the condition under which a glued edge is in the Eulerian subset or out of it, and it is what the boundary state pins.

def RS.EdgeSubset.InterfacePaired {γ δ : Type} {V : Fragment (γ ⊕ δ)} (F : EdgeSubset V) (e : γ ≃ δ) : Prop

The subset uses the two halves of every interface pair together.

Equations

• F.InterfacePaired e = ∀ (a : γ), V.boundaryFlag (Sum.inl a) ∈ F.boundaryFlags ↔ V.boundaryFlag (Sum.inr (e a)) ∈ F.boundaryFlags

def RS.EdgeSubset.usedSideEquiv {γ δ : Type} {V : Fragment (γ ⊕ δ)} (F : EdgeSubset V) : UsedLab F ≃ { a : γ // V.boundaryFlag (Sum.inl a) ∈ F.boundaryFlags } ⊕ { b : δ // V.boundaryFlag (Sum.inr b) ∈ F.boundaryFlags }

The used labels, split by side.

Equations

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

def RS.EdgeSubset.interfaceSideEquiv {γ δ : Type} {V : Fragment (γ ⊕ δ)} (F : EdgeSubset V) (e : γ ≃ δ) (hp : F.InterfacePaired e) : { a : γ // V.boundaryFlag (Sum.inl a) ∈ F.boundaryFlags } ≃ { b : δ // V.boundaryFlag (Sum.inr b) ∈ F.boundaryFlags }

The identification of the two sides' used labels.

Equations

• F.interfaceSideEquiv e hp = e.subtypeEquiv ⋯

noncomputable def RS.EdgeSubset.interfaceCut {γ δ : Type} {V : Fragment (γ ⊕ δ)} (F : EdgeSubset V) (e : γ ≃ δ) (hp : F.InterfacePaired e) : DirMatching (UsedLab F)

The interface matching on the used labels: each used label of one side paired with the label it is glued to.

Equations

• F.interfaceCut e hp = RS.DirMatching.map F.usedSideEquiv.symm (RS.DirMatching.interfaceEquivMatching (F.interfaceSideEquiv e hp))

def RS.EdgeSubset.interfaceSwap {γ δ : Type} (e : γ ≃ δ) : γ ⊕ δ → γ ⊕ δ

The label involution the interface matching realises: swap sides along the identification.

Equations

• RS.EdgeSubset.interfaceSwap e = Sum.elim (fun (a : γ) => Sum.inr (e a)) fun (b : δ) => Sum.inl (e.symm b)

theorem RS.EdgeSubset.interfaceCut_edge_val {γ δ : Type} {V : Fragment (γ ⊕ δ)} (F : EdgeSubset V) (e : γ ≃ δ) (hp : F.InterfacePaired e) (x : UsedLab F) : ↑((F.interfaceCut e hp).edge x) = interfaceSwap e ↑x

The interface matching pairs by the swap.

Pairing, read on the swap

InterfacePaired is about the two halves of a sum; the constructions the recursion applies — a glue, then a relabel — do not preserve that shape, the glued fragment's labels being a subtype rather than a sum. Reading the condition on the swap instead removes the shape from it, and then both constructions transport it by a single equation between label maps.

def RS.EdgeSubset.SwapPaired {L : Type} {V : Fragment L} (F : EdgeSubset V) (ι : L → L) : Prop

The subset uses a label exactly when it uses its partner.

Equations

• F.SwapPaired ι = ∀ (x : L), V.boundaryFlag x ∈ F.boundaryFlags ↔ V.boundaryFlag (ι x) ∈ F.boundaryFlags

theorem RS.EdgeSubset.swapPaired_iff_interfacePaired {γ δ : Type} {V : Fragment (γ ⊕ δ)} (F : EdgeSubset V) (e : γ ≃ δ) : F.SwapPaired (interfaceSwap e) ↔ F.InterfacePaired e

Pairing on the swap is pairing across the interface.

theorem RS.EdgeSubset.swapPaired_of_mem_iff {L L' : Type} {V : Fragment L} {V' : Fragment L'} (F : EdgeSubset V) (F' : EdgeSubset V') (ι : L → L) (ι' : L' → L') (φ : L' → L) (hmem : ∀ (x : L'), V'.boundaryFlag x ∈ F'.boundaryFlags ↔ V.boundaryFlag (φ x) ∈ F.boundaryFlags) (hcomp : ∀ (x : L'), φ (ι' x) = ι (φ x)) (h : F.SwapPaired ι) : F'.SwapPaired ι'

Pairing transports along any reading of one subset's used labels in another's. Both constructions the recursion applies are of this shape: a glue reads a surviving label as a label, a relabel reads a new index as an old one.

theorem RS.EdgeSubset.swapPaired_relabelUp {α β : Type} [LinearOrder α] [LinearOrder β] {W : Fragment α} (E : α ≃o β) (F : EdgeSubset W) (ι : α → α) (ι' : β → β) (hcomp : ∀ (x : α), E.symm (ι' (E x)) = ι x) (h : F.SwapPaired ι) : (relabelUp E.toEquiv F).SwapPaired ι'

Pairing shifts through a relabel.

theorem RS.EdgeSubset.agreeingSubset_of_swapPaired {L : Type} {V : Fragment L} (F : EdgeSubset V) (ι : L → L) (h : F.SwapPaired ι) {i j : L} (hij : ι i = j) : AgreeingSubset i j F.flags

A paired subset reaches the glue. The glue only sees the base's subsets that use its two labels together, and a subset paired by the swap uses them together whenever the swap pairs them.

theorem RS.EdgeSubset.edge_eq_of_swap {L : Type} {V : Fragment L} (F : EdgeSubset V) (ι : L → L) {N : DirMatching (UsedLab F)} (hN : ∀ (x : UsedLab F), ↑(N.edge x) = ι ↑x) {i j : L} (hbi : V.boundaryFlag i ∈ F.boundaryFlags) (hbj : V.boundaryFlag j ∈ F.boundaryFlags) (hij : ι i = j) : N.edge ⟨i, hbi⟩ = ⟨j, hbj⟩

The glued pair are partners of the interface matching, which is what makes the glue contract it.

The interface matching through a relabel

The interface recursion relabels after every glue, and the relabel carries the interface identification with it. Since the matching's pairing is the swap, all the transport has to check is that the swap commutes with the relabel — one equation between label maps, with no subsets, systems or orientations in it.

theorem RS.EdgeSubset.interfaceCut_relabelUp_edge {α γ' δ' : Type} [LinearOrder α] [LinearOrder (γ' ⊕ δ')] {W : Fragment α} (F : EdgeSubset W) (E : α ≃o γ' ⊕ δ') (e' : γ' ≃ δ') (hp' : (relabelUp E.toEquiv F).InterfacePaired e') (x : UsedLab F) : ↑((DirMatching.map (usedLabRelabelEquiv E F) ((relabelUp E.toEquiv F).interfaceCut e' hp')).edge x) = E.symm (interfaceSwap e' (E ↑x))

The relabelled interface matching pairs by the transported swap.

One stage of the interface matching

At a stage the fragment is glued and then relabelled, and the interface matching of the result has to be the base's, contracted at the glued pair. All four kinds of cut read a surviving label as a label, so the whole comparison is one equation between label maps: the transported swap on surviving labels is the base's swap.

theorem RS.EdgeSubset.restrict_edge_of_swap {L Lg : Type} {V : Fragment L} {Vg : Fragment Lg} (Fl : EdgeSubset V) (Fg : EdgeSubset Vg) (φ : Lg → L) (ι : L → L) {N : DirMatching (UsedLab Fl)} (hN : ∀ (x : UsedLab Fl), ↑(N.edge x) = ι ↑x) {Ng : DirMatching (UsedLab Fg)} (hNg : ∀ (z : UsedLab Fg), φ ↑(Ng.edge z) = ι (φ ↑z)) {i j : UsedLab Fl} (hNij : N.edge i = j) (G : UsedLab Fg ≃ DirMatching.Surviving i j) (hG : ∀ (w : UsedLab Fg), ↑↑(G w) = φ ↑w) : (DirMatching.map G Ng).edge = (N.restrict hNij).edge

A glue restricts a matching that pairs by an involution of the labels. Both sides pair by the same involution, so reading the glued fragment's matching on the base's used labels gives the base's, restricted at the glued pair.

The swap through the interface step

The recursion's relabel is interfaceStepEquiv, which deletes the glued label from each half and re-indexes. The interface swap commutes with it: on either side the deletion is at the top of the half, so it leaves every surviving label's index alone, and the swap is the identity on indices.

def RS.EdgeSubset.stepIdent (n : ℕ) : Fin (0 + n) ≃ Fin (n + 0)

The identification of the two halves at interface size n.

Equations

• RS.EdgeSubset.stepIdent n = finCongr ⋯

theorem RS.EdgeSubset.stepIdent_val {n : ℕ} (v : Fin (0 + n)) : ↑((stepIdent n) v) = ↑v

The interface identification keeps a label's index.

theorem RS.EdgeSubset.interfaceSwap_interfaceStep (n : ℕ) (x : { x : Fin (0 + n + 1) ⊕ Fin (n + 1 + 0) // x ≠ Sum.inl ⟨0 + n, ⋯⟩ ∧ x ≠ Sum.inr ⟨n, ⋯⟩ }) : ↑((interfaceStepEquiv 0 n 0).symm (interfaceSwap (stepIdent n) ((interfaceStepEquiv 0 n 0) x))) = interfaceSwap (stepIdent (n + 1)) ↑x

The interface swap commutes with the recursion's relabel.

theorem RS.EdgeSubset.interfaceSwap_cut (n : ℕ) : interfaceSwap (stepIdent (n + 1)) (Sum.inl ⟨0 + n, ⋯⟩) = Sum.inr ⟨n, ⋯⟩

The recursion's cut pair are interface partners, which is what makes the glue contract the interface matching rather than merge two of its arcs.

The closed top

At the empty interface there are no labels, hence no through edges, and the through-edge product the flag model carries is one. That is where RS21's s_h(G,H) and the flag model's summand meet.

theorem RS.EdgeSubset.throughFlags_isEmpty {L : Type} [IsEmpty L] {V : Fragment L} (F : EdgeSubset V) : F.throughFlags = ∅

A closed fragment has no through flags: every flag meets a vertex.

theorem RS.EdgeSubset.allInternal_isEmpty {L : Type} [IsEmpty L] {V : Fragment L} (F : EdgeSubset V) : F.allInternal

At the closed top every flag is internal: there are no labels to attach to.

theorem RS.EdgeSubset.pathSign_isEmpty {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} (F : EdgeSubset V) (κ : F.RelTransitionSystem) : pathSign κ = 1

The chord sign is trivial at the closed top. There are no labels, hence no chords to cross.

theorem RS.EdgeSubset.throughValueC_isEmpty {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} {k ℓ : ℕ} (F : EdgeSubset V) (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) (hbnd : genBoundarySubsetMatches V F.flags st) (hne : Nonempty F.CanonData) : F.throughValueC h st hbnd = F.throughSummand h st hbnd (↑(Classical.choice hne).snd) (Classical.choice hne).fst.openCircuitCount

The closed top's value is RS21's s_h(G,H): the circuit sign times the colouring sum, with no chord sign and no through-edge product.

theorem RS.EdgeSubset.throughMixedPartitionC_isEmpty {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) : throughMixedPartitionC h V st = (↑k - 2 * ↑ℓ) ^ V.circles * ∑ s : Finset V.Flag, if hc : ∀ f ∈ s, V.pairing f ∈ s then if hbnd : genBoundarySubsetMatches V s st then if { flags := s, pairing_mem := hc }.Eulerian then if hne : Nonempty { flags := s, pairing_mem := hc }.CanonData then { flags := s, pairing_mem := hc }.throughSummand h st hbnd (↑(Classical.choice hne).snd) (Classical.choice hne).fst.openCircuitCount else 0 else 0 else 0 else 0

The closed top's partition value is a sum of RS21's summands. With no labels the chord sign is one and the through-edge product is one, so each Eulerian subset contributes its circuit sign times its colouring sum — RS21's s_h(G,H).

theorem RS.EdgeSubset.throughProduct_isEmpty {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} {k ℓ : ℕ} (F : EdgeSubset V) (st : GenBoundaryState k ℓ L) : F.throughProduct st = 1

The through-edge product is one at the closed top.

The union at a disjoint union

At the start of the interface recursion the fragment is a disjoint union, its two boundary halves are the two fragments' own labels, and its chord matching is the two fragments' chord matchings side by side. So the union of the chord matching with the interface matching is RS21's own union M(ω₁,κ₁) ∪ M(ω₂,κ₂), read on one copy of the label set through the interface identification — which is the form Lemma 11 for a composition consumes.

def RS.EdgeSubset.usedLeftEquiv {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) : { a : α // (W₁.disjUnion W₂).boundaryFlag (Sum.inl a) ∈ F.boundaryFlags } ≃ UsedLab (leftSub F)

The used labels of the left half.

Equations

• F.usedLeftEquiv = Equiv.subtypeEquivRight ⋯

def RS.EdgeSubset.usedRightEquiv {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) : { b : β // (W₁.disjUnion W₂).boundaryFlag (Sum.inr b) ∈ F.boundaryFlags } ≃ UsedLab (rightSub F)

The used labels of the right half.

Equations

• F.usedRightEquiv = Equiv.subtypeEquivRight ⋯

def RS.EdgeSubset.usedDisjUnionEquiv {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) : UsedLab F ≃ UsedLab (leftSub F) ⊕ UsedLab (rightSub F)

The used labels of a disjoint union, split into the two sides' own.

Equations

• F.usedDisjUnionEquiv = F.usedSideEquiv.trans (F.usedLeftEquiv.sumCongr F.usedRightEquiv)

theorem RS.EdgeSubset.chordInv_prodRel_inl {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) {a : α} (hb : (W₁.disjUnion W₂).boundaryFlag (Sum.inl a) ∈ F.boundaryFlags) : F.chordInv (prodRel κ₁ κ₂) (Sum.inl a) = Sum.inl ((leftSub F).chordInv κ₁ a)

The chord of a left label is the left side's chord.

theorem RS.EdgeSubset.chordInv_prodRel_inr {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) {b : β} (hb : (W₁.disjUnion W₂).boundaryFlag (Sum.inr b) ∈ F.boundaryFlags) : F.chordInv (prodRel κ₁ κ₂) (Sum.inr b) = Sum.inr ((rightSub F).chordInv κ₂ b)

The chord of a right label is the right side's chord.

theorem RS.EdgeSubset.cutMatching_disjUnion_edge {α β : Type} [LinearOrder α] [LinearOrder β] [LinearOrder (α ⊕ β)] {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) (o₁ : κ₁.Orientation) (o₂ : κ₂.Orientation) : (DirMatching.map F.usedDisjUnionEquiv (cutMatching F (prodRel κ₁ κ₂) (prodOrient o₁ o₂))).edge = ((cutMatching (leftSub F) κ₁ o₁).sumMatching (cutMatching (rightSub F) κ₂ o₂)).edge

The chord matching of a disjoint union is the two sides' chord matchings, side by side.

def RS.EdgeSubset.interfaceSideDisjEquiv {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) (e : α ≃ β) (hp : F.InterfacePaired e) : UsedLab (leftSub F) ≃ UsedLab (rightSub F)

The interface identification, read on the two sides' own used labels.

Equations

• F.interfaceSideDisjEquiv e hp = F.usedLeftEquiv.symm.trans ((F.interfaceSideEquiv e hp).trans F.usedRightEquiv)

def RS.EdgeSubset.interfaceSideDisjOrderIso {α β : Type} [LinearOrder α] [LinearOrder β] {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) (E : α ≃o β) (hp : F.InterfacePaired E.toEquiv) : UsedLab (leftSub F) ≃o UsedLab (rightSub F)

The interface identification on the two sides' used labels, as an order isomorphism when the identification is one.

Equations

• F.interfaceSideDisjOrderIso E hp = { toEquiv := F.interfaceSideDisjEquiv E.toEquiv hp, map_rel_iff' := ⋯ }

theorem RS.EdgeSubset.interfaceCut_disjUnion_edge {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) (e : α ≃ β) (hp : F.InterfacePaired e) : (DirMatching.map F.usedDisjUnionEquiv (F.interfaceCut e hp)).edge = (DirMatching.interfaceEquivMatching (F.interfaceSideDisjEquiv e hp)).edge

The interface matching of a disjoint union is the interface identification, read on the two sides' used labels.

theorem RS.EdgeSubset.vertexSum_disjUnion {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ (α ⊕ β)) (hbnd : genBoundarySubsetMatches (W₁.disjUnion W₂) F.flags st) (hbnd₁ : genBoundarySubsetMatches W₁ (leftSub F).flags fun (a : α) => st (Sum.inl a)) (hbnd₂ : genBoundarySubsetMatches W₂ (rightSub F).flags fun (b : β) => st (Sum.inr b)) {κ₁ : (leftSub F).RelTransitionSystem} {κ₂ : (rightSub F).RelTransitionSystem} (o₁ : κ₁.Orientation) (o₂ : κ₂.Orientation) : F.vertexSum h st hbnd (prodOrient o₁ o₂) = (leftSub F).vertexSum h (fun (a : α) => st (Sum.inl a)) hbnd₁ o₁ * (rightSub F).vertexSum h (fun (b : β) => st (Sum.inr b)) hbnd₂ o₂

The colouring sum splits over a disjoint union. RS21's ∏_{v ∈ V′(F₁∗F₂)} is ∏_{v ∈ V′(F₁)} ∏_{v ∈ V′(F₂)}, and at a fixed interface colouring the two sides' sums are independent.

theorem RS.EdgeSubset.unionCount_cutMatching_disjUnion {α β : Type} [LinearOrder α] [LinearOrder β] [Fintype α] [Fintype β] [LinearOrder (α ⊕ β)] {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) (e : α ≃ β) (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) (o₁ : κ₁.Orientation) (o₂ : κ₂.Orientation) (hp : F.InterfacePaired e) : (cutMatching F (prodRel κ₁ κ₂) (prodOrient o₁ o₂)).unionCount (F.interfaceCut e hp) = (cutMatching (leftSub F) κ₁ o₁).unionCount (DirMatching.map (F.interfaceSideDisjEquiv e hp).symm (cutMatching (rightSub F) κ₂ o₂))

RS21's union, at the start of the recursion. The union of a disjoint union's chord matching with its interface matching counts what the two fragments' own chord matchings count, identified along the interface.