The non-separated per-step status identification

The non-separated counterpart of antiLow_labels_eq_statusChange: for the transported frame of a non-separated step — reached from a canonical source o by first flipping the anchor chain (the c-chain, realized as a PortedFlipSet) and then transporting across the repair — the fold of the anchor pair with a full disjoint anti-low list is exactly the status-change set (nonsep_labels_eq_statusChange).

The identification dissolves into a per-chord XOR computation. For a participating end x the chain flip toggles the direction exactly when x is an end of the anchor chord (pairing_mem_flipSet_iff, via chain disjointness), so with T := x on the anchor chord, old := high-in-κ, new := high-in-κ':

• x or its new partner is anti-canonical for the transported frame iff new ⊕ (old ⊕ T) — the new-chord rigidity pairs the two ends' directions (anti_ends_iff_toggle_xor_status);
• the anchor membership contributes T once more, and T ⊕ (new ⊕ old ⊕ T) = new ⊕ old is the status change — the (2,3)-chord phenomenon (an anchor end whose status did not change must be anti: the extra toggle needs undoing) is the case T = true, new = old of the same algebra.

No swap-end data is consumed: the identity holds for the anchored transported frame of any repair from a canonical source.

Propositional XOR helpers

The toggle set of the anchored chain flip

theorem RS.EdgeSubset.pairing_mem_flipSet_iff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} : PortedFlipSet κ S p₁ p₂ i₁ i₂ → ∀ {β₂ : W.Flag} (hβ₂ : β₂ ∈ F.boundaryFlags) (hint₂ : W.pairing β₂ ∈ F.internalFlags) (honS : ∀ f ∈ S, OnBoundaryChain κ β₂ f) (hSon : ∀ f ∈ F.internalFlags, OnBoundaryChain κ β₂ f → f ∈ S) {x : W.Flag} (hx : x ∈ F.boundaryFlags) (hxint : W.pairing x ∈ F.internalFlags), W.pairing x ∈ S ↔ x = β₂ ∨ x = κ.pathMatch β₂ hβ₂

The chain flip toggles exactly the anchor chord's ends: a ported flip set realized by the boundary chain of β₂ contains the entry edge of a participating boundary flag x iff x is an end of β₂'s chord. The two anchor ends' entry edges lie on the chain by construction; any other participating end's entry edge is on a genuinely distinct chain (onBoundaryChain_disjoint).

The per-end evaluation of the anchored transported frame

theorem RS.EdgeSubset.nonsep_labels_eq_statusChange {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {iβ iγ : α} (hsq : RepairSquare κ a b c d v) {o : κ.Orientation} (hc : PathCanonical o) (hpf : PortedFlipSet κ S p₁ p₂ iβ iγ) (hflip : (o.portFlip hpf).isOut c = !(o.portFlip hpf).isOut a) {β₂ : W.Flag} (hβ₂ : β₂ ∈ F.boundaryFlags) (hint₂ : W.pairing β₂ ∈ F.internalFlags) (honS : ∀ f ∈ S, OnBoundaryChain κ β₂ f) (hSon : ∀ f ∈ F.internalFlags, OnBoundaryChain κ β₂ f → f ∈ S) (hlabβ : F.boundaryLabel hβ₂ = iβ) (hlabγ : F.boundaryLabel ⋯ = iγ) {L : List (α × α)} (hall : ∀ p ∈ L, AntiLowPair (RelTransitionSystem.Orientation.transportRepair hsq (o.portFlip hpf) hflip) p) (hdisj : List.Pairwise PairDisjoint L) (hlen : L.length = (antiLowSet (RelTransitionSystem.Orientation.transportRepair hsq (o.portFlip hpf) hflip)).card) {i : α} : i ∈ pairFold ((iβ, iγ) :: L) ↔ (i ∈ highSet (κ.repair a b c d v hsq)) ≠ (i ∈ highSet κ)

The non-separated per-step status identification: for the anchored transported frame of a non-separated step from a canonical source — flip the anchor chain of β₂ (the c-chain, realized as the ported flip set S with the chord's two end labels iβ, iγ), then transport across the repair — the fold of the anchor pair (iβ, iγ) with a full pairwise-disjoint anti-low list of the transported frame is exactly the set of labels whose high-status differs between the repaired and the source systems. The anchor pair is β₂'s chord in the source system; the list pairs are anti-low chords of the repaired system at the transported frame.