Boundary-relative transition systems

For an open fragment W : Fragment α and an Eulerian edge subset that may contain boundary-attached flags, the standard TransitionSystem is too strong: it requires every participating flag to be internally attached (attach_internal). This file defines a weaker notion.

Design

A RelTransitionSystem W F for an edge subset F : EdgeSubset W matches the internal participating flags pairwise at common vertices, leaving boundary-attached flags unmatched (they are path endpoints).

The walk permutation κ ∘ σ is well-defined only on internal flags. Internal circuits are the orbits of this internal walk permutation.

Paths connect boundary flags in pairs: starting from a boundary flag b, follow the edge pairing σ to the partner σ b (internal), then apply matching κ, then σ again, alternating until reaching another boundary flag. The resulting pairing is pathMatch.

Representation choice for the gluing theorem

The path matching is an involution on boundary s-flags. For the eventual gluing decomposition:

circuitCount(glued) = internalCircuitCount(F) + internalCircuitCount(G) + cycleCount(pathMatch_G ∘ pathMatch_F)

the composition of two path matchings produces closed cycles that become "cross-boundary" circuits. Representing pathMatch as an involution on boundary flags makes this composition natural.

For a closed fragment (no boundary flags), RelTransitionSystem degenerates to TransitionSystem and internalCircuitCount equals circuitCount.

Internal vs boundary flag classification

noncomputable def RS.EdgeSubset.internalFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) : Finset W.Flag

The internal flags of an edge subset: participating flags attached to a vertex.

Equations

• F.internalFlags = {f ∈ F.flags | ∃ (v : W.Vertex), W.attach f = Sum.inl v}

theorem RS.EdgeSubset.mem_internalFlags_iff {α : Type} {W : Fragment α} {f : W.Flag} {F : EdgeSubset W} : f ∈ F.internalFlags ↔ f ∈ F.flags ∧ ∃ (v : W.Vertex), W.attach f = Sum.inl v

A flag is internal exactly when it is in the subset and attached to a vertex.

noncomputable def RS.EdgeSubset.boundaryFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) : Finset W.Flag

The boundary flags of an edge subset: participating flags attached to a boundary label.

Equations

• F.boundaryFlags = {f ∈ F.flags | ∃ (i : α), W.attach f = Sum.inr i}

theorem RS.EdgeSubset.mem_internalFlags_or_boundaryFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} (hf : f ∈ F.flags) : f ∈ F.internalFlags ∨ f ∈ F.boundaryFlags

Every participating flag is either internal or boundary.

theorem RS.EdgeSubset.internalFlags_disjoint_boundaryFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) : Disjoint F.internalFlags F.boundaryFlags

Internal and boundary flags are disjoint.

theorem RS.EdgeSubset.mem_flags_of_internalFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} (hf : f ∈ F.internalFlags) : f ∈ F.flags

An internal flag is in the edge subset.

theorem RS.EdgeSubset.mem_flags_of_boundaryFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} (hf : f ∈ F.boundaryFlags) : f ∈ F.flags

A boundary flag is in the edge subset.

theorem RS.EdgeSubset.attach_internal_of_mem {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} (hf : f ∈ F.internalFlags) : ∃ (v : W.Vertex), W.attach f = Sum.inl v

An internal flag is attached to some vertex.

theorem RS.EdgeSubset.attach_boundary_of_mem {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} (hf : f ∈ F.boundaryFlags) : ∃ (i : α), W.attach f = Sum.inr i

A boundary flag is attached to some label.

theorem RS.EdgeSubset.boundaryFlag_mem_boundaryFlags {α : Type} {W : Fragment α} {F : EdgeSubset W} {a : α} (hf : W.boundaryFlag a ∈ F.flags) : W.boundaryFlag a ∈ F.boundaryFlags

A participating boundary flag lies in the boundary flags: it attaches to a label, so it cannot be internal.

def RS.EdgeSubset.allInternal {α : Type} {W : Fragment α} (F : EdgeSubset W) : Prop

All participating flags are internal (no boundary flags).

Equations

• F.allInternal = (F.boundaryFlags = ∅)

theorem RS.EdgeSubset.mem_internalFlags_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {f : W.Flag} (hf : f ∈ F.flags) : f ∈ F.internalFlags

When all flags are internal, a participating flag is internal.

Boundary-relative transition system

structure RS.EdgeSubset.RelTransitionSystem {α : Type} {W : Fragment α} (F : EdgeSubset W) : Type

A boundary-relative transition system on an edge subset: a fixed-point-free involution of its internal flags matching flags at a common vertex. Boundary flags are path endpoints and are not matched. This mirrors TransitionSystem but restricts the domain from all participating flags to internal flags only.

• match_ : W.Flag → W.Flag

  The matching, defined on all flags but only meaningful on internal participating flags.

• match_invol (f : W.Flag) : f ∈ F.internalFlags → self.match_ (self.match_ f) = f

  The matching is an involution on the internal flags.

• match_ne (f : W.Flag) : f ∈ F.internalFlags → self.match_ f ≠ f

  The matching has no fixed points on internal flags.

• match_mem (f : W.Flag) : f ∈ F.internalFlags → self.match_ f ∈ F.internalFlags

  The matching maps internal flags to internal flags.

• match_vertex (f : W.Flag) : f ∈ F.internalFlags → ∀ (v : W.Vertex), W.attach f = Sum.inl v → W.attach (self.match_ f) = Sum.inl v

  Matched flags share an internal vertex.

Compatibility: conversions

theorem RS.EdgeSubset.mem_internalFlags_of {α : Type} {W : Fragment α} {F : EdgeSubset W} {f : W.Flag} (hf : f ∈ F.flags) (hv : ∃ (v : W.Vertex), W.attach f = Sum.inl v) : f ∈ F.internalFlags

A participating flag that is internally attached is an internal flag.

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

Every TransitionSystem is a RelTransitionSystem.

Equations

• κ.toRelTransitionSystem = { match_ := κ.match_, match_invol := ⋯, match_ne := ⋯, match_mem := ⋯, match_vertex := ⋯ }

Walk and circuit count on internal flags

noncomputable def RS.EdgeSubset.RelTransitionSystem.internalWalk {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) : W.Flag

The walk map on flags via a relative transition: follow pairing then matching.

Equations

• κ.internalWalk f = κ.match_ (W.pairing f)

theorem RS.EdgeSubset.RelTransitionSystem.internalWalk_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hp : W.pairing f ∈ F.internalFlags) : κ.internalWalk f ∈ F.internalFlags

If a flag's pairing is internal, its walk successor is internal.

theorem RS.EdgeSubset.RelTransitionSystem.internalWalk_injOn {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f g : W.Flag} (hpf : W.pairing f ∈ F.internalFlags) (hpg : W.pairing g ∈ F.internalFlags) (h : κ.internalWalk f = κ.internalWalk g) : f = g

The walk map is injective on flags whose pairings are internal.

theorem RS.EdgeSubset.RelTransitionSystem.pairing_internal_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (_κ : F.RelTransitionSystem) (hall : F.allInternal) {f : W.Flag} (hf : f ∈ F.internalFlags) : W.pairing f ∈ F.internalFlags

When all flags are internal, the pairing of an internal flag is internal.

theorem RS.EdgeSubset.RelTransitionSystem.internalWalk_mem_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (hall : F.allInternal) {f : W.Flag} (hf : f ∈ F.internalFlags) : κ.internalWalk f ∈ F.internalFlags

When all flags are internal, the walk preserves internal flags.

theorem RS.EdgeSubset.RelTransitionSystem.internalWalk_injOn_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (hall : F.allInternal) {f g : W.Flag} (hf : f ∈ F.internalFlags) (hg : g ∈ F.internalFlags) (h : κ.internalWalk f = κ.internalWalk g) : f = g

When all flags are internal, the walk is injective.

noncomputable def RS.EdgeSubset.RelTransitionSystem.walkPermInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (hall : F.allInternal) : Equiv.Perm ↥F.internalFlags

The walk permutation on internal flags, when all flags are internal.

Equations

• κ.walkPermInternal hall = Equiv.ofBijective (fun (f : ↥F.internalFlags) => ⟨κ.internalWalk ↑f, ⋯⟩) ⋯

noncomputable def RS.EdgeSubset.RelTransitionSystem.internalCircuitCount {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (hall : F.allInternal) : ℕ

The internal circuit count when all flags are internal.

Equations

• κ.internalCircuitCount hall = ((κ.walkPermInternal hall).cycleType.card + Fintype.card ↑(Function.fixedPoints ⇑(κ.walkPermInternal hall))) / 2

Compatibility: circuit-count agreement for closed subsets

theorem RS.EdgeSubset.internalFlags_eq_flags_of_transition {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : F.internalFlags = F.flags

When a TransitionSystem exists (all flags internal), the internal flags equal the full flag set.

theorem RS.EdgeSubset.allInternal_of_transition {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : F.allInternal

A standard TransitionSystem implies all flags are internal.

noncomputable def RS.EdgeSubset.flagsEquivInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : ↥F.flags ≃ ↥F.internalFlags

The equivalence between full-flag and internal-flag subtypes when all flags are internal.

Equations

• RS.EdgeSubset.flagsEquivInternal κ = { toFun := fun (f : ↥F.flags) => ⟨↑f, ⋯⟩, invFun := fun (f : ↥F.internalFlags) => ⟨↑f, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem RS.EdgeSubset.walkPerm_eq_of_transition {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : κ.toRelTransitionSystem.walkPermInternal ⋯ = (flagsEquivInternal κ).permCongr κ.walkPerm

The walk permutations agree under the canonical equivalence.

theorem RS.EdgeSubset.relTransition_circuitCount_eq {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) : κ.toRelTransitionSystem.internalCircuitCount ⋯ = κ.circuitCount

Compatibility: for a closed-fragment transition system, internalCircuitCount equals circuitCount.

Orientation for relative transition systems

structure RS.EdgeSubset.RelTransitionSystem.Orientation {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : Type

An orientation compatible with a boundary-relative transition system: an in/out designation of the internal flags, flipped by the matching and by the edge pairing (when both ends are internal).

• isOut : W.Flag → Bool

  Whether a flag is outgoing.

• match_flip (f : W.Flag) : f ∈ F.internalFlags → self.isOut (κ.match_ f) = !self.isOut f

  The matching flips orientation on internal flags.

• pairing_flip (f : W.Flag) : f ∈ F.internalFlags → W.pairing f ∈ F.internalFlags → self.isOut (W.pairing f) = !self.isOut f

  The pairing flips orientation on internal flags whose partner is also internal.

Path chain tracing

noncomputable def RS.EdgeSubset.traceChain {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : ℕ → W.Flag → Option W.Flag

Follow the chain from a flag: apply pairing, check if boundary; if internal, apply matching and recurse. Returns none if the fuel runs out.

Equations

• One or more equations did not get rendered due to their size.
• RS.EdgeSubset.traceChain κ 0 x✝ = none