The pair enumeration

The Definition 5 odd list at a vertex is, order-exactly, the per-flag value map over an explicit flag list: the incoming flags in the fixed order, each followed by its match.

noncomputable def RS.defFiveValue {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) (f : ↥F.flags) : Fin (2 * ℓ)

The Definition 5 per-flag odd value: outgoing flags carry the partner of their colour, incoming flags the colour itself.

Equations

• RS.defFiveValue o φ f = if o.isOut ↑f = true then RS.oddPartner ℓ (↑φ f) else ↑φ f

theorem RS.isOut_of_mem_inFlagsAt {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.TransitionSystem} (o : κ.Orientation) {v : W.Vertex} {f : W.Flag} (hf : f ∈ F.inFlagsAt o v) : o.isOut f = false

Incoming flags are incoming.

noncomputable def RS.pairFlagList {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.TransitionSystem} (o : κ.Orientation) (v : W.Vertex) : List ↥F.flags

The flag list underlying the odd list at a vertex: the incoming flags in the fixed order, each followed by its match.

Equations

• RS.pairFlagList o v = List.flatMap (fun (f : ↥F.flags) => [f, ⟨κ.match_ ↑f, ⋯⟩]) ((F.inFlagsAt o v).attachWith (fun (x : W.Flag) => x ∈ F.flags) ⋯)

theorem RS.oddListAt_eq_map {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) (v : W.Vertex) : F.oddListAt o φ v = List.map (defFiveValue o φ) (pairFlagList o v)

The odd list is the value map of the pair enumeration, order-exactly.