Relabel sets for the canonical ledgers

A canonical ledger reports the state it lands in as stateOddFlipSet st E. This module is the arithmetic of the set E: it is a symmetric-difference fold (pairFold) of label pairs, one pair per flipped chain, each pair the two end labels of a chord of the stage system. Within one recanonicalization the flipped chains are distinct anti-canonical chains (AntiLowPair), so the pairs are pairwise disjoint (PairDisjoint) and the fold is a disjoint union (mem_pairFold_of_pairwise).

The accumulated relabel of a whole route is the status difference statusDiff, which telescopes along chains (statusDiff_trans) and vanishes on a pairing-preserving one (statusDiff_of_samePairing).

noncomputable def RS.symmU {α : Type} (E₁ E₂ : Finset α) : Finset α

Symmetric difference of two finite sets — the composition law of stateOddFlipSet (stateOddFlipSet_symmU).

Equations

• RS.symmU E₁ E₂ = E₁ \ E₂ ∪ E₂ \ E₁

theorem RS.mem_symmU {α : Type} {E₁ E₂ : Finset α} {i : α} : i ∈ symmU E₁ E₂ ↔ i ∈ E₁ ∧ i ∉ E₂ ∨ i ∈ E₂ ∧ i ∉ E₁

Membership in a symmetric difference: in exactly one of the two sets.

theorem RS.symmU_self {α : Type} (A : Finset α) : symmU A A = ∅

The symmetric difference of a set with itself is empty.

theorem RS.symmU_trans {α : Type} (A B C : Finset α) : symmU (symmU A B) (symmU B C) = symmU A C

Telescoping: symmetric differences against a common middle compose.

theorem RS.symmU_empty_left {α : Type} (E : Finset α) : symmU ∅ E = E

The empty set is a left unit.

theorem RS.symmU_assoc {α : Type} (E₁ E₂ E₃ : Finset α) : symmU (symmU E₁ E₂) E₃ = symmU E₁ (symmU E₂ E₃)

Symmetric difference is associative, so a fold over a list is well-behaved.

noncomputable def RS.pairSet {α : Type} (p : α × α) : Finset α

The two-element label set of a label pair.

Equations

• RS.pairSet p = {p.1, p.2}

theorem RS.mem_pairSet {α : Type} {p : α × α} {i : α} : i ∈ pairSet p ↔ i = p.1 ∨ i = p.2

Membership in a pair's label set.

noncomputable def RS.pairFold {α : Type} (L : List (α × α)) : Finset α

The symmetric-difference fold of a list of label pairs.

Equations

• RS.pairFold L = List.foldr (fun (p : α × α) (E : Finset α) => RS.symmU (RS.pairSet p) E) ∅ L

theorem RS.pairFold_nil {α : Type} : pairFold [] = ∅

The fold over no pairs is empty: nothing relabelled.

theorem RS.pairFold_cons {α : Type} (p : α × α) (L : List (α × α)) : pairFold (p :: L) = symmU (pairSet p) (pairFold L)

One more pair contributes its two labels, cancelling any that the rest of the fold already carries.

theorem RS.pairFold_append {α : Type} (L₁ L₂ : List (α × α)) : pairFold (L₁ ++ L₂) = symmU (pairFold L₁) (pairFold L₂)

The fold turns concatenation into symmetric difference — the composition law the accumulated relabel needs.

theorem RS.mem_pairFold_of_pairwise {α : Type} {L : List (α × α)} (hL : List.Pairwise PairDisjoint L) {i : α} : i ∈ pairFold L ↔ ∃ p ∈ L, i = p.1 ∨ i = p.2

The fold of pairwise disjoint pairs is their union: under PairDisjoint no cancellation occurs, so membership in the fold is membership in some pair.

Set relabels: boundary matching and composition

theorem RS.stateOddFlipSet_symmU {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} (E₁ E₂ : Finset α) : stateOddFlipSet (stateOddFlipSet st E₁) E₂ = stateOddFlipSet st (symmU E₁ E₂)

Composition of set relabels is the symmU of the sets.

Anti-canonical chain pairs

def RS.EdgeSubset.AntiLowPair {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) (p : α × α) : Prop

A chord pair whose low end is anti-canonical for o: the label pair of a chain flipped by the recanonicalization of o.

Equations

• RS.EdgeSubset.AntiLowPair o p = ∃ (β : W.Flag) (hβ : β ∈ F.boundaryFlags), β ∈ RS.EdgeSubset.antiLowSet o ∧ p.1 = F.boundaryLabel hβ ∧ p.2 = F.boundaryLabel ⋯

theorem RS.EdgeSubset.AntiLowPair.lt {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {p : α × α} (h : AntiLowPair o p) : p.1 < p.2

An anti-low pair is ordered: low label first.

theorem RS.EdgeSubset.AntiLowPair.mono {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o' : κ.Orientation} (hsub : antiLowSet o' ⊆ antiLowSet o) {p : α × α} (h : AntiLowPair o' p) : AntiLowPair o p

Anti-canonical pairs survive enlarging the anti-canonical set.

theorem RS.EdgeSubset.antiLowPair_disjoint {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {β γ : W.Flag} (hβ : β ∈ F.boundaryFlags) (hγ : γ ∈ F.boundaryFlags) (hβm : β ∈ antiLowSet o) (hγm : γ ∈ antiLowSet o) (hne : β ≠ γ) : PairDisjoint (F.boundaryLabel hβ, F.boundaryLabel ⋯) (F.boundaryLabel hγ, F.boundaryLabel ⋯)

Distinct anti-canonical chains have disjoint label pairs: the low ends are distinct low ends, so no end of one chord can be an end of the other.

noncomputable def RS.EdgeSubset.statusDiff {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] (κ κ' : F.RelTransitionSystem) : Finset α

The status difference of two systems: the labels whose high-status differs — the potential of the canonical route's accumulated relabel.

Equations

• RS.EdgeSubset.statusDiff κ κ' = RS.symmU (RS.EdgeSubset.highSet κ) (RS.EdgeSubset.highSet κ')

theorem RS.EdgeSubset.statusDiff_self {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] (κ : F.RelTransitionSystem) : statusDiff κ κ = ∅

A system differs from itself nowhere: the relabel accumulated along a trivial route is empty.

theorem RS.EdgeSubset.statusDiff_trans {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] (κ₁ κ₂ κ₃ : F.RelTransitionSystem) : symmU (statusDiff κ₁ κ₂) (statusDiff κ₂ κ₃) = statusDiff κ₁ κ₃

The status difference telescopes along chains.

theorem RS.EdgeSubset.statusDiff_of_samePairing {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] {κ κ' : F.RelTransitionSystem} (h : SamePairing κ κ') : statusDiff κ κ' = ∅

Same-pairing endpoints have empty status difference.

theorem RS.prop_ne_cases {P Q : Prop} (h : P ≠ Q) : P ∧ ¬Q ∨ ¬P ∧ Q

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

theorem RS.prop_ne_of_left {P Q : Prop} (hP : P) (hQ : ¬Q) : P ≠ Q

One holds and the other does not, so they differ.

theorem RS.prop_ne_of_right {P Q : Prop} (hP : ¬P) (hQ : Q) : P ≠ Q

The mirrored case.