The directed matching a transition system induces on the used labels

An Eulerian subset with a compatible local pairing decomposes into circuits and directed trails between labelled ends. The trails give a directed perfect matching on the labels the subset uses: partners are the two ends of a trail, and the direction is the one the trail runs in.

Two kinds of trail occur. Most have at least one internal step, and there the orientation's chain direction reads the trail's sense off the entry edge; the two ends carry opposite values by chain-direction rigidity. A trail of a single edge — both of whose ends are labelled — has no internal step, and the orientation's laws say nothing about it, so its sense is taken from the label order. That is the same orientation the mixed partition function's own through-edge product uses.

def RS.IsThroughLabel {α : Type} {W : Fragment α} (F : EdgeSubset W) (i : α) : Prop

A used label whose trail is a single edge: its entry edge is another used label's flag.

Equations

• RS.IsThroughLabel F i = (W.pairing (W.boundaryFlag i) ∈ F.boundaryFlags)

theorem RS.pairing_internal_of_not_through {α : Type} {W : Fragment α} (F : EdgeSubset W) {i : α} (hb : W.boundaryFlag i ∈ F.boundaryFlags) (hnt : ¬IsThroughLabel F i) : W.pairing (W.boundaryFlag i) ∈ F.internalFlags

Off the single-edge trails the entry edge is internal.

theorem RS.isThroughLabel_chordInv {α : Type} {W : Fragment α} (F : EdgeSubset W) (κ : F.RelTransitionSystem) {i : α} (hb : W.boundaryFlag i ∈ F.boundaryFlags) (ht : IsThroughLabel F i) : IsThroughLabel F (F.chordInv κ i)

The single-edge trails come in pairs.

theorem RS.decide_lt_flip {α : Type} [LinearOrder α] {i j : α} (h : i ≠ j) : decide (j < i) = !decide (i < j)

Comparing two distinct labels the other way negates.

noncomputable def RS.cutMatching {α : Type} [LinearOrder α] {W : Fragment α} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (o : κ.Orientation) : DirMatching { i : α // W.boundaryFlag i ∈ F.boundaryFlags }

The directed matching a transition system induces on the used labels — RS21's M(ω,κ). Partners are the two ends of a trail; the direction is the trail's own, read from the orientation where the trail has an internal step and from the label order where it is a single edge.

Equations

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

Undoing the dual basis

RS21's boundary vector at a used leg is f_{χ₁(i)} where the arc enters and g_{χ₁(i)} where it leaves. Written in the basis of the f's, the leaving legs carry the partner colour and the partner sign. So a basis coordinate x of the tensor determines χ₁ by undoing the partner at the legs the trail leaves, and contributes the product of those legs' signs.

The two operations below are that change of basis and its weight.

theorem RS.chordInv_relabelUp {α : Type} [LinearOrder α] {W : Fragment α} {β : Type} [LinearOrder β] (e : α ≃o β) (F : EdgeSubset W) (κ : F.RelTransitionSystem) (b : β) : (EdgeSubset.relabelUp e.toEquiv F).chordInv (relabelTransUp e.toEquiv F κ) b = e (F.chordInv κ (e.symm b))

The chord involution shifts through the relabel.

noncomputable def RS.usedLabRelabelEquiv {α : Type} [LinearOrder α] {W : Fragment α} {β : Type} [LinearOrder β] (e : α ≃o β) (F : EdgeSubset W) : { b : β // (W.relabel e.toEquiv).boundaryFlag b ∈ (EdgeSubset.relabelUp e.toEquiv F).boundaryFlags } ≃ { a : α // W.boundaryFlag a ∈ F.boundaryFlags }

The used labels shift through the relabel.

Equations

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

theorem RS.cutMatching_relabelUp_edge {α : Type} [LinearOrder α] {W : Fragment α} {β : Type} [LinearOrder β] (e : α ≃o β) (F : EdgeSubset W) (κ : F.RelTransitionSystem) (o' : (relabelTransUp e.toEquiv F κ).Orientation) (a : { a : α // W.boundaryFlag a ∈ F.boundaryFlags }) : ↑((DirMatching.map (usedLabRelabelEquiv e F) (cutMatching (EdgeSubset.relabelUp e.toEquiv F) (relabelTransUp e.toEquiv F κ) o')).edge a) = F.chordInv κ ↑a

The chord matching shifts through the relabel, on pairings.

The arcs' directions, as data

RS21's Eulerian orientation directs every edge of the subset, including one whose two ends are both labelled. The chain orientation of a relative transition system directs only the internal flags, so it fixes the direction of a chain but says nothing about such an edge. The missing freedom is recorded here: the directions of the chord matching's arcs are taken as data — any directed matching on the used labels whose partner map is the chord involution — and the chain orientation supplies one choice among them.

Only the directions enter the change of basis and its weight, so both are stated against a bare direction function.

@[reducible, inline]

abbrev RS.UsedLab {α : Type} {W : Fragment α} (F : EdgeSubset W) : Type

The used labels of a subset.

Equations

• RS.UsedLab F = { i : α // W.boundaryFlag i ∈ F.boundaryFlags }

noncomputable def RS.untwistD {α : Type} {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (tl : UsedLab F → Bool) (x : GenBoundaryState k ℓ α) : GenBoundaryState k ℓ α

Undo the dual basis against a given set of arc directions.

Equations

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

noncomputable def RS.dualWeightD {α : Type} {W : Fragment α} [Fintype α] {k ℓ : ℕ} (F : EdgeSubset W) (tl : UsedLab F → Bool) (x : GenBoundaryState k ℓ α) : ℂ

The dual basis's weight against a given set of arc directions.

Equations

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

noncomputable def RS.untwist {α : Type} [LinearOrder α] {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (o : κ.Orientation) (x : GenBoundaryState k ℓ α) : GenBoundaryState k ℓ α

Undo the dual basis: partner the colour at each leg the trail leaves.

Equations

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

noncomputable def RS.dualWeight {α : Type} [LinearOrder α] {W : Fragment α} [Fintype α] {k ℓ : ℕ} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (o : κ.Orientation) (x : GenBoundaryState k ℓ α) : ℂ

The dual basis's weight: the partner signs at the legs the trail leaves.

Equations

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

A chain flip touches only its own two labels

The flip set of a ported chain consists of internal flags, and its only exits are the two ports, whose partners are the chain's two boundary flags. So a used label whose entry flag lies in the flip set is one of those two.

theorem RS.label_of_pairing_mem_flipSet {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ i₂) {i : α} (hb : W.boundaryFlag i ∈ F.boundaryFlags) (hmem : W.pairing (W.boundaryFlag i) ∈ S) : i = i₁ ∨ i = i₂

Only the chain's own two labels have their entry flag in the flip set.

theorem RS.pairing_boundaryFlag_eq_port {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ i₂) : W.pairing (W.boundaryFlag i₁) = p₁

The chain's near port is the entry flag of its first label.

theorem RS.pairing_boundaryFlag_eq_port' {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ i₂) : W.pairing (W.boundaryFlag i₂) = p₂

And of its second.

theorem RS.not_isThroughLabel_port {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ i₂) : ¬IsThroughLabel F i₁

A chain's own labels are not through-labels: their entry flags are internal.

theorem RS.not_isThroughLabel_port' {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ i₂) : ¬IsThroughLabel F i₂

And the second.

A chain flip reverses one arc

RS21's M(ω′,κ′) differs from M(ω,κ) by inverting one arc. In the flag model that is exactly what a chain flip does: the tail function changes at the chain's two labels and nowhere else, and those two labels are the ends of one arc.

theorem RS.cutMatching_portFlip {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ i₂) (hb₁ : W.boundaryFlag i₁ ∈ F.boundaryFlags) (hchord : F.chordInv κ i₁ = i₂) : cutMatching F κ (o.portFlip h) = (cutMatching F κ o).reverseArc ⟨i₁, hb₁⟩

A chain flip reverses exactly the chain's own arc.

theorem RS.exists_chainFlip {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (o : κ.Orientation) {i₁ : α} (hb₁ : W.boundaryFlag i₁ ∈ F.boundaryFlags) (hnt : ¬IsThroughLabel F i₁) : ∃ (S : Finset W.Flag) (p₁ : W.Flag) (p₂ : W.Flag) (hp : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ (F.chordInv κ i₁)), cutMatching F κ (o.portFlip hp) = (cutMatching F κ o).reverseArc ⟨i₁, hb₁⟩

A used label whose chain has an interior admits a chain flip. This is the half of RS21's step 1 the chain orientation provides: the trail through the interior can be inverted, and doing so reverses exactly that label's arc.

Evaluating the change of basis

Undoing the dual basis acts pointwise: at a used label it partners the colour exactly when the trail leaves that label, and elsewhere it does nothing.

theorem RS.untwist_apply_of_mem {α : Type} [LinearOrder α] {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (o : κ.Orientation) (x : GenBoundaryState k ℓ α) {i : α} (hb : W.boundaryFlag i ∈ F.boundaryFlags) : untwist F κ o x i = if (cutMatching F κ o).tail ⟨i, hb⟩ = true then match x i with | Sum.inl a => Sum.inl a | Sum.inr c => Sum.inr (oddPartner ℓ c) else x i

The change of basis at a used label.

theorem RS.untwist_apply_of_not_mem {α : Type} [LinearOrder α] {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (o : κ.Orientation) (x : GenBoundaryState k ℓ α) {i : α} (hb : W.boundaryFlag i ∉ F.boundaryFlags) : untwist F κ o x i = x i

The change of basis is trivial off the used labels.

The chain flip's effect on the dual basis

Reversing a chain exchanges which of its two ends is the tail, so undoing the dual basis after the flip is undoing it before with the two ends' colours partnered — which is the state flip the summand's own chain-flip ledger produces.

theorem RS.dualFactor_sq {k ℓ : ℕ} (v : Fin k ⊕ Fin (2 * ℓ)) : ((match v with | Sum.inl val => 1 | Sum.inr c => dualSign ℓ c) * match v with | Sum.inl val => 1 | Sum.inr c => dualSign ℓ c) = 1

The dual basis's per-label weight squares to one.

theorem RS.tail_portFlip_of_mem {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ i₂) (hb₁ : W.boundaryFlag i₁ ∈ F.boundaryFlags) (hchord : F.chordInv κ i₁ = i₂) {i : α} (hb : W.boundaryFlag i ∈ F.boundaryFlags) (hj : i = i₁ ∨ i = i₂) : (cutMatching F κ (o.portFlip h)).tail ⟨i, hb⟩ = !(cutMatching F κ o).tail ⟨i, hb⟩

The direction flips at the chain's two labels.

theorem RS.tail_portFlip_of_not_mem {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ i₂) (hb₁ : W.boundaryFlag i₁ ∈ F.boundaryFlags) (hchord : F.chordInv κ i₁ = i₂) {i : α} (hb : W.boundaryFlag i ∈ F.boundaryFlags) (hj : ¬(i = i₁ ∨ i = i₂)) : (cutMatching F κ (o.portFlip h)).tail ⟨i, hb⟩ = (cutMatching F κ o).tail ⟨i, hb⟩

And nowhere else.

theorem RS.untwist_portFlip {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ i₂) (hb₁ : W.boundaryFlag i₁ ∈ F.boundaryFlags) (hchord : F.chordInv κ i₁ = i₂) {k ℓ : ℕ} (x : GenBoundaryState k ℓ α) : untwist F κ (o.portFlip h) x = stateOddFlip (untwist F κ o x) i₁ i₂

A chain flip partners the two chain ends.

theorem RS.dualWeight_portFlip_mul {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : EdgeSubset.PortedFlipSet κ S p₁ p₂ i₁ i₂) (hb₁ : W.boundaryFlag i₁ ∈ F.boundaryFlags) (hchord : F.chordInv κ i₁ = i₂) [Fintype α] {k ℓ : ℕ} (x : GenBoundaryState k ℓ α) {c₁ c₂ : Fin (2 * ℓ)} (hc₁ : x i₁ = Sum.inr c₁) (hc₂ : x i₂ = Sum.inr c₂) : dualWeight F κ (o.portFlip h) x * dualWeight F κ o x = dualSign ℓ c₁ * dualSign ℓ c₂

The chain flip's weight: the dual basis's weights before and after a chain flip multiply to the two chain ends' signs, since they differ exactly at those two labels and every factor squares to one.

theorem RS.untwist_apply_odd {α : Type} [LinearOrder α] {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (o : κ.Orientation) (x : GenBoundaryState k ℓ α) {i : α} (hb : W.boundaryFlag i ∈ F.boundaryFlags) {c : Fin (2 * ℓ)} (hc : x i = Sum.inr c) : untwist F κ o x i = Sum.inr (if (cutMatching F κ o).tail ⟨i, hb⟩ = true then oddPartner ℓ c else c)

The change of basis at an odd used label.

Reversing one arc's direction

RS21's (12) inverts a directed trail. When the trail is a single edge joining two labelled ends there is nothing inside to invert, so the whole effect is on the dual basis: the leg that carried g carries f and the other way about. The two legs' weights are therefore exchanged, and since the two ends of an arc carry partner colours, the exchange costs a sign.

theorem RS.dualWeightD_reverseArc_mul {α : Type} {W : Fragment α} [Fintype α] [DecidableEq α] {k ℓ : ℕ} (F : EdgeSubset W) (M : DirMatching (UsedLab F)) (a : UsedLab F) (x : GenBoundaryState k ℓ α) {c : Fin (2 * ℓ)} (hta : M.tail a = true) (hca : x ↑a = Sum.inr c) (hca' : x ↑(M.edge a) = Sum.inr (oddPartner ℓ c)) : dualWeightD F (M.reverseArc a).tail x * dualWeightD F M.tail x = -1

Reversing an arc exchanges the two legs' weights, at a cost of one sign. The hypothesis is the support condition: the two ends of an arc carry partner colours.

theorem RS.untwistD_apply_mem {α : Type} {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (tl : UsedLab F → Bool) (x : GenBoundaryState k ℓ α) {i : α} (hb : W.boundaryFlag i ∈ F.boundaryFlags) : untwistD F tl x i = if tl ⟨i, hb⟩ = true then Sum.map id (oddPartner ℓ) (x i) else x i

The change of basis at a used leg.

theorem RS.untwistD_apply_not_mem {α : Type} {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (tl : UsedLab F → Bool) (x : GenBoundaryState k ℓ α) {i : α} (hb : W.boundaryFlag i ∉ F.boundaryFlags) : untwistD F tl x i = x i

The change of basis away from the used legs.

theorem RS.untwistD_reverseArc {α : Type} {W : Fragment α} [DecidableEq α] {k ℓ : ℕ} (F : EdgeSubset W) (M : DirMatching (UsedLab F)) (a : UsedLab F) (x : GenBoundaryState k ℓ α) : untwistD F (M.reverseArc a).tail x = stateOddFlip (untwistD F M.tail x) ↑a ↑(M.edge a)

Reversing an arc partners the colour at its two legs.

theorem RS.dualWeightD_mul_self {α : Type} {W : Fragment α} [Fintype α] {k ℓ : ℕ} (F : EdgeSubset W) (tl : UsedLab F → Bool) (x : GenBoundaryState k ℓ α) : dualWeightD F tl x * dualWeightD F tl x = 1

The dual basis's weight at given arc directions squares to one.

theorem RS.genBoundarySubsetMatches_untwistD {α : Type} {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (tl : UsedLab F → Bool) (x : GenBoundaryState k ℓ α) : genBoundarySubsetMatches W F.flags (untwistD F tl x) ↔ genBoundarySubsetMatches W F.flags x

The change of basis preserves which legs are odd, so the subset-matching condition does not see the arc directions.

theorem RS.dualWeight_mul_self {α : Type} [LinearOrder α] {W : Fragment α} [Fintype α] {k ℓ : ℕ} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (o : κ.Orientation) (x : GenBoundaryState k ℓ α) : dualWeight F κ o x * dualWeight F κ o x = 1

The dual basis's weight squares to one.

The through-edge product ignores a chain flip

A chain's two labels are not through-labels, so flipping the state there leaves every through-edge's two colours alone.

theorem RS.isThroughLabel_of_mem_throughFlags {α : Type} {W : Fragment α} {F : EdgeSubset W} {f : W.Flag} (hf : f ∈ F.throughFlags) {i : α} (hi : W.attach f = Sum.inr i) : IsThroughLabel F i

A through-flag's own label is a through-label.

theorem RS.mem_throughFlags_of_isThroughLabel {α : Type} {W : Fragment α} {F : EdgeSubset W} {i : α} (hb : W.boundaryFlag i ∈ F.boundaryFlags) (hit : IsThroughLabel F i) : W.boundaryFlag i ∈ F.throughFlags

A used through-label's flag is a through-flag.