Open circuit count for boundary-relative transition systems

For an edge subset F that may have boundary flags, the internal circuit count (internalCircuitCount) is defined only when F.allInternal holds. This file generalises the count to open edge subsets by restricting to the periodic flags — internal flags whose forward walk eventually returns to them.

Main definitions

• PeriodicFlag — a flag on a closed circuit: internal, with the walk staying internal and returning to it.
• periodicFlags — the finset of periodic flags.
• walkPermPeriodic — the walk restricted to periodic flags as a permutation.
• openCircuitCount — (cycleType.card + fixedPoints) / 2 on periodic flags.

Main results

• openCircuitCount_of_allInternal — when all flags are internal the open and internal circuit counts agree.
• internal_periodic_or_terminates — every internal flag is either periodic or its chain reaches the boundary.
• not_periodic_of_boundary_chain — boundary-terminating flags are not periodic.

1. PeriodicFlag

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

A flag on a closed circuit: it is internal, every intermediate pairing stays internal, and the walk returns to it.

Equations

• κ.PeriodicFlag f = (f ∈ F.internalFlags ∧ ∃ (n : ℕ), 1 ≤ n ∧ (∀ j < n, W.pairing (RS.EdgeSubset.iterWalk κ f j) ∈ F.internalFlags) ∧ RS.EdgeSubset.iterWalk κ f n = f)

theorem RS.EdgeSubset.RelTransitionSystem.PeriodicFlag.mem_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {f : W.Flag} (hf : κ.PeriodicFlag f) : f ∈ F.internalFlags

A periodic flag is internal.

Periodicity helpers

theorem RS.EdgeSubset.iterWalk_add_period {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) (n k : ℕ) (hperiod : iterWalk κ f n = f) : iterWalk κ f (n + k) = iterWalk κ f k

Shift a period: iterWalk κ f (n + k) = iterWalk κ f k when iterWalk κ f n = f.

theorem RS.EdgeSubset.all_pairings_internal_of_periodic {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hper : κ.PeriodicFlag f) (j : ℕ) : W.pairing (iterWalk κ f j) ∈ F.internalFlags

All pairings along a periodic walk are internal.

theorem RS.EdgeSubset.iterWalk_mem_internal_of_periodic {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hper : κ.PeriodicFlag f) (j : ℕ) (hj : 1 ≤ j) : iterWalk κ f j ∈ F.internalFlags

All iterates along a periodic walk are internal.

theorem RS.EdgeSubset.RelTransitionSystem.periodicFlag_step {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {f : W.Flag} (hf : κ.PeriodicFlag f) : κ.PeriodicFlag (iterWalk κ f 1)

The walk-successor of a periodic flag is periodic (same period).

2. periodicFlags

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

The finset of periodic flags.

Equations

• κ.periodicFlags = {f ∈ F.internalFlags | ∃ (n : ℕ), 1 ≤ n ∧ (∀ j < n, W.pairing (RS.EdgeSubset.iterWalk κ f j) ∈ F.internalFlags) ∧ RS.EdgeSubset.iterWalk κ f n = f}

theorem RS.EdgeSubset.RelTransitionSystem.mem_periodicFlags {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} : f ∈ κ.periodicFlags ↔ κ.PeriodicFlag f

Membership in periodicFlags iff PeriodicFlag.

theorem RS.EdgeSubset.RelTransitionSystem.periodicFlags_sub {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : f ∈ κ.periodicFlags) : f ∈ F.internalFlags

A periodic flag is internal.

Walk closure on periodic flags

theorem RS.EdgeSubset.RelTransitionSystem.internalWalk_periodic {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : f ∈ κ.periodicFlags) : κ.internalWalk f ∈ κ.periodicFlags

The walk maps periodic flags to periodic flags.

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

The walk is injective on periodic flags.

3. walkPermPeriodic

noncomputable def RS.EdgeSubset.RelTransitionSystem.walkPermPeriodic {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : Equiv.Perm ↥κ.periodicFlags

The walk permutation restricted to periodic flags.

Equations

• κ.walkPermPeriodic = Equiv.ofBijective (fun (f : ↥κ.periodicFlags) => ⟨κ.internalWalk ↑f, ⋯⟩) ⋯

4. openCircuitCount

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

The open circuit count: half the orbit count of the walk on periodic flags.

Equations

• κ.openCircuitCount = (κ.walkPermPeriodic.cycleType.card + Fintype.card ↑(Function.fixedPoints ⇑κ.walkPermPeriodic)) / 2

Backward period extraction

theorem RS.EdgeSubset.iterWalk_period_of_repeat {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) (i d : ℕ) (hcont : ∀ j < i + d, W.pairing (iterWalk κ f j) ∈ F.internalFlags) (heq : iterWalk κ f i = iterWalk κ f (i + d)) : iterWalk κ f d = f

If the walk repeats at positions i and i + d (with all intermediate pairings internal), then it has period d from position 0.

Pigeonhole period extraction

5. Compatibility with internalCircuitCount

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

Under allInternal, every internal flag is periodic (via pigeonhole on the walk iterates).

noncomputable def RS.EdgeSubset.periodicEquivInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (hall : F.allInternal) : ↥κ.periodicFlags ≃ ↥F.internalFlags

The equivalence between periodic-flag and internal-flag subtypes under allInternal.

Equations

• RS.EdgeSubset.periodicEquivInternal κ hall = { toFun := fun (g : ↥κ.periodicFlags) => ⟨↑g, ⋯⟩, invFun := fun (g : ↥F.internalFlags) => ⟨↑g, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem RS.EdgeSubset.walkPermPeriodic_eq_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (hall : F.allInternal) : κ.walkPermPeriodic = (periodicEquivInternal κ hall).symm.permCongr (κ.walkPermInternal hall)

The two walk permutations agree under the canonical equivalence.

theorem RS.EdgeSubset.openCircuitCount_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (hall : F.allInternal) : κ.openCircuitCount = κ.internalCircuitCount hall

Compatibility: for a closed edge subset, openCircuitCount equals internalCircuitCount.

6. Boundary paths are not periodic

theorem RS.EdgeSubset.traceChain_none_of_all_internal_pairings {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (h : ∀ (j : ℕ), W.pairing (iterWalk κ f j) ∈ F.internalFlags) (fuel : ℕ) : traceChain κ fuel f = none

The chain from a flag with all-internal pairings always returns none (never reaches the boundary).

theorem RS.EdgeSubset.not_periodic_of_boundary_chain {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) (hterm : ∃ (fuel : ℕ) (b : W.Flag), traceChain κ fuel f = some b) : ¬κ.PeriodicFlag f

A flag whose chain reaches the boundary is not periodic.

Dichotomy: periodic or boundary-terminating

theorem RS.EdgeSubset.internal_periodic_or_terminates {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) (hf : f ∈ F.internalFlags) : κ.PeriodicFlag f ∨ ∃ (fuel : ℕ) (b : W.Flag), traceChain κ fuel f = some b

Every internal flag is either periodic or its chain reaches the boundary.

The edge-pairing reversal on periodic flags

Reversing every periodic flag along its own edge conjugates the walk permutation into its inverse, which is what makes the open circuits come in pairs.

theorem RS.EdgeSubset.pairing_mem_periodicFlags {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : f ∈ κ.periodicFlags) : W.pairing f ∈ κ.periodicFlags

The periodic flags are closed under the edge pairing: a closed circuit's edges lie wholly on it.

noncomputable def RS.EdgeSubset.revPerm {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : Equiv.Perm ↥κ.periodicFlags

The edge-pairing reversal on periodic flags.

Equations

• RS.EdgeSubset.revPerm κ = Function.Involutive.toPerm (fun (x : ↥κ.periodicFlags) => ⟨W.pairing ↑x, ⋯⟩) ⋯

theorem RS.EdgeSubset.walkPerm_revPerm_walkPerm {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : κ.walkPermPeriodic * revPerm κ * κ.walkPermPeriodic = revPerm κ

The reversal conjugates the walk to its inverse: traversing a circuit backwards.

theorem RS.EdgeSubset.revPerm_mul_self {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : revPerm κ * revPerm κ = 1

The reversal is an involution.

theorem RS.EdgeSubset.revPerm_inv {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : (revPerm κ)⁻¹ = revPerm κ

Equivalently, it is its own inverse.