Orientation existence

Every boundary-relative transition system admits an orientation: the boundary-completed walk is an involution pair, and two-colouring its orbits by the orbit representative gives the directions. Canonical data therefore exist exactly when a transition system does.

Orientation existence

Every boundary-relative transition system admits an orientation: complete the matching across the boundary by the path matching (fixed-point-free by the chain-reversal parity), and two-colour the alternating-walk orbits exactly as buildOrientation does — the conjugation identity is pure group algebra of two involutions.

theorem RS.EdgeSubset.RelTransitionSystem.pathMatch_ne {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) : κ.pathMatch b hb ≠ b

The path matching has no fixed points: a chain cannot end where it starts — folding the reversal identity into the middle hits a pairing or matching fixed point.

theorem RS.internal_not_boundary {α : Type} {W : Fragment α} {F : EdgeSubset W} {f : W.Flag} (hf : f ∈ F.internalFlags) : f ∉ F.boundaryFlags

Internal and boundary flags are disjoint.

noncomputable def RS.relComplete {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) : W.Flag

The matching completed across the boundary by the path matching.

Equations

• RS.relComplete κ f = if _hf : f ∈ F.internalFlags then κ.match_ f else if hb : f ∈ F.boundaryFlags then κ.pathMatch f hb else f

theorem RS.relComplete_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : f ∈ F.internalFlags) : relComplete κ f = κ.match_ f

The completed matching is the system's own on internal flags.

theorem RS.relComplete_boundary {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hb : f ∈ F.boundaryFlags) : relComplete κ f = κ.pathMatch f hb

And the path matching on boundary flags.

theorem RS.relComplete_off {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : f ∉ F.flags) : relComplete κ f = f

Off the subset it is the identity.

theorem RS.relComplete_invol {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : Function.Involutive (relComplete κ)

The completed matching is a global involution.

theorem RS.relComplete_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : f ∈ F.flags) : relComplete κ f ∈ F.flags

The completed matching preserves the participating flags.

theorem RS.relComplete_ne {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : f ∈ F.flags) : relComplete κ f ≠ f

The completed matching has no fixed points on participating flags.

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

The completed matching as a permutation of the participating flags.

Equations

• RS.relMatchPerm κ = { toFun := fun (x : ↥F.flags) => ⟨RS.relComplete κ ↑x, ⋯⟩, invFun := fun (x : ↥F.flags) => ⟨RS.relComplete κ ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RS.relMatchPerm_val {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (x : ↥F.flags) : ↑((relMatchPerm κ) x) = relComplete κ ↑x

The completed matching as a permutation, on underlying flags.

theorem RS.relMatchPerm_mul_self {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : relMatchPerm κ * relMatchPerm κ = 1

It is an involution.

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

The completed walk permutation.

Equations

• RS.relWalkPerm κ = RS.relMatchPerm κ * F.pairingPerm

@[simp]

theorem RS.relWalkPerm_val {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (x : ↥F.flags) : ↑((relWalkPerm κ) x) = relComplete κ (W.pairing ↑x)

The walk permutation: cross the edge, then match.

theorem RS.relWalkPerm_inv {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : (relWalkPerm κ)⁻¹ = F.pairingPerm * relMatchPerm κ

Its inverse walks the other way: match, then cross.

theorem RS.relConj {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : F.pairingPerm * relWalkPerm κ * F.pairingPerm = (relWalkPerm κ)⁻¹

The pairing conjugates the completed walk to its inverse.

theorem RS.relConj_zpow {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (n : ℤ) : F.pairingPerm * relWalkPerm κ ^ n * F.pairingPerm = relWalkPerm κ ^ (-n)

The mirror symmetry: conjugating a power of the walk by the edge pairing inverts it — traversing a chain backwards.

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

A flag and its pairing partner are never in the same completed walk orbit.

theorem RS.relMatch_sameCycle_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : f ∈ F.internalFlags) : (relWalkPerm κ).SameCycle ⟨κ.match_ f, ⋯⟩ ⟨W.pairing f, ⋯⟩

An internal flag's match and its edge partner lie on the same walk orbit.

theorem RS.relPairing_match_sameCycle {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : f ∈ F.internalFlags) : (relWalkPerm κ).SameCycle ⟨W.pairing (κ.match_ f), ⋯⟩ ⟨f, ⋯⟩

So do the edge partner of a flag's match and the flag itself.

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

Orientation existence: every boundary-relative transition system admits an orientation — two-colour the completed-walk orbits by the orbit-representative comparison.

Equations

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

theorem RS.nonempty_canonical_any {β : Type} [LinearOrder β] {V : Fragment β} {F : EdgeSubset V} (κ : F.RelTransitionSystem) : Nonempty { o : κ.Orientation // EdgeSubset.PathCanonical o }

Unconditional canonicity: every system on every subset has a path-canonical orientation.

The bottom splitting

With orientation existence, canonical data reduce to bare system existence, and the pinned term of a disjoint-union subset factorizes side by side at the restricted systems, the value product being threaded through the support certificates.

theorem RS.nonempty_canonData_iff_system {β : Type} [LinearOrder β] {V : Fragment β} (F : EdgeSubset V) : Nonempty F.CanonData ↔ Nonempty F.RelTransitionSystem

Canonical data are exactly system existence.

The product family

The tower base as the product of the side-pinned families: the side restrictions return the side families up to MatchEq, so the bottom of the tower is side-pinned by construction — the side-pinning covariance dissolves.

theorem RS.join_support_left {α β : Type} [LinearOrder α] {W₁ : Fragment α} {W₂ : Fragment β} [instS : LinearOrder (α ⊕ β)] {s : Finset (W₁.disjUnion W₂).Flag} (hc : ∀ f ∈ s, (W₁.disjUnion W₂).pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) : ∃ (hcL : ∀ f ∈ leftPart s, W₁.pairing f ∈ leftPart s), { flags := leftPart s, pairing_mem := hcL }.Eulerian ∧ Nonempty { flags := leftPart s, pairing_mem := hcL }.CanonData

The left support transfer of a join subset.

theorem RS.join_support_right {α β : Type} [LinearOrder β] {W₁ : Fragment α} {W₂ : Fragment β} [instS : LinearOrder (α ⊕ β)] {s : Finset (W₁.disjUnion W₂).Flag} (hc : ∀ f ∈ s, (W₁.disjUnion W₂).pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) : ∃ (hcR : ∀ f ∈ rightPart s, W₂.pairing f ∈ rightPart s), { flags := rightPart s, pairing_mem := hcR }.Eulerian ∧ Nonempty { flags := rightPart s, pairing_mem := hcR }.CanonData

The right support transfer of a join subset.

theorem RS.nonempty_canonData_glueOpen {α : Type} [LinearOrder α] {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') (hne : Nonempty { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.CanonData) : Nonempty { flags := s', pairing_mem := hc' }.CanonData

Canonical data ascend the open glue. A lift's system glues, and every system is orientable, so the glued subset carries canonical data as soon as the lift does.