Representative flags

Each edge's representative flag is the one enumerated on the low slot half. The set of participating flags whose edge representative is outgoing (under an orientation) is closed under the pairing — it is the flip set aligning the data colouring with the Definition 5 odd lists.

noncomputable def RS.repFlag (W : ClosedFragment) (g : W.Flag) : W.Flag

The representative flag of a flag's edge: the one on the low slot half.

Equations

• RS.repFlag W g = if ↑((RS.starFlagEnum W) g) < RS.edgeCount W then g else W.pairing g

theorem RS.repFlag_low (W : ClosedFragment) (g : W.Flag) (h : ↑((starFlagEnum W) g) < edgeCount W) : repFlag W g = g

A flag on the low half represents its own edge.

theorem RS.repFlag_high (W : ClosedFragment) (g : W.Flag) (h : ¬↑((starFlagEnum W) g) < edgeCount W) : repFlag W g = W.pairing g

A flag on the high half is represented by its partner.

theorem RS.repFlag_pairing (W : ClosedFragment) (g : W.Flag) : repFlag W (W.pairing g) = repFlag W g

The representative flag is pairing-invariant.

noncomputable def RS.outRepSet (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : Finset W.Flag

The flip set of an orientation: participating flags whose edge representative is outgoing.

Equations

• RS.outRepSet W F o = {g ∈ F.flags | o.isOut (RS.repFlag W g) = true}

theorem RS.outRepSet_pairing_mem (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (g : W.Flag) : g ∈ outRepSet W F o → W.pairing g ∈ outRepSet W F o

The flip set is closed under the pairing.

theorem RS.mem_outRepSet_iff (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (g : W.Flag) (hg : g ∈ F.flags) : g ∈ outRepSet W F o ↔ o.isOut (repFlag W g) = true

Membership in the flip set depends only on the edge.