The boundary-relative constrained summand

The Definition 5 summand re-founded on boundary-relative transition systems: vertex-local odd lists and signs over a relative orientation (in-flags at a vertex are automatically internal), and the state-constrained summand with an abstract circuit exponent — specialized to the open circuit count when that lands. For subsets arising from a standard transition system, the relative data agrees with the original.

Vertex-local data over a relative orientation

noncomputable def RS.EdgeSubset.relInFlagsAt {α : Type} {W : Fragment α} (F : EdgeSubset W) {κ : F.RelTransitionSystem} (o : κ.Orientation) (v : W.Vertex) : List W.Flag

In-flags at a vertex for a boundary-relative orientation: the participating flags attached to the vertex and marked incoming, in the fixed enumeration order.

Equations

• F.relInFlagsAt o v = {f ∈ F.flags | W.attach f = Sum.inl v ∧ o.isOut f = false}.sort fun (x1 x2 : W.Flag) => x1 ≤ x2

theorem RS.EdgeSubset.mem_internal_of_mem_relInFlagsAt {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {v : W.Vertex} {f : W.Flag} (hf : f ∈ F.relInFlagsAt o v) : f ∈ F.internalFlags

An in-flag at a vertex is an internal flag.

Agreement with the standard data

def RS.EdgeSubset.TransitionSystem.Orientation.toRel {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.TransitionSystem} (o : κ.Orientation) : κ.toRelTransitionSystem.Orientation

Transport of an orientation to the relative system.

Equations

• o.toRel = { isOut := o.isOut, match_flip := ⋯, pairing_flip := ⋯ }

theorem RS.mem_relInFlagsAt_iff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {vv : W.Vertex} {f : W.Flag} : f ∈ F.relInFlagsAt o vv ↔ f ∈ F.flags ∧ W.attach f = Sum.inl vv ∧ o.isOut f = false

Membership in the in-flag list, unfolded.

theorem RS.relInFlagsAt_nodup {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) (vv : W.Vertex) : (F.relInFlagsAt o vv).Nodup

The in-flag list is Nodup.