Per-step status identification of the relabel sets

Two composable identifications for the paired assembly. First, the pairs of a full pairwise-disjoint AntiLowPair list enumerate the anti-canonical set: membership in the pairFold of such a list is exactly being an end label of some anti-canonical chain (mem_pairFold_antiLow) — the completeness direction pins every anti flag's label as a first component by comparing cardinalities (Finset.eq_of_subset_of_card_le). Second, for the transported frame of a separated step from a canonical source, the anti set's end labels are exactly the labels whose high-status changed across the repair (antiLow_labels_eq_statusChange): an anti end is low-in-new but high-in-old, and its new partner is high-in-new but low-in-old (the re-paired ends carry opposite old statuses, swap_dirs_opposite); conversely a status-changed label must sit on a re-paired end (mem_highSet_repair_untouched).

Propositional inequality helpers

The enumeration lemma

theorem RS.EdgeSubset.antiLowSet_subset_boundary {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) : antiLowSet o ⊆ F.boundaryFlags

The anti-canonical set consists of boundary flags.

theorem RS.EdgeSubset.mem_pairFold_antiLow {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {L : List (α × α)} (hall : ∀ p ∈ L, AntiLowPair o p) (hdisj : List.Pairwise PairDisjoint L) (hlen : L.length = (antiLowSet o).card) {a : α} : a ∈ pairFold L ↔ ∃ (β : W.Flag) (hβ : β ∈ F.boundaryFlags), β ∈ antiLowSet o ∧ (a = F.boundaryLabel hβ ∨ a = F.boundaryLabel ⋯)

Pairs of a full disjoint anti-low list enumerate the anti set: for a list of anti-low pairs, pairwise disjoint and as long as the anti set, membership in the fold is exactly being an end label of some anti-canonical chain. The completeness direction is a counting argument: the first components form a Nodup list of labels of anti flags, and label injectivity forces them to exhaust the anti set.

The separated-step status identification

theorem RS.EdgeSubset.antiLow_labels_eq_statusChange {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) {o : κ.Orientation} (hflip : o.isOut c = !o.isOut a) (hc : PathCanonical o) {e₁ e₂ : W.Flag} (he₁ : e₁ ∈ F.boundaryFlags) (he₂ : e₂ ∈ F.boundaryFlags) (hcross : (κ.repair a b c d v hsq).pathMatch e₁ he₁ = e₂) (hfar : (κ.repair a b c d v hsq).pathMatch (κ.pathMatch e₁ he₁) ⋯ = κ.pathMatch e₂ he₂) (hout : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), δ ≠ e₁ → δ ≠ e₂ → δ ≠ κ.pathMatch e₁ he₁ → δ ≠ κ.pathMatch e₂ he₂ → (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ) (hint₁ : W.pairing e₁ ∈ F.internalFlags) (hint₂ : W.pairing e₂ ∈ F.internalFlags) (hintP₁ : W.pairing (κ.pathMatch e₁ he₁) ∈ F.internalFlags) (hintP₂ : W.pairing (κ.pathMatch e₂ he₂) ∈ F.internalFlags) {i : α} : (∃ (β : W.Flag) (hβ : β ∈ F.boundaryFlags), β ∈ antiLowSet (RelTransitionSystem.Orientation.transportRepair hsq o hflip) ∧ (i = F.boundaryLabel hβ ∨ i = F.boundaryLabel ⋯)) ↔ (i ∈ highSet (κ.repair a b c d v hsq)) ≠ (i ∈ highSet κ)

The separated-step status identification: for the transported frame of a separated step from a canonical source, the end labels of the anti-canonical chords — each anti low end with its partner in the repaired system, the shape produced by mem_pairFold_antiLow at the transported frame — are exactly the labels whose high-status differs between the repaired and the source systems.

theorem RS.prop_ne_iff {P Q : Prop} : P ≠ Q ↔ P ∧ ¬Q ∨ Q ∧ ¬P

Propositional inequality as an exclusive disjunction, in the symmU component order.