Set-indexed state relabels

The odd-partner relabel over a finite set of labels: the ambient algebra of the accumulated state relabels of the canonical route. Composition is symmetric difference, so pairing-returning accumulations cancel by parity.

noncomputable def RS.stateOddFlipSet {k ℓ : ℕ} {α : Type} (st : GenBoundaryState k ℓ α) (E : Finset α) : GenBoundaryState k ℓ α

The odd-partner relabel at every label of a finite set.

Equations

• RS.stateOddFlipSet st E i = if i ∈ E then Sum.map id (RS.oddPartner ℓ) (st i) else st i

theorem RS.stateOddFlipSet_of_mem {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {E : Finset α} {i : α} (h : i ∈ E) : stateOddFlipSet st E i = Sum.map id (oddPartner ℓ) (st i)

On the relabel set the state entry is ∂-flipped.

theorem RS.stateOddFlipSet_of_notMem {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {E : Finset α} {i : α} (h : i ∉ E) : stateOddFlipSet st E i = st i

Off it the state is unchanged.

theorem RS.stateOddFlipSet_empty {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} : stateOddFlipSet st ∅ = st

The empty relabel is the identity.

theorem RS.stateOddFlip_eq_flipSet {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {i₁ i₂ : α} : stateOddFlip st i₁ i₂ = stateOddFlipSet st {i₁, i₂}

The pair relabel is the two-element set relabel.

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

Composition is symmetric difference: two set relabels compose to the relabel at the symmetric difference — labels hit twice cancel by the odd-partner involution.

theorem RS.stateOddFlipSet_isInr {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {E : Finset α} (i : α) : (∃ (c : Fin (2 * ℓ)), stateOddFlipSet st E i = Sum.inr c) ↔ ∃ (c : Fin (2 * ℓ)), st i = Sum.inr c

The relabel does not change which labels carry odd colours.

theorem RS.genBoundarySubsetMatches_stateOddFlipSet {k ℓ : ℕ} {α : Type} {W : Fragment α} {s : Finset W.Flag} {st : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W s st) (E : Finset α) : genBoundarySubsetMatches W s (stateOddFlipSet st E)

The boundary-membership constraint survives any set relabel.