Directed perfect matchings and the rotation of their union

A directed perfect matching is a fixed-point-free involution together with a choice of tail at each edge. Two of them on the same set have a union in which every point carries one arc of each, so the union decomposes into alternating cycles.

When the union is Eulerian — at every point one arc enters and one leaves — the cycles are coherently directed, and following the arc that leaves is a permutation whose cycles are exactly the union's components. That permutation carries the second matching to the first, direction and all, and its sign is (-1) to the number of components, because every component has even length.

This is the sign lemma the Gram identity for mixed partition functions runs on: the product of two matchings' signs is (-1) to the number of components of their union.

structure RS.DirMatching (α : Type) : Type

A directed perfect matching: a fixed-point-free involution with a chosen tail at each edge.

• edge : α → α

  The matched partner.

• edge_invol (a : α) : self.edge (self.edge a) = a

  The partner map is an involution.

• edge_ne (a : α) : self.edge a ≠ a

  No point is its own partner.

• tail : α → Bool

  Whether the arc at this point leaves it.

• tail_flip (a : α) : self.tail (self.edge a) = !self.tail a

  Each arc leaves exactly one of its two ends.

def RS.DirMatching.Alternating {α : Type} (M N : DirMatching α) : Prop

The union is Eulerian: at every point exactly one of the two matchings' arcs leaves it.

Equations

• M.Alternating N = ∀ (a : α), N.tail a = !M.tail a

def RS.DirMatching.rot {α : Type} (M N : DirMatching α) (a : α) : α

The rotation of an Eulerian union: follow the arc that leaves.

Equations

• M.rot N a = if M.tail a = true then M.edge a else N.edge a

def RS.DirMatching.rotInv {α : Type} (M N : DirMatching α) (a : α) : α

The step backwards: follow the arc that enters.

Equations

• M.rotInv N a = if M.tail a = true then N.edge a else M.edge a

theorem RS.DirMatching.tail_edge_alt {α : Type} {M N : DirMatching α} (h : M.Alternating N) (a : α) : M.tail (N.edge a) = !M.tail a

Along an Eulerian union the second matching's tails are the first's, flipped.

theorem RS.DirMatching.tail_rot {α : Type} {M N : DirMatching α} (h : M.Alternating N) (a : α) : M.tail (M.rot N a) = !M.tail a

The rotation lands on the other end of the arc it followed.

theorem RS.DirMatching.rotInv_rot {α : Type} {M N : DirMatching α} (h : M.Alternating N) (a : α) : M.rotInv N (M.rot N a) = a

The rotation is undone by the backward step.

theorem RS.DirMatching.rot_rotInv {α : Type} {M N : DirMatching α} (h : M.Alternating N) (a : α) : M.rot N (M.rotInv N a) = a

And undoes it.

def RS.DirMatching.rotPerm {α : Type} (M N : DirMatching α) (h : M.Alternating N) : Equiv.Perm α

The rotation of an Eulerian union, as a permutation.

Equations

• M.rotPerm N h = { toFun := M.rot N, invFun := M.rotInv N, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RS.DirMatching.rotPerm_apply {α : Type} {M N : DirMatching α} (h : M.Alternating N) (a : α) : (M.rotPerm N h) a = M.rot N a

The rotation permutation acts by following the arc that leaves.

theorem RS.DirMatching.sameCycle_rot_edge {α : Type} {M N : DirMatching α} (h : M.Alternating N) (a : α) : (M.rotPerm N h).SameCycle a (M.edge a)

The rotation reaches the first matching's partner. Together with the next lemma this is the statement that the rotation's orbits are exactly the connected components of the union: one step of the rotation, forwards or backwards, crosses each of the two arcs at a point.

theorem RS.DirMatching.sameCycle_rot_edge' {α : Type} {M N : DirMatching α} (h : M.Alternating N) (a : α) : (M.rotPerm N h).SameCycle a (N.edge a)

The rotation reaches the second matching's partner.

theorem RS.DirMatching.even_card {α : Type} [Fintype α] (M : DirMatching α) : Even (Fintype.card α)

A directed perfect matching forces an even ground set: the partner map exchanges the tails with the heads.

@[reducible, inline]

abbrev RS.DirMatching.Tail {α : Type} (M : DirMatching α) : Type

The tails of a directed matching, as a subtype.

Equations

• M.Tail = { a : α // M.tail a = true }

noncomputable def RS.DirMatching.tailHeadEquiv {α : Type} (M : DirMatching α) : { a : α // ¬M.tail a = true } ≃ { a : α // M.tail a = true }

The partner map exchanges tails and heads.

Equations

• M.tailHeadEquiv = { toFun := fun (a : { a : α // ¬M.tail a = true }) => ⟨M.edge ↑a, ⋯⟩, invFun := fun (a : { a : α // M.tail a = true }) => ⟨M.edge ↑a, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem RS.DirMatching.two_mul_card_tail {α : Type} [Fintype α] (M : DirMatching α) : 2 * Fintype.card M.Tail = Fintype.card α

The ground set is twice the tails.

Symmetries of a directed matching are even

A permutation commuting with the partner map and preserving the tails is determined by its restriction to the tails, and the restriction to the heads is that same permutation conjugated by the partner map. The two restrictions therefore have equal sign, and their product — the whole permutation — has sign one.

structure RS.DirMatching.Stab {α : Type} (M : DirMatching α) (g : Equiv.Perm α) : Prop

A symmetry of a directed matching: it commutes with the partner map and fixes each point's direction.

• edge (a : α) : g (M.edge a) = M.edge (g a)

  It commutes with the partner map.

• tail (a : α) : M.tail (g a) = M.tail a

  It preserves the tails.

theorem RS.DirMatching.sign_of_stab {α : Type} [Fintype α] [DecidableEq α] {M : DirMatching α} {g : Equiv.Perm α} (h : M.Stab g) : Equiv.Perm.sign g = 1

A symmetry of a directed matching is even.

The rotation carries one matching to the other

theorem RS.DirMatching.edge_rot {α : Type} {M N : DirMatching α} (h : M.Alternating N) (a : α) : M.edge (M.rot N a) = M.rot N (N.edge a)

The rotation conjugates the second matching into the first.

theorem RS.DirMatching.tail_rot_eq {α : Type} {M N : DirMatching α} (h : M.Alternating N) (a : α) : M.tail (M.rot N a) = N.tail a

The rotation carries the second matching's directions to the first's.

Its sign counts the components

theorem RS.DirMatching.sign_rotPerm {α : Type} {M N : DirMatching α} [Fintype α] [DecidableEq α] (h : M.Alternating N) (hcard : Even (Fintype.card α)) : ↑↑(Equiv.Perm.sign (M.rotPerm N h)) = (-1) ^ orbitCount (M.rotPerm N h)

The rotation's sign is (-1) to its number of orbits. The orbits are the components of the union, and each has even length, so this is the sign lemma for a matching pair.

Every carrier has the rotation's sign

A permutation carrying one directed matching to the other differs from the rotation by a symmetry of the target, so all carriers share the rotation's sign — and that sign counts the union's components. This is the matching-sign lemma the Gram identity uses.

structure RS.DirMatching.Carries {α : Type} (M N : DirMatching α) (σ : Equiv.Perm α) : Prop

A permutation carrying one directed matching onto another.

• edge (a : α) : σ (N.edge a) = M.edge (σ a)

  It intertwines the two partner maps.

• tail (a : α) : M.tail (σ a) = N.tail a

  It matches the directions.

theorem RS.DirMatching.Carries.edge_symm {α : Type} {M N : DirMatching α} {σ : Equiv.Perm α} (hσ : M.Carries N σ) (a : α) : (Equiv.symm σ) (M.edge a) = N.edge ((Equiv.symm σ) a)

A carrier's inverse intertwines the partner maps the other way.

theorem RS.DirMatching.carries_rotPerm {α : Type} {M N : DirMatching α} (h : M.Alternating N) : M.Carries N (M.rotPerm N h)

The rotation carries.

theorem RS.DirMatching.sign_eq_of_carries_pair {α : Type} {M N : DirMatching α} [Fintype α] [DecidableEq α] {σ τ : Equiv.Perm α} (hσ : M.Carries N σ) (hτ : M.Carries N τ) : Equiv.Perm.sign σ = Equiv.Perm.sign τ

Any two carriers have the same sign. They differ by a symmetry of the target, and symmetries are even. No Eulerian hypothesis is needed: this is what makes a directed matching's sign well defined.

A carrier always exists

RS21 speaks of "a permutation that sends M(ω,κ) to the standard matching" without exhibiting one. Any bijection between the two matchings' tails extends over the partner maps to a carrier, and the tails are half the ground set on both sides, so such a bijection exists whenever the ground sets agree.

noncomputable def RS.DirMatching.ofTailEquiv {α : Type} (M N : DirMatching α) (b : N.Tail ≃ M.Tail) : Equiv.Perm α

The carrier built from a bijection of tails: send a tail where the bijection does, and a head to the partner of its tail's image.

Equations

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

theorem RS.DirMatching.carries_ofTailEquiv {α : Type} (M N : DirMatching α) (b : N.Tail ≃ M.Tail) : M.Carries N (M.ofTailEquiv N b)

The tail bijection's extension carries.

theorem RS.DirMatching.exists_carries {α : Type} [Finite α] (M N : DirMatching α) : ∃ (σ : Equiv.Perm α), M.Carries N σ

A carrier exists between any two directed matchings on the same set.

The sign of a directed matching

RS21 fixes a reference matching — the one with arcs (i₁,i₂),…,(i_{|S|−1},i_{|S|}) — and takes a matching's sign to be that of any permutation carrying it to the reference. Well definedness is sign_eq_of_carries_pair. What the Gram identity uses is not the sign itself but the product of two of them, and that product is the sign of a carrier between them — independent of which reference was fixed.

theorem RS.DirMatching.Carries.comp {α : Type} {M N P : DirMatching α} {σ τ : Equiv.Perm α} (hσ : M.Carries N σ) (hτ : N.Carries P τ) : M.Carries P (σ * τ)

Carriers compose.

theorem RS.DirMatching.Carries.inv {α : Type} {M N : DirMatching α} {σ : Equiv.Perm α} (hσ : M.Carries N σ) : N.Carries M σ⁻¹

Carriers invert.

noncomputable def RS.DirMatching.sgnRel {α : Type} [Fintype α] [DecidableEq α] (R M : DirMatching α) : ℤˣ

The sign of a directed matching against a reference.

Equations

• R.sgnRel M = Equiv.Perm.sign (Classical.choose ⋯)

theorem RS.DirMatching.sgnRel_eq_of_carries {α : Type} [Fintype α] [DecidableEq α] (R M : DirMatching α) {σ : Equiv.Perm α} (hσ : R.Carries M σ) : R.sgnRel M = Equiv.Perm.sign σ

The sign is that of any carrier to the reference.

theorem RS.DirMatching.sgnRel_mul_sgnRel {α : Type} [Fintype α] [DecidableEq α] (R M N : DirMatching α) {σ : Equiv.Perm α} (hσ : M.Carries N σ) : R.sgnRel M * R.sgnRel N = Equiv.Perm.sign σ

The product of two matchings' signs is the sign of a carrier between them, whatever reference was fixed.

The interface matching

Composing two fragments identifies each label of the first with the same label of the second. On the labels that is a directed perfect matching in its own right — the one RS21 pairs with the chord matching to form the union whose components count the circuits the gluing closes.

def RS.DirMatching.interfaceMatching (γ : Type) : DirMatching (γ ⊕ γ)

The interface matching: each label of one side paired with the same label of the other.

Equations

• RS.DirMatching.interfaceMatching γ = { edge := Sum.swap, edge_invol := ⋯, edge_ne := ⋯, tail := Sum.isLeft, tail_flip := ⋯ }

@[simp]

theorem RS.DirMatching.interfaceMatching_edge {γ : Type} (x : γ ⊕ γ) : (interfaceMatching γ).edge x = x.swap

The interface matching pairs a label with its copy on the other side.

@[simp]

theorem RS.DirMatching.interfaceMatching_tail {γ : Type} (x : γ ⊕ γ) : (interfaceMatching γ).tail x = x.isLeft

Its arcs are directed out of the left side.

The standard matching

RS21 fixes the matching with arcs (i₁,i₂),…,(i_{|S|−1},i_{|S|}) on S = {i₁ < ⋯ < i_{|S|}}. On Fin (2m) that is the pairing of 2j with 2j+1, directed upward; on any linearly ordered set of even size it is that one transported along the order isomorphism.

def RS.DirMatching.map {α β : Type} (e : α ≃ β) (M : DirMatching α) : DirMatching β

Transport a directed matching along an equivalence.

Equations

• RS.DirMatching.map e M = { edge := fun (b : β) => e (M.edge (e.symm b)), edge_invol := ⋯, edge_ne := ⋯, tail := fun (b : β) => M.tail (e.symm b), tail_flip := ⋯ }

def RS.DirMatching.finStd (m : ℕ) : DirMatching (Fin (2 * m))

The standard directed matching on Fin (2m): 2j paired with 2j+1, directed upward.

Equations

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

noncomputable def RS.DirMatching.stdMatching {α : Type} [LinearOrder α] [Fintype α] {m : ℕ} (hcard : Fintype.card α = 2 * m) : DirMatching α

The standard directed matching on a linearly ordered set of even size.

Equations

• RS.DirMatching.stdMatching hcard = RS.DirMatching.map (monoEquivOfFin α hcard).toEquiv (RS.DirMatching.finStd m)

Transporting a matching

The two fragments of a composition carry matchings on their own used labels. Comparing them means transporting one along the bijection the shared labelling gives, and the sign against a transported reference is unchanged.

theorem RS.DirMatching.carries_map {α β : Type} (e : α ≃ β) {R M : DirMatching α} {σ : Equiv.Perm α} (hσ : R.Carries M σ) : (map e R).Carries (map e M) (e.permCongr σ)

A carrier transports along a bijection.

theorem RS.DirMatching.map_map {α β γ : Type} (e : α ≃ β) (f : β ≃ γ) (M : DirMatching α) : map f (map e M) = map (e.trans f) M

Transport composes.

theorem RS.DirMatching.sgnRel_map {α : Type} [Fintype α] [DecidableEq α] {β : Type} [Fintype β] [DecidableEq β] (e : α ≃ β) (R M : DirMatching α) : (map e R).sgnRel (map e M) = R.sgnRel M

The sign is unchanged by transport.

theorem RS.DirMatching.stdMatching_map {α : Type} [LinearOrder α] [Fintype α] {β : Type} [LinearOrder β] [Fintype β] (e : α ≃o β) {m : ℕ} (h : Fintype.card α = 2 * m) (h' : Fintype.card β = 2 * m) : map e.toEquiv (stdMatching h) = stdMatching h'

The standard matching is natural in the order.

theorem RS.DirMatching.sgnRel_mul_sgnRel_map {α : Type} [LinearOrder α] [Fintype α] {β : Type} [LinearOrder β] [Fintype β] (e : α ≃o β) {m : ℕ} (h : Fintype.card α = 2 * m) (h' : Fintype.card β = 2 * m) (M : DirMatching α) (N : DirMatching β) {σ : Equiv.Perm α} (hσ : M.Carries (map e.symm.toEquiv N) σ) : (stdMatching h).sgnRel M * (stdMatching h').sgnRel N = Equiv.Perm.sign σ

The two fragments' signs, on a common reference. With the second matching transported along an order isomorphism of the two used-label sets, the product of the two signs is the sign of a carrier between them — reference-free, as RS21's Lemma 11 needs.

theorem RS.DirMatching.sgnRel_mul_sgnRel_map_alternating {α : Type} [LinearOrder α] [Fintype α] {β : Type} [LinearOrder β] [Fintype β] (e : α ≃o β) {m : ℕ} (h : Fintype.card α = 2 * m) (h' : Fintype.card β = 2 * m) (M : DirMatching α) (N : DirMatching β) (halt : M.Alternating (map e.symm.toEquiv N)) : ↑↑((stdMatching h).sgnRel M * (stdMatching h').sgnRel N) = (-1) ^ orbitCount (M.rotPerm (map e.symm.toEquiv N) halt)

RS21's Lemma 11 for a composition: with the union of the two fragments' matchings Eulerian, the product of their signs is (-1) to the number of components of that union.

Reversing one arc

RS21's invariance (12) turns on the observation that inverting a directed trail changes M(ω,κ) by reversing the direction of one arc, and that this flips the matching's sign. Reversing an arc composes any carrier with the transposition of that arc's two ends.

def RS.DirMatching.reverseArc {α : Type} [DecidableEq α] (M : DirMatching α) (a : α) : DirMatching α

Reverse the direction of one arc, leaving the pairing alone.

Equations

• M.reverseArc a = { edge := M.edge, edge_invol := ⋯, edge_ne := ⋯, tail := fun (b : α) => if b = a ∨ b = M.edge a then !M.tail b else M.tail b, tail_flip := ⋯ }

theorem RS.DirMatching.reverseArc_tail {α : Type} [DecidableEq α] (M : DirMatching α) (a b : α) : (M.reverseArc a).tail b = if b = a ∨ b = M.edge a then !M.tail b else M.tail b

The reversed matching's directions, pointwise.

theorem RS.DirMatching.swap_edge_comm {α : Type} [DecidableEq α] (M : DirMatching α) (a b : α) : (Equiv.swap a (M.edge a)) (M.edge b) = M.edge ((Equiv.swap a (M.edge a)) b)

The arc-reversing transposition commutes with the pairing.

theorem RS.DirMatching.carries_reverseArc {α : Type} {M R : DirMatching α} [DecidableEq α] {σ : Equiv.Perm α} (hσ : R.Carries M σ) (a : α) : R.Carries (M.reverseArc a) (σ * Equiv.swap a (M.edge a))

A carrier for the reversed matching: compose with the transposition of the reversed arc's two ends.

theorem RS.DirMatching.sgnRel_reverseArc {α : Type} [Fintype α] [DecidableEq α] (R M : DirMatching α) (a : α) : R.sgnRel (M.reverseArc a) = -R.sgnRel M

Reversing an arc flips the sign — RS21's sgn(M(ω,κ)) = -sgn(M(ω′,κ′)).

theorem RS.DirMatching.ext {α : Type} {M N : DirMatching α} (he : M.edge = N.edge) (ht : M.tail = N.tail) : M = N

Two directed matchings agreeing on partners and directions are equal.

Lemma 11 in general

RS21's Lemma 11 reads the sign of a permutation carrying one directed matching to another as (-1)^{c(M∪N)+o(M∪N)}, where o(M∪N) is the parity of the number of arcs that must be reversed to make the union Eulerian. The Eulerian case above is o = 0; RS21 reduces to it by (12), which is available for a directed trail but not for an edge joining two labels directly, so the general case is what a fragment's matchings need.

The general case follows from the Eulerian one by reversing arcs. Two matchings with the same pairing differ on a set of points closed under that pairing — a set of whole arcs — and reversing those arcs one at a time carries one to the other, flipping the sign each time.

def RS.DirMatching.flipSet {α : Type} [Fintype α] (P P' : DirMatching α) : Finset α

The points at which two matchings disagree on direction.

Equations

• P.flipSet P' = {a : α | P'.tail a ≠ P.tail a}

theorem RS.DirMatching.mem_flipSet {α : Type} [Fintype α] {P P' : DirMatching α} {a : α} : a ∈ P.flipSet P' ↔ P'.tail a ≠ P.tail a

Membership in the disagreement set.

theorem RS.DirMatching.edge_mem_flipSet {α : Type} [Fintype α] {P P' : DirMatching α} (he : P'.edge = P.edge) {a : α} (ha : a ∈ P.flipSet P') : P.edge a ∈ P.flipSet P'

The disagreement set is a set of whole arcs: matchings with the same pairing disagree at both ends of an arc or at neither.

theorem RS.DirMatching.even_card_flipSet {α : Type} [Fintype α] {P P' : DirMatching α} (he : P'.edge = P.edge) : Even (P.flipSet P').card

The disagreement set has an even number of points.

theorem RS.DirMatching.flipSet_reverseArc {α : Type} [Fintype α] [DecidableEq α] {P P' : DirMatching α} (he : P'.edge = P.edge) {a : α} (ha : a ∈ P.flipSet P') : (P.reverseArc a).flipSet P' = P.flipSet P' \ {a, P.edge a}

Reversing an arc removes it from the disagreement set and leaves the rest alone.

Repairing a union to Eulerian position

RS21 puts the union of two matchings into Eulerian position before applying Lemma 11, by reversing arcs of each. Such a repair always exists: reversing arcs is free to choose a direction at each point, subject only to the two arcs at a point pointing opposite ways, so a repair is exactly a two-colouring of the union — a T : α → Bool flipped by both pairings.

The union of two fixed-point-free involutions is a disjoint union of cycles of even length, so it is two-colourable, and the colouring is built here without decomposing into cycles. Write p for the composite of the two pairings. A colouring is a function constant on p-cycles that the first pairing flips, so it is a choice of one cycle from each pair {C, e₁C} — and those two cycles are always distinct, by the dihedral relation e₁ p e₁ = p⁻¹ together with the fixed-point-freeness of both pairings.

def RS.DirMatching.edgePerm {α : Type} (M : DirMatching α) : Equiv.Perm α

The pairing of a matching, as a permutation.

Equations

• M.edgePerm = { toFun := M.edge, invFun := M.edge, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RS.DirMatching.edgePerm_apply {α : Type} (M : DirMatching α) (a : α) : M.edgePerm a = M.edge a

The pairing permutation acts by the partner map.

theorem RS.DirMatching.edgePerm_inv {α : Type} (M : DirMatching α) : M.edgePerm⁻¹ = M.edgePerm

A pairing is its own inverse.

theorem RS.DirMatching.inv_edgePerm_mul {α : Type} (M N : DirMatching α) : (N.edgePerm * M.edgePerm)⁻¹ = M.edgePerm * N.edgePerm

The composite of two pairings inverts by taking them in the other order.

theorem RS.DirMatching.edgePerm_conj {α : Type} (M N : DirMatching α) (i : ℤ) : M.edgePerm * (N.edgePerm * M.edgePerm) ^ i * M.edgePerm = (N.edgePerm * M.edgePerm) ^ (-i)

The dihedral relation: conjugating the composite by either pairing inverts it.

theorem RS.DirMatching.not_sameCycle_edge {α : Type} (M N : DirMatching α) (a : α) : ¬(N.edgePerm * M.edgePerm).SameCycle a (M.edge a)

The cycle of a point and the cycle of its partner are distinct. Were they the same, the dihedral relation would place a fixed point of one of the two pairings on that cycle: at the midpoint of the displacement when it is even, one step further when it is odd. This is the even length of the union's cycles, in the only form the repair needs.

noncomputable def RS.DirMatching.cycleOf {α : Type} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (a : α) : Finset α

The cycle of a point, as a finset.

Equations

• RS.DirMatching.cycleOf p a = {x : α | p.SameCycle a x}

theorem RS.DirMatching.mem_cycleOf {α : Type} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {a x : α} : x ∈ cycleOf p a ↔ p.SameCycle a x

Membership in a cycle: being on the same cycle as the base point.

theorem RS.DirMatching.self_mem_cycleOf {α : Type} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (a : α) : a ∈ cycleOf p a

A point lies on its own cycle.

theorem RS.DirMatching.cycleOf_eq {α : Type} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {a b : α} (h : p.SameCycle a b) : cycleOf p a = cycleOf p b

Points on one cycle have the same cycle.

noncomputable def RS.DirMatching.cycleKey {α : Type} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) (a : α) : Fin (Fintype.card α)

The key of a cycle: the least index of a point on it.

Equations

• RS.DirMatching.cycleKey p a = (Finset.image (⇑(Fintype.equivFin α)) (RS.DirMatching.cycleOf p a)).min' ⋯

theorem RS.DirMatching.cycleKey_eq {α : Type} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {a b : α} (h : p.SameCycle a b) : cycleKey p a = cycleKey p b

Points on the same cycle have the same key, so the key names the cycle.

theorem RS.DirMatching.sameCycle_of_cycleKey_eq {α : Type} [Fintype α] [DecidableEq α] {p : Equiv.Perm α} {a b : α} (h : cycleKey p a = cycleKey p b) : p.SameCycle a b

Distinct cycles have distinct keys: a key is attained on its own cycle, and two cycles sharing a point coincide.

theorem RS.DirMatching.exists_alternating_repair {α : Type} [Finite α] (M N : DirMatching α) : ∃ (M' : DirMatching α) (N' : DirMatching α), M'.edge = M.edge ∧ N'.edge = N.edge ∧ M'.Alternating N'

Any two matchings admit a common repair to Eulerian position — RS21's σ₁ and σ₂. The repair leaves both pairings alone and makes the union alternating.

theorem RS.DirMatching.tail_ne_of_alternating {α : Type} {M N : DirMatching α} (h : M.Alternating N) {i j : α} (hN : N.edge i = j) : M.tail j = !M.tail i

The direction hypothesis is automatic along an arc of the interface matching: the union being Eulerian at the two identified labels is exactly what the contraction needs.

Contracting a matching at an identified pair

Gluing one interface pair identifies two labels. On the chord matching that is a contraction: the two labels are removed and their partners are matched to one another, which is the same rewiring the flag model performs on the edge pairing.

The contraction is defined when the two identified labels are not already partners. When they are, gluing closes a circuit instead, and the two labels simply disappear — that dichotomy is what makes the circuit count go up by one exactly once per component of the union.

Directions contract only when the two identified labels carry opposite ones, which is RS21's requirement that the two Eulerian orientations induce an Eulerian orientation of the glued subset.

@[reducible, inline]

abbrev RS.DirMatching.Surviving {α : Type} (i j : α) : Type

The points surviving the identification of i and j.

Equations

• RS.DirMatching.Surviving i j = { x : α // x ≠ i ∧ x ≠ j }

theorem RS.DirMatching.rot_rot_of_interface {α : Type} {M N : DirMatching α} (h : M.Alternating N) {i j : α} (hN : N.edge i = j) (x : Surviving i j) (hs : M.rot N ↑x = i ∨ M.rot N ↑x = j) : M.rot N (M.rot N ↑x) = i ∨ M.rot N (M.rot N ↑x) = j

An excursion through the identified pair has length two.

def RS.DirMatching.contractEdge {α : Type} [DecidableEq α] (M : DirMatching α) (i j x : α) : α

The contracted partner map: the partners of the two identified points are matched to one another.

Equations

• M.contractEdge i j x = if M.edge x = i then M.edge j else if M.edge x = j then M.edge i else M.edge x

theorem RS.DirMatching.contractEdge_congr {α : Type} [DecidableEq α] {M M' : DirMatching α} (h : M'.edge = M.edge) (i j x : α) : M'.contractEdge i j x = M.contractEdge i j x

The contracted partner map reads only the pairing.

theorem RS.DirMatching.contractEdge_ne {α : Type} [DecidableEq α] (M : DirMatching α) {i j : α} (hopen : M.edge i ≠ j) (x : α) : M.contractEdge i j x ≠ i ∧ M.contractEdge i j x ≠ j

The contracted partner map avoids the two identified points: they are gone from the contracted set.

theorem RS.DirMatching.contractEdge_invol {α : Type} [DecidableEq α] (M : DirMatching α) {i j : α} (hij : i ≠ j) (x : α) (hx : x ≠ i) (hx' : x ≠ j) : M.contractEdge i j (M.contractEdge i j x) = x

It is an involution on the survivors.

theorem RS.DirMatching.contractEdge_ne_self {α : Type} [DecidableEq α] (M : DirMatching α) {i j : α} (hij : i ≠ j) (x : α) : M.contractEdge i j x ≠ x

And fixed-point-free, so it is again a perfect matching.

def RS.DirMatching.contract {α : Type} [DecidableEq α] (M : DirMatching α) {i j : α} (hij : i ≠ j) (hopen : M.edge i ≠ j) (hdir : M.tail j = !M.tail i) : DirMatching (Surviving i j)

The contraction of a matching at an identified pair. The two identified points must carry opposite directions, which is what makes the contracted directions consistent — RS21's requirement that the two Eulerian orientations induce an Eulerian orientation of the glued subset.

Equations

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

The interface matching after one identification

Gluing one interface pair consumes one arc of the interface matching and contracts the chord matching at its two ends. The remaining interface arcs restrict to the surviving labels, and the union of the two matchings stays Eulerian, so the step can be iterated.

def RS.DirMatching.restrict {α : Type} (N : DirMatching α) {i j : α} (hN : N.edge i = j) : DirMatching (Surviving i j)

The interface matching restricted to the labels surviving the identification of one of its own arcs.

Equations

• N.restrict hN = { edge := fun (x : RS.DirMatching.Surviving i j) => ⟨N.edge ↑x, ⋯⟩, edge_invol := ⋯, edge_ne := ⋯, tail := fun (x : RS.DirMatching.Surviving i j) => N.tail ↑x, tail_flip := ⋯ }

theorem RS.DirMatching.alternating_contract {α : Type} [DecidableEq α] {M N : DirMatching α} (h : M.Alternating N) {i j : α} (hij : i ≠ j) (hN : N.edge i = j) (hopen : M.edge i ≠ j) : (M.contract hij hopen ⋯).Alternating (N.restrict hN)

The union stays Eulerian after one identification.

One step of the contracted rotation

One step of the contracted rotation is one or three steps of the original: the contraction short-circuits the two identified labels, so a step that would have landed on one of them instead continues past both. Either way the step stays inside a single orbit of the original rotation, which is what carries orbits across the contraction.

theorem RS.DirMatching.sameCycle_rot_contract {α : Type} [DecidableEq α] {M N : DirMatching α} (h : M.Alternating N) {i j : α} (hij : i ≠ j) (hN : N.edge i = j) (hopen : M.edge i ≠ j) (x : Surviving i j) : (M.rotPerm N h).SameCycle ↑x ↑(((M.contract hij hopen ⋯).rotPerm (N.restrict hN) ⋯) x)

A contracted step stays in one orbit of the original rotation.

theorem RS.DirMatching.sameCycle_of_contract {α : Type} [DecidableEq α] {M N : DirMatching α} (h : M.Alternating N) {i j : α} (hij : i ≠ j) (hN : N.edge i = j) (hopen : M.edge i ≠ j) {x y : Surviving i j} (hxy : ((M.contract hij hopen ⋯).rotPerm (N.restrict hN) ⋯).SameCycle x y) : (M.rotPerm N h).SameCycle ↑x ↑y

The contraction's orbits map to the original's.

The contracted rotation is the original, short-circuited

A survivor whose rotation step lands on a surviving point takes the same step in the contraction. A survivor whose step lands on one of the two identified points is carried three steps instead: through both of them and out the far side. Those are the only two cases, and together they say the contracted rotation is the original with the identified pair skipped.

theorem RS.DirMatching.rot_contract_val {α : Type} {M N : DirMatching α} [DecidableEq α] (h : M.Alternating N) {i j : α} (hij : i ≠ j) (hN : N.edge i = j) (hopen : M.edge i ≠ j) (x : Surviving i j) : ↑(((M.contract hij hopen ⋯).rotPerm (N.restrict hN) ⋯) x) = if M.tail ↑x = true then M.contractEdge i j ↑x else N.edge ↑x

The rotation's step at a survivor, in the contraction.

theorem RS.DirMatching.rot_contract_eq_rot {α : Type} {M N : DirMatching α} [DecidableEq α] (h : M.Alternating N) {i j : α} (hij : i ≠ j) (hN : N.edge i = j) (hopen : M.edge i ≠ j) (x : Surviving i j) (hs : M.rot N ↑x ≠ i) (hs' : M.rot N ↑x ≠ j) : ↑(((M.contract hij hopen ⋯).rotPerm (N.restrict hN) ⋯) x) = M.rot N ↑x

A step landing on a survivor is unchanged.

theorem RS.DirMatching.rot_contract_eq_rot_three {α : Type} {M N : DirMatching α} [DecidableEq α] (h : M.Alternating N) {i j : α} (hij : i ≠ j) (hN : N.edge i = j) (hopen : M.edge i ≠ j) (x : Surviving i j) (hs : M.rot N ↑x = i ∨ M.rot N ↑x = j) : ↑(((M.contract hij hopen ⋯).rotPerm (N.restrict hN) ⋯) x) = M.rot N (M.rot N (M.rot N ↑x))

A step landing on an identified point runs three steps.

The converse: the contraction loses no orbits

A rotation path between two survivors passes through the identified pair only in excursions of length two, and the contraction takes each such excursion in a single step. So survivors joined by the original rotation are joined by the contracted one, and together with the forward direction the two rotations have the same orbits.

noncomputable def RS.DirMatching.pickSurvivor {α : Type} [DecidableEq α] (M : DirMatching α) {i j : α} (hopen : M.edge i ≠ j) (a : α) : Surviving i j

The survivor standing for a point: itself where it survives, and otherwise the partner of the first identified label, which lies on the same orbit as both of them.

Equations

• M.pickSurvivor hopen a = if ha : a ≠ i ∧ a ≠ j then ⟨a, ha⟩ else ⟨M.edge i, ⋯⟩

theorem RS.DirMatching.sameCycle_pickSurvivor {α : Type} {M N : DirMatching α} [DecidableEq α] (h : M.Alternating N) {i j : α} (hN : N.edge i = j) (hopen : M.edge i ≠ j) (a : α) : (M.rotPerm N h).SameCycle a ↑(M.pickSurvivor hopen a)

A point and the survivor standing for it lie on the same cycle of the rotation, so the choice does not move between components.

theorem RS.DirMatching.sameCycle_contract_of_sameCycle {α : Type} {M N : DirMatching α} [Finite α] [DecidableEq α] (h : M.Alternating N) {i j : α} (hij : i ≠ j) (hN : N.edge i = j) (hopen : M.edge i ≠ j) {x y : Surviving i j} (hxy : (M.rotPerm N h).SameCycle ↑x ↑y) : ((M.contract hij hopen ⋯).rotPerm (N.restrict hN) ⋯).SameCycle x y

Survivors joined by the original rotation are joined by the contracted one.

An open glue step preserves the orbit count

The two directions together say the contraction's orbits are the original's, so gluing a pair whose two labels are not already partners changes neither the components of the union nor their number. That is the half of RS21's circuit-count bookkeeping in which no circuit closes.

noncomputable def RS.DirMatching.orbitsEquivContract {α : Type} {M N : DirMatching α} [Fintype α] [DecidableEq α] (h : M.Alternating N) {i j : α} (hij : i ≠ j) (hN : N.edge i = j) (hopen : M.edge i ≠ j) : Orbits ((M.contract hij hopen ⋯).rotPerm (N.restrict hN) ⋯) ≃ Orbits (M.rotPerm N h)

The contraction has the same orbits.

Equations

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

theorem RS.DirMatching.orbitCount_contract {α : Type} {M N : DirMatching α} [Fintype α] [DecidableEq α] (h : M.Alternating N) {i j : α} (hij : i ≠ j) (hN : N.edge i = j) (hopen : M.edge i ≠ j) : orbitCount ((M.contract hij hopen ⋯).rotPerm (N.restrict hN) ⋯) = orbitCount (M.rotPerm N h)

An open glue step preserves the number of components.

A closed glue step closes one circuit

When the two identified labels are already partners in the chord matching, they form a component of the union by themselves: the rotation carries each to the other and nothing else meets them. Gluing that pair closes it into a circuit and removes it, so the number of components drops by exactly one. This is the other half of RS21's circuit-count bookkeeping, and the only half in which a circuit appears.

theorem RS.DirMatching.rot_closed {α : Type} {M N : DirMatching α} {i j : α} (hM : M.edge i = j) (hN : N.edge i = j) : M.rot N i = j ∧ M.rot N j = i

The rotation carries each identified label to the other.

theorem RS.DirMatching.rot_survivor_closed {α : Type} {M N : DirMatching α} {i j : α} (hM : M.edge i = j) (hN : N.edge i = j) (x : Surviving i j) : M.rot N ↑x ≠ i ∧ M.rot N ↑x ≠ j

Nothing outside the identified pair meets it.

theorem RS.DirMatching.rotPerm_restrict {α : Type} {M N : DirMatching α} (h : M.Alternating N) {i j : α} (hM : M.edge i = j) (hN : N.edge i = j) (x : Surviving i j) : ↑(((M.restrict hM).rotPerm (N.restrict hN) ⋯) x) = M.rot N ↑x

The restricted rotation is the rotation restricted.

theorem RS.DirMatching.rot_surviving_iff {α : Type} {M N : DirMatching α} (h : M.Alternating N) {i j : α} (hM : M.edge i = j) (hN : N.edge i = j) (x : α) : (M.rotPerm N h) x ≠ i ∧ (M.rotPerm N h) x ≠ j ↔ x ≠ i ∧ x ≠ j

The identified pair is invariant under the rotation, and so is its complement.

theorem RS.DirMatching.orbitCount_pair {α : Type} {M N : DirMatching α} [Fintype α] [DecidableEq α] (h : M.Alternating N) {i j : α} (hM : M.edge i = j) (hN : N.edge i = j) : orbitCount ((M.rotPerm N h).subtypePerm ⋯) = 1

The rotation restricted to the identified pair has one orbit.

theorem RS.DirMatching.orbitCount_restrict_closed {α : Type} {M N : DirMatching α} [Fintype α] [DecidableEq α] (h : M.Alternating N) {i j : α} (hM : M.edge i = j) (hN : N.edge i = j) : orbitCount ((M.restrict hM).rotPerm (N.restrict hN) ⋯) + 1 = orbitCount (M.rotPerm N h)

A closed glue step closes exactly one circuit.

The component count ignores the directions

The rotation depends on which arc leaves each point, but its orbits do not: one step of either rotation crosses one of the two arcs at a point, and both arcs are visible to the other rotation as well. So the number of components of the union is a function of the two pairings alone.

This is what lets a matching be transported across a construction that changes the directions — a glue, say, which can turn a label into a through-label and so flip the convention that fixes its direction — as long as the pairings correspond.

theorem RS.DirMatching.orbitCount_rotPerm_congr {α : Type} [Fintype α] [DecidableEq α] {M₁ N₁ M₂ N₂ : DirMatching α} (h₁ : M₁.Alternating N₁) (h₂ : M₂.Alternating N₂) (heM : M₁.edge = M₂.edge) (heN : N₁.edge = N₂.edge) : orbitCount (M₁.rotPerm N₁ h₁) = orbitCount (M₂.rotPerm N₂ h₂)

The number of components does not depend on the directions.

The glue steps, stated on the pairings alone

The transport from a fragment supplies matchings whose pairings are the contraction's but whose directions come from whatever convention the glued object uses. Since the component count ignores the directions, the two steps can be stated that way, and the transport then has only the pairings to check.

theorem RS.DirMatching.orbitCount_contract_congr {α : Type} [Fintype α] [DecidableEq α] {M N : DirMatching α} (h : M.Alternating N) {i j : α} (hij : i ≠ j) (hN : N.edge i = j) (hopen : M.edge i ≠ j) {M' N' : DirMatching (Surviving i j)} (h' : M'.Alternating N') (heM : M'.edge = (M.contract hij hopen ⋯).edge) (heN : N'.edge = (N.restrict hN).edge) : orbitCount (M'.rotPerm N' h') = orbitCount (M.rotPerm N h)

An open glue step, with arbitrary directions.

theorem RS.DirMatching.orbitCount_restrict_closed_congr {α : Type} [Fintype α] [DecidableEq α] {M N : DirMatching α} (h : M.Alternating N) {i j : α} (hM : M.edge i = j) (hN : N.edge i = j) {M' N' : DirMatching (Surviving i j)} (h' : M'.Alternating N') (heM : M'.edge = (M.restrict hM).edge) (heN : N'.edge = (N.restrict hN).edge) : orbitCount (M'.rotPerm N' h') + 1 = orbitCount (M.rotPerm N h)

A closed glue step, with arbitrary directions.

theorem RS.DirMatching.orbitCount_map {α : Type} [Fintype α] [DecidableEq α] {β : Type} [Fintype β] [DecidableEq β] (e : α ≃ β) {M N : DirMatching α} (h : M.Alternating N) (h' : (map e M).Alternating (map e N)) : orbitCount ((map e M).rotPerm (map e N) h') = orbitCount (M.rotPerm N h)

Transporting a pair of matchings along a bijection conjugates the rotation, so the component count is unchanged.

theorem RS.DirMatching.map_edge {α β : Type} (e : α ≃ β) (M : DirMatching α) (b : β) : (map e M).edge b = e (M.edge (e.symm b))

The transported matching's partner map, conjugated by the equivalence.

theorem RS.DirMatching.map_edge_congr {α β : Type} (e : α ≃ β) {M M' : DirMatching α} (h : M'.edge = M.edge) : (map e M').edge = (map e M).edge

Transported matchings have the same pairing when the originals do.

theorem RS.DirMatching.alternating_map {α β : Type} (e : α ≃ β) {M N : DirMatching α} (h : M.Alternating N) : (map e M).Alternating (map e N)

Transporting a pair of matchings preserves the Eulerian condition.

theorem RS.DirMatching.contractEdge_of_closed {α : Type} [DecidableEq α] (M : DirMatching α) {i j : α} (hM : M.edge i = j) (x : α) (hx : x ≠ i) (hx' : x ≠ j) : M.contractEdge i j x = M.edge x

At a closed pair the contraction is the plain restriction: no surviving point has either identified label as its partner.

The component count of a union

RS21's c(M ∪ N) is the number of connected components of the union of two directed matchings, and the union has those components whatever the directions are: the repair to Eulerian position exists and the count does not depend on which one is taken. Naming the count that way removes the Eulerian position from every statement that only reads it — and that is most of them, the position mattering only where the signs do.

noncomputable def RS.DirMatching.unionCount {α : Type} [Fintype α] (M N : DirMatching α) : ℕ

The number of components of the union of two matchings — RS21's c(M ∪ N), read at any repair to Eulerian position. It carries no decidability instance: on a sum type the ambient one is the sum's own, which is not the one a linear order supplies, and the two would not match where the recursion compares them.

Equations

• M.unionCount N = RS.orbitCount (⋯.choose.rotPerm ⋯.choose ⋯)

theorem RS.DirMatching.unionCount_eq_orbitCount {α : Type} [Fintype α] [DecidableEq α] {M N M' N' : DirMatching α} (h' : M'.Alternating N') (heM : M'.edge = M.edge) (heN : N'.edge = N.edge) : M.unionCount N = orbitCount (M'.rotPerm N' h')

The count is what any Eulerian pair with the same pairings counts.

theorem RS.DirMatching.unionCount_congr {α : Type} [Fintype α] {M₁ N₁ M₂ N₂ : DirMatching α} (heM : M₁.edge = M₂.edge) (heN : N₁.edge = N₂.edge) : M₁.unionCount N₁ = M₂.unionCount N₂

The count depends on the pairings alone.

theorem RS.DirMatching.unionCount_of_isEmpty {α : Type} [Fintype α] [IsEmpty α] (M N : DirMatching α) : M.unionCount N = 0

An empty ground set has no components.

theorem RS.DirMatching.unionCount_map {α : Type} [Fintype α] {β : Type} [Fintype β] (e : α ≃ β) (M N : DirMatching α) : (map e M).unionCount (map e N) = M.unionCount N

The count survives a relabelling of the ground set.

theorem RS.DirMatching.sgnRel_mul_sgnRel_of_alternating {γ δ : Type} [LinearOrder γ] [LinearOrder δ] [Fintype γ] [Fintype δ] (E : γ ≃o δ) {m : ℕ} (hc : Fintype.card γ = 2 * m) (hc' : Fintype.card δ = 2 * m) (M : DirMatching γ) (N : DirMatching δ) (halt : ∀ (a : γ), N.tail (E a) = !M.tail a) : ↑↑((stdMatching hc).sgnRel M) * ↑↑((stdMatching hc').sgnRel N) = (-1) ^ M.unionCount (map E.symm.toEquiv N)

Lemma 11 across an identification: two matchings whose directions are opposite along an order isomorphism have signs multiplying to (-1) to the number of components of their union.

The union read across a two-sided interface

RS21 reads M(ω₁,κ₁) ∪ M(ω₂,κ₂) on one copy of the label set S, the two fragments' arcs sharing their ends. The flag model keeps the two fragments' labels apart, so the same union is read on the sum: the two chord matchings side by side, against the matching that identifies the two copies. The two readings count the same components — one step of the one-copy rotation is one or three steps of the two-copy one, and the two copies of a label always lie on a common component.

def RS.DirMatching.sumMatching {γ δ : Type} (M : DirMatching γ) (N : DirMatching δ) : DirMatching (γ ⊕ δ)

Two matchings, side by side.

Equations

• M.sumMatching N = { edge := Sum.map M.edge N.edge, edge_invol := ⋯, edge_ne := ⋯, tail := Sum.elim M.tail N.tail, tail_flip := ⋯ }

def RS.DirMatching.interfaceEquivMatching {γ δ : Type} (e : γ ≃ δ) : DirMatching (γ ⊕ δ)

The interface matching across an identification of the two sides' labels.

Equations

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

theorem RS.DirMatching.unionCount_sumMatching {γ δ : Type} [Fintype γ] [Fintype δ] (e : γ ≃ δ) (M₁ : DirMatching γ) (M₂ : DirMatching δ) : (M₁.sumMatching M₂).unionCount (interfaceEquivMatching e) = M₁.unionCount (map e.symm M₂)

The union on two copies counts what the union on one copy counts.