The non-separated count parities

The two orbit-counting inputs of RS.Novel.Skein.NonSeparatedStep, proved:

• nonSeparatedSegmentParity — a same-component square preserves the circuit-count parity (NonSeparatedSegmentParity);
• nonSeparatedMergeParity — a square whose c-edge lies on a circuit not carrying a flips the count parity (NonSeparatedMergeParity).

Method

Both are computed on the closed-up full walk Π of RS.Novel.Skein.SeparatedParity: a localized square turns the repaired full walk into (a d)(b c) · Π (fullPerm_repair), and permOrbitCount Π = permOrbitCount walkPermPeriodic + |B| converts full-walk orbit ledgers into circuit-count ledgers.

Merge case (c periodic, a off its orbit): exactly separatedCountParity — the two swaps act coherently (permOrbitCount_swap_swap_mul, Δ = ±2 on Π-orbits, Δ = ±1 on circuits, parity flips). The separated-orientation exclusion a ≁ c is replaced by the orbit-disjointness hypothesis via sameCycle_periodic_val.

Segment case (WalkReach κ c a): the walk gives c ∼ a, the mirror symmetry gives b ∼ σa ∼ σc ∼ d, and the mirror collision at c gives b ≁ c. The first swap therefore merges the two traversal orbits of the component and the second swap splits the merged cycle again (a ∼ d after the merge): the net change of the Π-orbit count is zero (permOrbitCount_swap_swap_mul_cancel below), so the circuit count is unchanged and the parity is even.

The localization needed for fullPerm_repair comes from squareLocalized_of_walkReach (segment case) and from periodic_or_onBoundaryChain (merge case); their [LinearOrder α] assumption is discharged by well-ordering the label type.

The incoherent double swap: merge then split

The same-component parity (segment reversal, Δ = 0)

theorem RS.nonSeparatedSegmentParity : NonSeparatedSegmentParity

The segment count parity (the input NonSeparatedSegmentParity): a same-component square preserves the circuit-count parity. The first swap merges the two traversal orbits of the component, the second splits them again: Δ permOrbitCount = 0.

The distinct-component parity (splice merge, Δ = ±1)

theorem RS.nonSeparatedMergeParity : NonSeparatedMergeParity

The merge count parity (the input NonSeparatedMergeParity): a square whose c-edge lies on a circuit not carrying a flips the count parity. The argument of separatedCountParity, with the separated-orientation exclusion a ≁ c replaced by the orbit-disjointness hypothesis.