Existence of path-canonical orientations

Every orientation of a boundary-relative transition system can be repaired into a path-canonical one by flipping exactly the internal flags lying on non-canonically oriented boundary-to-boundary chains.

Main results

• EdgeSubset.exists_pathCanonical — from any orientation of a relative transition system, a path-canonical orientation of the same system exists.
• EdgeSubset.canonOrientation — the orientation it produces, built by flipping every chain whose low end points outwards.

Proof route

1. BadFlag marks the pairing-side flags of chains whose low-labelled boundary end has an outgoing entry edge (ChainNonCanon); the symmetric formulation covers every internal flag of such a chain, since match-side flags are the pairing-side flags of the reverse chain (iterWalk_reverse).
2. The flip set is closed under the matching (badFlag_match) and under the edge pairing on internal partners (badFlag_pairing), so negating isOut on it yields a valid orientation (canonOrientation).
3. Exit steps of a forward walk are unique (exit_step_unique), and a pairing-side flag's forward walk exits at its chain's base end (chain_flag_exit); hence the chain data witnessing badness of an entry flag are pinned to the entry's own chain, and the flip decision at each entry flag matches its chain's canonicality status (pathCanonical_canonOrientation).

1. Exit uniqueness and chain membership

theorem RS.EdgeSubset.exit_step_unique {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} {k₁ k₂ : ℕ} (hc₁ : ∀ t < k₁, W.pairing (iterWalk κ f t) ∈ F.internalFlags) (ht₁ : W.pairing (iterWalk κ f k₁) ∈ F.boundaryFlags) (hc₂ : ∀ t < k₂, W.pairing (iterWalk κ f t) ∈ F.internalFlags) (ht₂ : W.pairing (iterWalk κ f k₂) ∈ F.boundaryFlags) : k₁ = k₂

Exit uniqueness: two boundary-exit data for the forward walk of one flag agree on the exit step.

theorem RS.EdgeSubset.chain_flag_exit {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} {k m : ℕ} (hcont : ∀ t < k, W.pairing (iterWalk κ b t) ∈ F.internalFlags) (hmk : m < k) : (∀ t < m, W.pairing (iterWalk κ (W.pairing (iterWalk κ b m)) t) ∈ F.internalFlags) ∧ W.pairing (iterWalk κ (W.pairing (iterWalk κ b m)) m) = b

Chain-flag exit data: the forward walk of the pairing-side flag at step m of a chain from b has internal pairings before step m and exits at b at step m.

theorem RS.EdgeSubset.pathMatch_eq_of_chain {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) {k : ℕ} (hcont : ∀ t < k, W.pairing (iterWalk κ b t) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ b k) ∈ F.boundaryFlags) : κ.pathMatch b hb = W.pairing (iterWalk κ b k)

The path match of a boundary end equals the terminal pairing of any boundary-terminated chain data from it (via exit uniqueness — no fuel bound required on the given data).

theorem RS.EdgeSubset.pathMatch_eq_pairing_of_boundary {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) (hp : W.pairing b ∈ F.boundaryFlags) : κ.pathMatch b hb = W.pairing b

A flag whose partner is a boundary flag is matched to it.

2. Non-canonical chains and the flip set

def RS.EdgeSubset.ChainNonCanon {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (o : κ.Orientation) (b : W.Flag) : Prop

The chain from boundary end b is non-canonically oriented: its lower-labelled end — whichever of b and its path match that is — has an outgoing entry edge.

Equations

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

theorem RS.EdgeSubset.chainNonCanon_pathMatch {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {b : W.Flag} (h : ChainNonCanon κ o b) (hb : b ∈ F.boundaryFlags) : ChainNonCanon κ o (κ.pathMatch b hb)

Non-canonicality passes to the opposite chain end.

def RS.EdgeSubset.BadFlag {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (o : κ.Orientation) (f : W.Flag) : Prop

The flip set: f is a pairing-side flag of a non-canonically oriented boundary-to-boundary chain.

Equations

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

theorem RS.EdgeSubset.badFlag_match {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {f : W.Flag} (h : BadFlag κ o f) : BadFlag κ o (κ.match_ f)

Match closure: the flip set is closed under the matching — the match of a pairing-side flag is a pairing-side flag of the reverse chain, whose base end is the path match of the original.

theorem RS.EdgeSubset.badFlag_pairing {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {f : W.Flag} (h : BadFlag κ o f) (hp : W.pairing f ∈ F.internalFlags) : BadFlag κ o (W.pairing f)

Pairing closure: the flip set is closed under the edge pairing whenever the partner is internal — the partner is a match-side flag, i.e. a pairing-side flag of the reverse chain.

3. The flipped orientation

noncomputable def RS.EdgeSubset.canonIsOut {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (o : κ.Orientation) (f : W.Flag) : Bool

The candidate canonical orientation as a raw flag function: negate on the flip set.

Equations

• RS.EdgeSubset.canonIsOut κ o f = if RS.EdgeSubset.BadFlag κ o f then !o.isOut f else o.isOut f

theorem RS.EdgeSubset.canonIsOut_of_bad {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {f : W.Flag} (h : BadFlag κ o f) : canonIsOut κ o f = !o.isOut f

On a flag of a badly oriented chain the repair reverses.

theorem RS.EdgeSubset.canonIsOut_of_not_bad {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {f : W.Flag} (h : ¬BadFlag κ o f) : canonIsOut κ o f = o.isOut f

Elsewhere it leaves the orientation alone.

noncomputable def RS.EdgeSubset.canonOrientation {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (o : κ.Orientation) : κ.Orientation

The flipped orientation: negate the given orientation on the flip set. The closure lemmas make the flip commute with both orientation axioms.

Equations

• RS.EdgeSubset.canonOrientation κ o = { isOut := RS.EdgeSubset.canonIsOut κ o, match_flip := ⋯, pairing_flip := ⋯ }

theorem RS.EdgeSubset.canonOrientation_isOut {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (o : κ.Orientation) (f : W.Flag) : (canonOrientation κ o).isOut f = canonIsOut κ o f

The repaired orientation's table is that repair.

4. Canonicality of the flipped orientation

theorem RS.EdgeSubset.pathCanonical_canonOrientation {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (o : κ.Orientation) : PathCanonical (canonOrientation κ o)

The flipped orientation is path-canonical: at each low-end entry flag, exit uniqueness pins any badness witness to the entry's own chain, so the flip decision matches the chain's prior status.

Existence and its canonical-frame form

theorem RS.EdgeSubset.exists_pathCanonical {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (o : κ.Orientation) : ∃ (o' : κ.Orientation), PathCanonical o'

Existence of path-canonical orientations: any orientation of a boundary-relative transition system can be repaired into a path-canonical orientation of the same system.