Existence of transition systems with orientations

Every Eulerian edge subset whose participating flags all attach to internal vertices admits a transition system equipped with an orientation. The construction proceeds in two parts:

1. The matching κ (Part 1): at each vertex the participating flags have even cardinality (from the Eulerian condition); a fixed-point-free involution matching flags at common vertices is built by the finite combinatorial lemma exists_involution_of_even, applied per-vertex and glued into a global function.

2. The orientation (Part 2): the edge pairing σ conjugates the walk permutation to its inverse; this forces the walk-orbit of f and of σ f to be disjoint for every participating f. An orientation is obtained by choosing, for each orbit-pair, one side as "out" using orbit representatives under the flag order.

The involution lemma

theorem RS.exists_involution_of_even {β : Type} (s : Finset β) (hs : Even s.card) : ∃ (m : β → β), (∀ x ∈ s, m x ∈ s) ∧ (∀ x ∈ s, m (m x) = x) ∧ ∀ x ∈ s, m x ≠ x

A finset of even cardinality admits a fixed-point-free involution mapping the set to itself. Proved by strong induction on the finset: for cardinality 0 the properties are vacuous; for cardinality ≥ 2 pick two distinct elements, match them, and recurse on the remainder.

Part 1: constructing the transition system

noncomputable def RS.EdgeSubset.buildTransitionSystem {α : Type} {W : Fragment α} (F : EdgeSubset W) (hE : F.Eulerian) (hint : ∀ f ∈ F.flags, ∃ (v : W.Vertex), W.attach f = Sum.inl v) : F.TransitionSystem

Given an Eulerian edge subset whose flags all attach to internal vertices, construct a transition system by building per-vertex matchings and gluing them.

Equations

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

Part 2: the walk–pairing conjugation and orientation

theorem RS.EdgeSubset.TransitionSystem.walk_pairing_eq {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) {f : W.Flag} (_hf : f ∈ F.flags) : κ.walk (W.pairing f) = κ.match_ f

The walk applied to σ f gives κ f, since walk(σ f) = κ(σ(σ f)) = κ f.

theorem RS.EdgeSubset.TransitionSystem.walk_pairing_walk_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) {f : W.Flag} (hf : f ∈ F.flags) : κ.walk (W.pairing (κ.walk (W.pairing f))) = f

Fundamental computation: walk(σ(walk(σ f))) = f for participating f.

noncomputable def RS.EdgeSubset.pairingPerm {α : Type} {W : Fragment α} (F : EdgeSubset W) : Equiv.Perm ↥F.flags

The edge pairing as a permutation of participating flags.

Equations

• F.pairingPerm = Equiv.ofBijective (fun (f : ↥F.flags) => ⟨W.pairing ↑f, ⋯⟩) ⋯

@[simp]

theorem RS.EdgeSubset.pairingPerm_val {α : Type} {W : Fragment α} {F : EdgeSubset W} (x : ↥F.flags) : ↑(F.pairingPerm x) = W.pairing ↑x

The edge pairing as a permutation of participating flags.

theorem RS.EdgeSubset.pairingPerm_mul_self {α : Type} {W : Fragment α} {F : EdgeSubset W} : F.pairingPerm * F.pairingPerm = 1

σ² = 1 on participating flags.

theorem RS.EdgeSubset.pairingPerm_inv {α : Type} {W : Fragment α} {F : EdgeSubset W} : F.pairingPerm⁻¹ = F.pairingPerm

It is its own inverse.

@[simp]

theorem RS.EdgeSubset.TransitionSystem.walkPerm_val {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (x : ↥F.flags) : ↑(κ.walkPerm x) = κ.walk ↑x

The walk permutation acts by the walk step.

theorem RS.EdgeSubset.TransitionSystem.conj_eq_inv {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : F.pairingPerm * κ.walkPerm * F.pairingPerm = κ.walkPerm⁻¹

σ ∘ walk ∘ σ = walk⁻¹: the edge pairing conjugates the walk permutation to its inverse.

theorem RS.EdgeSubset.TransitionSystem.conj_zpow {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (n : ℤ) : F.pairingPerm * κ.walkPerm ^ n * F.pairingPerm = κ.walkPerm ^ (-n)

σ ∘ walk^n ∘ σ = walk^{−n} for all n : ℤ.

theorem RS.EdgeSubset.TransitionSystem.pairing_not_sameCycle {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) {f : W.Flag} (hf : f ∈ F.flags) : ¬κ.walkPerm.SameCycle ⟨f, hf⟩ ⟨W.pairing f, ⋯⟩

If f and σ f were in the same walk-orbit, the conjugation identity forces a contradiction.

theorem RS.EdgeSubset.TransitionSystem.match_sameCycle_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) {f : W.Flag} (hf : f ∈ F.flags) : κ.walkPerm.SameCycle ⟨κ.match_ f, ⋯⟩ ⟨W.pairing f, ⋯⟩

κ f is in the walk-orbit of σ f: walk(σ f) = κ f gives a direct witness.

theorem RS.EdgeSubset.TransitionSystem.pairing_match_sameCycle {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) {f : W.Flag} (hf : f ∈ F.flags) : κ.walkPerm.SameCycle ⟨W.pairing (κ.match_ f), ⋯⟩ ⟨f, hf⟩

σ(κ f) is in the walk-orbit of f: walk(σ(κ f)) = κ(σ(σ(κ f))) = κ(κ f) = f gives a direct witness.

Orientation construction

theorem RS.transition_decide_lt_flip {γ : Type} [LinearOrder γ] [DecidableRel fun (x1 x2 : γ) => x1 < x2] {a b : γ} (h : a ≠ b) : decide (a < b) = !decide (b < a)

In a linear order, a ≠ b implies decide(a < b) = !decide(b < a).

noncomputable def RS.EdgeSubset.TransitionSystem.buildOrientation {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : κ.Orientation

Construct an orientation for a transition system. Walk-orbits come in σ-paired pairs; the orientation assigns "out" to one side of each pair based on orbit representatives under the flag order.

Equations

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

The main theorem

theorem RS.EdgeSubset.exists_transition_orientation {α : Type} {W : Fragment α} (F : EdgeSubset W) (hE : F.Eulerian) (hint : ∀ f ∈ F.flags, ∃ (v : W.Vertex), W.attach f = Sum.inl v) : Nonempty ((κ : F.TransitionSystem) × κ.Orientation)

An Eulerian edge subset with internally-attached flags admits a transition system equipped with an orientation.