The chain enumerations

The intermediate flag enumerations of the parity chain: the edge-interleaved list, the oriented list, the matched list, and the global pair concatenation.

noncomputable def RS.partEdges (W : ClosedFragment) (F : EdgeSubset W) : List (Fin (edgeCount W))

The participating edges in edge order.

Equations

• RS.partEdges W F = (RS.edgeIndexSet W F).sort fun (x1 x2 : Fin (RS.edgeCount W)) => x1 ≤ x2

theorem RS.repMem_of_partEdge {W : ClosedFragment} {F : EdgeSubset W} {i : Fin (edgeCount W)} (hi : i ∈ edgeIndexSet W F) : (starFlagEnum W).symm (Fin.castAdd (edgeCount W) i) ∈ F.flags

Representative membership from edge participation.

theorem RS.partnerMem_of_partEdge {W : ClosedFragment} {F : EdgeSubset W} {i : Fin (edgeCount W)} (hi : i ∈ edgeIndexSet W F) : (starFlagEnum W).symm (Fin.natAdd (edgeCount W) i) ∈ F.flags

Partner membership from edge participation.

noncomputable def RS.edgePairList (W : ClosedFragment) (F : EdgeSubset W) : List ↥F.flags

The edge-interleaved enumeration: each participating edge contributes its representative then its partner.

Equations

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

noncomputable def RS.orientedPairList (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : List ↥F.flags

The oriented enumeration: each participating edge contributes its incoming then its outgoing flag.

Equations

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

noncomputable def RS.matchedPairList (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : List ↥F.flags

The matched enumeration: each participating edge contributes its incoming flag then that flag's match.

Equations

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

noncomputable def RS.globalPairList (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : List ↥F.flags

The global pair enumeration: the vertex pair enumerations in block order.

Equations

• RS.globalPairList W F o = List.flatMap (fun (v : Fin (RS.degList (RS.starAssignEnum W)).length) => RS.pairFlagList o (RS.blockVertex W v)) (List.finRange (RS.ds W).length)

theorem RS.blockVertex_injective' (W : ClosedFragment) : Function.Injective (blockVertex W)

blockVertex W is injective.

theorem RS.blockVertex_surjective' (W : ClosedFragment) : Function.Surjective (blockVertex W)

blockVertex W is surjective.