The separated count parity

Discharges SeparatedCountParity: a separated repair square on a localized configuration flips the circuit-count parity (Δ openCircuitCount = ±1).

Architecture

Instead of tracking the periodic-flag subtype (which changes across the move in the chain-local cases), we close up the whole system into a single permutation on all participating flags, the full walk Π = M ∘ σ, where σ is the edge pairing and M is the matching on internal flags extended by the path matching on boundary flags. Its orbits are the circuit orbits (two per circuit) plus one orbit per boundary flag (each boundary chain contributes its two traversal directions, each containing exactly one boundary flag). Hence

orbits Π = orbits (walkPermPeriodic) + boundaryFlags.card.

Because a localized square leaves the path matching untouched (pathMatch_repair_of_localized), the repaired full walk is the old one multiplied by the double transposition (a d)(b c). An abstract transposition lemma (multiplying by a swap changes the orbit count by exactly one, splitting iff the swapped points share an orbit) plus the mirror symmetry σ Π σ = Π⁻¹ and the separated orientation force the two swaps to act coherently: the orbit count moves by exactly ±2, i.e. the circuit count by ±1.

Main results

• permOrbitCount_swap_mul_sameCycle / ..._not_sameCycle — the abstract transposition ledger for total orbit counts.
• permOrbitCount_swap_swap_mul — the coherent double swap.
• EdgeSubset.fullPerm — the closed-up walk permutation.
• EdgeSubset.permOrbitCount_fullPerm_eq — the orbit bookkeeping orbits Π = orbits wpp + |B|.
• EdgeSubset.fullPerm_repair — the move is the double swap.
• separatedCountParity — the discharged SeparatedCountParity.

(i) Abstract orbit counting

noncomputable def RS.permOrbitCount {Y : Type} [Fintype Y] [DecidableEq Y] (g : Equiv.Perm Y) : ℕ

The total orbit count of a permutation: nontrivial cycles plus fixed points.

Equations

• RS.permOrbitCount g = g.cycleType.card + Fintype.card ↑(Function.fixedPoints ⇑g)

theorem RS.card_fixedPoints_add_card_support {Y : Type} [Fintype Y] [DecidableEq Y] (g : Equiv.Perm Y) : Fintype.card ↑(Function.fixedPoints ⇑g) + g.support.card = Fintype.card Y

Fixed points and support partition the domain.

theorem RS.perm_pow_mod {Y : Type} {g : Equiv.Perm Y} {x : Y} {p : ℕ} (_hp : 1 ≤ p) (hper : (g ^ p) x = x) (i : ℕ) : (g ^ i) x = (g ^ (i % p)) x

Reduce a permutation power at a recurrent point.

theorem RS.sameCycle_of_pow_eq {Y : Type} {g : Equiv.Perm Y} {x y : Y} {n : ℕ} (h : (g ^ n) x = y) : g.SameCycle x y

A SameCycle witness from a power.

theorem RS.sameCycle_swap_mul_iff {Y : Type} [Finite Y] [DecidableEq Y] {g : Equiv.Perm Y} {x y u : Y} (hux : ¬g.SameCycle u x) (huy : ¬g.SameCycle u y) (v : Y) : (Equiv.swap x y * g).SameCycle u v ↔ g.SameCycle u v

Untouched orbits: SameCycle from a point in neither swapped orbit transfers across the swap-multiplication.

theorem RS.sameCycle_swap_mul_of_not {Y : Type} [Finite Y] [DecidableEq Y] {g : Equiv.Perm Y} {x y : Y} (_hxy : x ≠ y) (hsc : ¬g.SameCycle x y) : (Equiv.swap x y * g).SameCycle x y

Merging: swapping two points of different orbits joins them.

Orbit counting via representatives

theorem RS.permOrbitCount_eq_card_of_reps {Y : Type} [Fintype Y] [DecidableEq Y] (g : Equiv.Perm Y) (S : Finset Y) (hcover : ∀ (z : Y), ∃ w ∈ S, g.SameCycle w z) (hsep : ∀ w ∈ S, ∀ w' ∈ S, g.SameCycle w w' → w = w') : permOrbitCount g = S.card

Orbit counting by representatives: a set meeting every orbit exactly once has the orbit count as its cardinality.

The cycle split

The transposition orbit ledger

theorem RS.permOrbitCount_swap_mul_sameCycle {Y : Type} [Fintype Y] [DecidableEq Y] {g : Equiv.Perm Y} {x y : Y} (hxy : x ≠ y) (hsc : g.SameCycle x y) : permOrbitCount (Equiv.swap x y * g) = permOrbitCount g + 1

Splitting: multiplying by a transposition of two points on one orbit raises the orbit count by one.

theorem RS.permOrbitCount_swap_mul_not_sameCycle {Y : Type} [Fintype Y] [DecidableEq Y] {g : Equiv.Perm Y} {x y : Y} (hxy : x ≠ y) (hsc : ¬g.SameCycle x y) : permOrbitCount g = permOrbitCount (Equiv.swap x y * g) + 1

Merging: multiplying by a transposition of two points on different orbits lowers the orbit count by one.

theorem RS.permOrbitCount_swap_swap_mul {Y : Type} [Fintype Y] [DecidableEq Y] {g : Equiv.Perm Y} {a b c d : Y} (hbc : b ≠ c) (had : a ≠ d) (hiff : g.SameCycle b c ↔ g.SameCycle a d) (hab : ¬g.SameCycle a b) (hac : ¬g.SameCycle a c) : permOrbitCount (Equiv.swap a d * (Equiv.swap b c * g)) = permOrbitCount g + 2 ∨ permOrbitCount g = permOrbitCount (Equiv.swap a d * (Equiv.swap b c * g)) + 2

The coherent double swap: with the mirror equivalence b ∼ c ↔ a ∼ d and the two exclusions a ≁ b, a ≁ c, the double transposition moves the orbit count by exactly two.

theorem RS.permOrbitCount_permCongr {γ δ : Type} [Fintype γ] [DecidableEq γ] [Fintype δ] [DecidableEq δ] (e : γ ≃ δ) (g : Equiv.Perm γ) : permOrbitCount (e.permCongr g) = permOrbitCount g

Transporting a permutation along an equivalence preserves the orbit count.

theorem RS.permOrbitCount_sumCongr {γ δ : Type} [Fintype γ] [DecidableEq γ] [Fintype δ] [DecidableEq δ] (σ : Equiv.Perm γ) (τ : Equiv.Perm δ) : permOrbitCount (Equiv.sumCongr σ τ) = permOrbitCount σ + permOrbitCount τ

The orbit count of a sumCongr is the sum of the orbit counts.

(ii) The closed-up full walk permutation

noncomputable def RS.EdgeSubset.pairingPermSP {α : Type} {W : Fragment α} (F : EdgeSubset W) : Equiv.Perm ↥F.flags

The edge pairing as a permutation of the participating flags.

Equations

• F.pairingPermSP = { toFun := fun (x : ↥F.flags) => ⟨W.pairing ↑x, ⋯⟩, invFun := fun (x : ↥F.flags) => ⟨W.pairing ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RS.EdgeSubset.pairingPermSP_val {α : Type} {W : Fragment α} {F : EdgeSubset W} (x : ↥F.flags) : ↑(F.pairingPermSP x) = W.pairing ↑x

The edge pairing as a permutation of participating flags, on underlying flags.

theorem RS.EdgeSubset.pairingPermSP_invol {α : Type} {W : Fragment α} {F : EdgeSubset W} (x : ↥F.flags) : F.pairingPermSP (F.pairingPermSP x) = x

It is an involution.

theorem RS.EdgeSubset.pairingPermSP_mul_self {α : Type} {W : Fragment α} {F : EdgeSubset W} : F.pairingPermSP * F.pairingPermSP = 1

Equivalently, its square is the identity.

noncomputable def RS.EdgeSubset.fullMatchFun {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (x : ↥F.flags) : ↥F.flags

The matching extended by the path matching, as a function on participating flags.

Equations

• RS.EdgeSubset.fullMatchFun κ x = if h : ↑x ∈ F.internalFlags then ⟨κ.match_ ↑x, ⋯⟩ else ⟨κ.pathMatch ↑x ⋯, ⋯⟩

theorem RS.EdgeSubset.fullMatchFun_val_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {x : ↥F.flags} (h : ↑x ∈ F.internalFlags) : ↑(fullMatchFun κ x) = κ.match_ ↑x

The full matching is the system's own on internal flags.

theorem RS.EdgeSubset.fullMatchFun_val_boundary {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {x : ↥F.flags} (h : ↑x ∈ F.boundaryFlags) : ↑(fullMatchFun κ x) = κ.pathMatch (↑x) h

And the path matching on boundary flags: this is what closes the chains into orbits.

theorem RS.EdgeSubset.fullMatchFun_invol {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (x : ↥F.flags) : fullMatchFun κ (fullMatchFun κ x) = x

The full matching is an involution, both halves being ones.

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

The extended matching as an (involutive) permutation.

Equations

• RS.EdgeSubset.fullMatchPerm κ = { toFun := RS.EdgeSubset.fullMatchFun κ, invFun := RS.EdgeSubset.fullMatchFun κ, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RS.EdgeSubset.fullMatchPerm_apply {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (x : ↥F.flags) : (fullMatchPerm κ) x = fullMatchFun κ x

The full matching as a permutation acts by that function.

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

Its square is the identity.

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

The full walk permutation: pairing followed by extended matching, a permutation of all participating flags.

Equations

• RS.EdgeSubset.fullPerm κ = RS.EdgeSubset.fullMatchPerm κ * F.pairingPermSP

theorem RS.EdgeSubset.fullPerm_apply {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (x : ↥F.flags) : (fullPerm κ) x = fullMatchFun κ (F.pairingPermSP x)

The full walk: cross the edge, then match — including at the boundary, where matching follows the chain to its far end.

theorem RS.EdgeSubset.fullPerm_val_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {x : ↥F.flags} (h : W.pairing ↑x ∈ F.internalFlags) : ↑((fullPerm κ) x) = κ.match_ (W.pairing ↑x)

Its value when the edge partner is internal.

theorem RS.EdgeSubset.fullPerm_val_boundary {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {x : ↥F.flags} (h : W.pairing ↑x ∈ F.boundaryFlags) : ↑((fullPerm κ) x) = κ.pathMatch (W.pairing ↑x) h

Its value when the edge partner is a boundary flag.

theorem RS.EdgeSubset.fullPerm_apply_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (x : ↥F.flags) : (fullPerm κ) (F.pairingPermSP x) = fullMatchFun κ x

Applying the full walk to a paired flag lands on the extended matching.

theorem RS.EdgeSubset.fullPerm_inv {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : (fullPerm κ)⁻¹ = F.pairingPermSP * fullMatchPerm κ

The inverse of the full walk.

theorem RS.EdgeSubset.sameCycle_pairingPermSP {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {x y : ↥F.flags} (h : (fullPerm κ).SameCycle x y) : (fullPerm κ).SameCycle (F.pairingPermSP x) (F.pairingPermSP y)

Mirror symmetry: the pairing conjugates the full walk to its inverse, so SameCycle transfers to paired flags.

Trajectories of the full walk

theorem RS.EdgeSubset.fullPerm_pow_val {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {x : ↥F.flags} {m : ℕ} (hcont : ∀ t < m, W.pairing (iterWalk κ (↑x) t) ∈ F.internalFlags) (j : ℕ) : j ≤ m → ↑((fullPerm κ ^ j) x) = iterWalk κ (↑x) j

While the pairings along a walk stay internal, powers of the full walk follow the iterated walk.

theorem RS.EdgeSubset.fullPerm_pow_val_periodic {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {x : ↥F.flags} (hper : κ.PeriodicFlag ↑x) (j : ℕ) : ↑((fullPerm κ ^ j) x) = iterWalk κ (↑x) j

Powers of the full walk at a periodic flag follow the iterated walk forever.

theorem RS.EdgeSubset.sameCycle_periodic_val {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {x y : ↥F.flags} (hper : κ.PeriodicFlag ↑x) (h : (fullPerm κ).SameCycle x y) : ∃ (i : ℕ), iterWalk κ (↑x) i = ↑y

SameCycle from a periodic flag produces a walk witness.

theorem RS.EdgeSubset.not_sameCycle_pairingPermSP_of_periodic {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {x : ↥F.flags} (hper : κ.PeriodicFlag ↑x) : ¬(fullPerm κ).SameCycle x (F.pairingPermSP x)

Mirror collision, periodic case: a periodic flag is never on the same full-walk orbit as its pairing.

Chain orbits of the full walk

theorem RS.EdgeSubset.fullPerm_chain_wrap {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β : W.Flag} (hβ : β ∈ F.boundaryFlags) {k : ℕ} (hkle : k ≤ F.flags.card) (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ β k) ∈ F.boundaryFlags) : (fullPerm κ ^ (k + 1)) ⟨β, ⋯⟩ = ⟨β, ⋯⟩

The chain wraps: the full walk from a boundary flag closes up after k + 1 steps (through the path-matching jump).

theorem RS.EdgeSubset.fullPerm_chain_sameCycle_val {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β : W.Flag} (hβ : β ∈ F.boundaryFlags) {k : ℕ} (hkle : k ≤ F.flags.card) (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ β k) ∈ F.boundaryFlags) {z : ↥F.flags} (h : (fullPerm κ).SameCycle ⟨β, ⋯⟩ z) : ∃ j ≤ k, ↑z = iterWalk κ β j

Values on the full-walk orbit of a boundary flag are chain values.

theorem RS.EdgeSubset.fullPerm_chain_boundary_eq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β : W.Flag} (hβ : β ∈ F.boundaryFlags) {k : ℕ} (hkle : k ≤ F.flags.card) (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ β k) ∈ F.boundaryFlags) {z : ↥F.flags} (h : (fullPerm κ).SameCycle ⟨β, ⋯⟩ z) (hzb : ↑z ∈ F.boundaryFlags) : z = ⟨β, ⋯⟩

A boundary flag on the full-walk orbit of a boundary flag is the base point.

theorem RS.EdgeSubset.not_sameCycle_pairingPermSP_of_chain {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β : W.Flag} (hβ : β ∈ F.boundaryFlags) {k : ℕ} (hkle : k ≤ F.flags.card) (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ β k) ∈ F.boundaryFlags) {f : W.Flag} (hfi : f ∈ F.flags) {t : ℕ} (htk : t ≤ k) (hft : f = iterWalk κ β t ∨ f = W.pairing (iterWalk κ β t)) : ¬(fullPerm κ).SameCycle ⟨f, hfi⟩ (F.pairingPermSP ⟨f, hfi⟩)

Mirror collision, chain case: a chain flag is never on the same full-walk orbit as its pairing.

theorem RS.EdgeSubset.isOut_iterWalk_chain {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β : W.Flag} {k : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (o : κ.Orientation) {i j : ℕ} (hi1 : 1 ≤ i) (hij : i ≤ j) (hjk : j ≤ k) : o.isOut (iterWalk κ β j) = o.isOut (iterWalk κ β i)

Orientation constancy along the walk side of a chain.

theorem RS.EdgeSubset.isOut_pairing_iterWalk_chain {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β : W.Flag} {k : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (o : κ.Orientation) {j : ℕ} (hjk : j < k) : o.isOut (W.pairing (iterWalk κ β j)) = !o.isOut (iterWalk κ β (j + 1))

The pairing-side orientation along a chain.

The periodic/chain decomposition of the orbit count

theorem RS.EdgeSubset.fullPerm_periodic_iff {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (x : ↥F.flags) : ↑((fullPerm κ) x) ∈ κ.periodicFlags ↔ ↑x ∈ κ.periodicFlags

The full walk preserves periodicity.

noncomputable def RS.EdgeSubset.fullPermPeriodic {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : Equiv.Perm { x : ↥F.flags // ↑x ∈ κ.periodicFlags }

The full walk restricted to periodic flags.

Equations

• RS.EdgeSubset.fullPermPeriodic κ = (RS.EdgeSubset.fullPerm κ).subtypePerm ⋯

noncomputable def RS.EdgeSubset.fullPermChain {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : Equiv.Perm { x : ↥F.flags // ↑x ∉ κ.periodicFlags }

The full walk restricted to non-periodic flags.

Equations

• RS.EdgeSubset.fullPermChain κ = (RS.EdgeSubset.fullPerm κ).subtypePerm ⋯

theorem RS.EdgeSubset.fullPerm_eq_sumCongr {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : fullPerm κ = (Equiv.sumCompl fun (x : ↥F.flags) => ↑x ∈ κ.periodicFlags).permCongr (Equiv.sumCongr (fullPermPeriodic κ) (fullPermChain κ))

The decomposition of the full walk over the periodicity partition.

theorem RS.EdgeSubset.permOrbitCount_fullPerm_split {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : permOrbitCount (fullPerm κ) = permOrbitCount (fullPermPeriodic κ) + permOrbitCount (fullPermChain κ)

The orbit count splits over the partition.

noncomputable def RS.EdgeSubset.periodicSubEquiv {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : { x : ↥F.flags // ↑x ∈ κ.periodicFlags } ≃ ↥κ.periodicFlags

The double-subtype carrier of the periodic part.

Equations

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

theorem RS.EdgeSubset.walkPermPeriodic_eq_permCongr {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : κ.walkPermPeriodic = (periodicSubEquiv κ).permCongr (fullPermPeriodic κ)

The periodic part of the full walk is the periodic walk permutation.

theorem RS.EdgeSubset.permOrbitCount_fullPermPeriodic {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : permOrbitCount (fullPermPeriodic κ) = permOrbitCount κ.walkPermPeriodic

The periodic part has the periodic orbit count.

theorem RS.EdgeSubset.fullPermChain_pow_val {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (z : { x : ↥F.flags // ↑x ∉ κ.periodicFlags }) (n : ℕ) : ↑((fullPermChain κ ^ n) z) = (fullPerm κ ^ n) ↑z

Values of powers of the chain part.

theorem RS.EdgeSubset.sameCycle_fullPermChain_val {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {z w : { x : ↥F.flags // ↑x ∉ κ.periodicFlags }} (h : (fullPermChain κ).SameCycle z w) : (fullPerm κ).SameCycle ↑z ↑w

SameCycle in the chain part descends to the full walk.

theorem RS.EdgeSubset.permOrbitCount_fullPermChain {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : permOrbitCount (fullPermChain κ) = F.boundaryFlags.card

The chain part counts the boundary flags: each non-periodic orbit contains exactly one boundary flag.

theorem RS.EdgeSubset.permOrbitCount_fullPerm_eq {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : permOrbitCount (fullPerm κ) = permOrbitCount κ.walkPermPeriodic + F.boundaryFlags.card

The orbit bookkeeping: the full walk's orbit count is the periodic orbit count plus the number of boundary flags.

The move as a double swap

theorem RS.EdgeSubset.fullPerm_repair {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) (hpm : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ) : fullPerm (κ.repair a b c d v hsq) = Equiv.swap ⟨a, ⋯⟩ ⟨d, ⋯⟩ * (Equiv.swap ⟨b, ⋯⟩ ⟨c, ⋯⟩ * fullPerm κ)

The move is a double swap: on a square whose repair leaves the path matching unchanged, the repaired full walk is the old full walk multiplied by the double transposition (a d)(b c).

Orientation exclusions

theorem RS.EdgeSubset.isOut_iterWalk_periodic {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {f : W.Flag} (hper : κ.PeriodicFlag f) (i : ℕ) : o.isOut (iterWalk κ f i) = o.isOut f

Orientation constancy along a periodic walk.

theorem RS.EdgeSubset.not_sameCycle_of_periodic_flip {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {x y : ↥F.flags} (hper : κ.PeriodicFlag ↑x) (hflip : o.isOut ↑y = !o.isOut ↑x) : ¬(fullPerm κ).SameCycle x y

The separated exclusion, periodic seed: a flag oppositely oriented to a periodic flag is not on its full-walk orbit.

theorem RS.EdgeSubset.not_sameCycle_of_chain_positions {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β : W.Flag} (hβ : β ∈ F.boundaryFlags) {k : ℕ} (hkle : k ≤ F.flags.card) (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ β k) ∈ F.boundaryFlags) (o : κ.Orientation) {x y : ↥F.flags} (hxi : ↑x ∈ F.internalFlags) (hyi : ↑y ∈ F.internalFlags) {s t : ℕ} (hsk : s ≤ k) (htk : t ≤ k) (hxs : ↑x = iterWalk κ β s ∨ ↑x = W.pairing (iterWalk κ β s)) (hyt : ↑y = iterWalk κ β t ∨ ↑y = W.pairing (iterWalk κ β t)) (hflip : o.isOut ↑y = !o.isOut ↑x) : ¬(fullPerm κ).SameCycle x y

The separated exclusion, chain seeds: two chain flags in separated orientation are not on a common full-walk orbit.

(iii) The discharged parity input

theorem RS.separatedCountParity : SeparatedCountParity

The separated count parity (the input SeparatedCountParity): a separated square on a localized configuration flips the circuit-count parity.