Monotone relabel invariance of the corrected constrained value

Transporting a fragment along an order isomorphism of its label types leaves the corrected state-constrained partition value unchanged, up to composing the boundary state with the isomorphism. Fragment.relabel keeps the flags, vertices, pairing, and circles on the nose and only re-decorates the boundary attachments, so every ingredient of the through value is transported by identity-shaped conversions; the orientation guard i < j of the through product is preserved because the relabeling is monotone.

Both sides of the value are defined by a Classical.choice of relative transition data, so the transport is stated for a value already pinned to a choice: the relabel carries one side's data to the other's, and the conversions are identity-shaped.

Attachment decoding under a relabel

theorem RS.relabel_pairing_eq {α β : Type} {W : Fragment α} (ee : α ≃ β) : (W.relabel ee).pairing = W.pairing

The relabel keeps the pairing.

theorem RS.relabel_attach_inl_iff {α β : Type} {W : Fragment α} (ee : α ≃ β) (f : W.Flag) (v : W.Vertex) : (W.relabel ee).attach f = Sum.inl v ↔ W.attach f = Sum.inl v

Internal attachment is untouched by a relabel.

theorem RS.relabel_attach_inr_iff {α β : Type} {W : Fragment α} (ee : α ≃ β) (f : W.Flag) (i : α) : (W.relabel ee).attach f = Sum.inr (ee i) ↔ W.attach f = Sum.inr i

Boundary attachment is shifted through the equivalence.

theorem RS.relabel_attach_inl_exists {α β : Type} {W : Fragment α} (ee : α ≃ β) (f : W.Flag) : (∃ (v : W.Vertex), (W.relabel ee).attach f = Sum.inl v) ↔ ∃ (v : W.Vertex), W.attach f = Sum.inl v

Being internally attached is invariant under a relabel.

theorem RS.relabel_attach_inr_exists {α β : Type} {W : Fragment α} (ee : α ≃ β) (f : W.Flag) : (∃ (b : β), (W.relabel ee).attach f = Sum.inr b) ↔ ∃ (i : α), W.attach f = Sum.inr i

Being boundary-attached is invariant under a relabel.

theorem RS.relabel_boundaryFlag_apply {α β : Type} {W : Fragment α} (ee : α ≃ β) (a : α) : (W.relabel ee).boundaryFlag (ee a) = W.boundaryFlag a

The relabelled boundary flag at a pushed-forward label.

Edge subsets under a relabel

def RS.EdgeSubset.relabelUp {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) : EdgeSubset (W.relabel ee)

Transport of an edge subset along a relabel: the flags and the pairing are untouched.

Equations

• RS.EdgeSubset.relabelUp ee F = { flags := F.flags, pairing_mem := ⋯ }

def RS.EdgeSubset.relabelDown {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset (W.relabel ee)) : EdgeSubset W

Transport of an edge subset back along a relabel.

Equations

• RS.EdgeSubset.relabelDown ee F = { flags := F.flags, pairing_mem := ⋯ }

theorem RS.relabelUp_deg {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) (v : W.Vertex) : (EdgeSubset.relabelUp ee F).deg v = F.deg v

Degrees are untouched by a relabel.

theorem RS.relabelUp_eulerian {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) : (EdgeSubset.relabelUp ee F).Eulerian ↔ F.Eulerian

The Eulerian condition is invariant under a relabel.

theorem RS.relabelUp_internalFlags {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) : (EdgeSubset.relabelUp ee F).internalFlags = F.internalFlags

The internal flags are untouched by a relabel.

theorem RS.relabelUp_throughFlags {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) : (EdgeSubset.relabelUp ee F).throughFlags = F.throughFlags

The through flags are untouched by a relabel.

theorem RS.relabelUp_coreFlags {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) : (EdgeSubset.relabelUp ee F).coreFlags = F.coreFlags

The core flags are untouched by a relabel.

The boundary-state matching under a relabel

theorem RS.relabel_genBoundarySubsetMatches_iff {α β : Type} {W : Fragment α} (ee : α ≃ β) {k ℓ : ℕ} (s : Finset W.Flag) (st : GenBoundaryState k ℓ β) : genBoundarySubsetMatches (W.relabel ee) s st ↔ genBoundarySubsetMatches W s fun (a : α) => st (ee a)

The subset boundary constraint reindexes through the equivalence.

Relative transition systems under a relabel

def RS.relabelTransUp {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) (κ : F.RelTransitionSystem) : (EdgeSubset.relabelUp ee F).RelTransitionSystem

Transport of a relative transition system along a relabel.

Equations

• RS.relabelTransUp ee F κ = { match_ := κ.match_, match_invol := ⋯, match_ne := ⋯, match_mem := ⋯, match_vertex := ⋯ }

def RS.relabelTransDown {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) (κ : (EdgeSubset.relabelUp ee F).RelTransitionSystem) : F.RelTransitionSystem

Transport of a relative transition system back along a relabel.

Equations

• RS.relabelTransDown ee F κ = { match_ := κ.match_, match_invol := ⋯, match_ne := ⋯, match_mem := ⋯, match_vertex := ⋯ }

def RS.relabelOrientUp {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) {κ : F.RelTransitionSystem} (o : κ.Orientation) : (relabelTransUp ee F κ).Orientation

Transport of an orientation along a relabel.

Equations

• RS.relabelOrientUp ee F o = { isOut := o.isOut, match_flip := ⋯, pairing_flip := ⋯ }

def RS.relabelOrientDown {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) {κ : (EdgeSubset.relabelUp ee F).RelTransitionSystem} (o : κ.Orientation) : (relabelTransDown ee F κ).Orientation

Transport of an orientation back along a relabel.

Equations

• RS.relabelOrientDown ee F o = { isOut := o.isOut, match_flip := ⋯, pairing_flip := ⋯ }

The open circuit count under a relabel

theorem RS.relabel_iterWalk {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) (κ : F.RelTransitionSystem) (f : W.Flag) (n : ℕ) : EdgeSubset.iterWalk (relabelTransUp ee F κ) f n = EdgeSubset.iterWalk κ f n

The iterated walk is untouched by a relabel.

theorem RS.relabel_periodicFlags {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) (κ : F.RelTransitionSystem) : (relabelTransUp ee F κ).periodicFlags = κ.periodicFlags

The periodic flags are untouched by a relabel.

noncomputable def RS.relabelPeriodicEquiv {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) (κ : F.RelTransitionSystem) : ↥(relabelTransUp ee F κ).periodicFlags ≃ ↥κ.periodicFlags

The periodic-flag subtypes agree under a relabel.

Equations

• RS.relabelPeriodicEquiv ee F κ = { toFun := fun (g : ↥(RS.relabelTransUp ee F κ).periodicFlags) => ⟨↑g, ⋯⟩, invFun := fun (g : ↥κ.periodicFlags) => ⟨↑g, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem RS.relabel_walkPermPeriodic {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) (κ : F.RelTransitionSystem) : (relabelTransUp ee F κ).walkPermPeriodic = (relabelPeriodicEquiv ee F κ).symm.permCongr κ.walkPermPeriodic

The periodic walk permutations agree under the canonical equivalence.

theorem RS.relabel_openCircuitCount {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) (κ : F.RelTransitionSystem) : (relabelTransUp ee F κ).openCircuitCount = κ.openCircuitCount

The open circuit count is untouched by a relabel.

Colourings under a relabel

noncomputable def RS.coreOddRelabelEquiv {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) (ℓ : ℕ) : (EdgeSubset.relabelUp ee F).CoreOddColouring ℓ ≃ F.CoreOddColouring ℓ

The core odd colourings agree under a relabel, via the equality of the core flag sets.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.relabel_evenColoursAt {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) {k : ℕ} (ψ : (EdgeSubset.relabelUp ee F).EvenColouring k) (v : W.Vertex) : (EdgeSubset.relabelUp ee F).evenColoursAt ψ v = F.evenColoursAt ψ v

The even-colour multiset at a vertex is untouched by a relabel.

Vertex-local data under a relabel

theorem RS.relabel_relInFlagsAt {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) {κ : F.RelTransitionSystem} (o : κ.Orientation) (v : W.Vertex) : (EdgeSubset.relabelUp ee F).relInFlagsAt (relabelOrientUp ee F o) v = F.relInFlagsAt o v

The in-flag list at a vertex is untouched by a relabel.

theorem RS.relabel_coreOddListAt {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) {ℓ : ℕ} {κ : F.RelTransitionSystem} (o : κ.Orientation) (φ : (EdgeSubset.relabelUp ee F).CoreOddColouring ℓ) (v : W.Vertex) : (EdgeSubset.relabelUp ee F).coreOddListAt (relabelOrientUp ee F o) φ v = F.coreOddListAt o ((coreOddRelabelEquiv ee F ℓ) φ) v

The vertex odd list is transported by the colouring equivalence.

theorem RS.relabel_coreOddSignAt {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) {ℓ : ℕ} {κ : F.RelTransitionSystem} (o : κ.Orientation) (φ : (EdgeSubset.relabelUp ee F).CoreOddColouring ℓ) (v : W.Vertex) : (EdgeSubset.relabelUp ee F).coreOddSignAt (relabelOrientUp ee F o) φ v = F.coreOddSignAt o ((coreOddRelabelEquiv ee F ℓ) φ) v

The vertex odd sign is transported by the colouring equivalence.

The boundary colour matches under a relabel

theorem RS.relabel_genEvenBoundaryMatch_iff {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) {k ℓ : ℕ} (st : GenBoundaryState k ℓ β) (hbnd : genBoundarySubsetMatches (W.relabel ee) (EdgeSubset.relabelUp ee F).flags st) (hbnd' : genBoundarySubsetMatches W F.flags fun (a : α) => st (ee a)) (ψ : (EdgeSubset.relabelUp ee F).EvenColouring k) : genEvenBoundaryMatch (EdgeSubset.relabelUp ee F) st hbnd ψ ↔ genEvenBoundaryMatch F (fun (a : α) => st (ee a)) hbnd' ψ

The even boundary match reindexes through the equivalence.

theorem RS.relabel_coreOddBoundaryMatch_iff {α β : Type} {W : Fragment α} (ee : α ≃ β) (F : EdgeSubset W) {k ℓ : ℕ} (st : GenBoundaryState k ℓ β) (φ : (EdgeSubset.relabelUp ee F).CoreOddColouring ℓ) : (EdgeSubset.relabelUp ee F).coreOddBoundaryMatch st φ ↔ F.coreOddBoundaryMatch (fun (a : α) => st (ee a)) ((coreOddRelabelEquiv ee F ℓ) φ)

The core odd boundary match reindexes through the equivalence and the colouring equivalence.

The through product under a monotone relabel

theorem RS.relabel_throughProduct {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃o β) {W : Fragment α} (F : EdgeSubset W) {k ℓ : ℕ} (st : GenBoundaryState k ℓ β) : (EdgeSubset.relabelUp e.toEquiv F).throughProduct st = F.throughProduct fun (a : α) => st (e a)

The through product transports along a monotone relabel: the orientation guard is preserved by monotonicity.

The through summand and value under a monotone relabel

theorem RS.relabel_throughSummand {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃o β) {W : Fragment α} (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ β) (hbnd : genBoundarySubsetMatches (W.relabel e.toEquiv) (EdgeSubset.relabelUp e.toEquiv F).flags st) (hbnd' : genBoundarySubsetMatches W F.flags fun (a : α) => st (e a)) {κ : F.RelTransitionSystem} (o : κ.Orientation) (c : ℕ) : (EdgeSubset.relabelUp e.toEquiv F).throughSummand h st hbnd (relabelOrientUp e.toEquiv F o) c = F.throughSummand h (fun (a : α) => st (e a)) hbnd' o c

The corrected constrained summand transports along a monotone relabel, at converted transition data.

The canonical-value migration

The corrected constrained value chooses among path-canonical transition data and weights the chosen summand by the chord-crossing sign. Every ingredient transports along a monotone relabel: the path matching is untouched (the walk and the flag classification are), canonicality transports because labels move monotonically, and the crossing count is invariant because the four chord endpoints of each pair shift through the order isomorphism, which preserves every comparison.

theorem RS.relabelUp_boundaryFlags {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃o β) {W : Fragment α} (F : EdgeSubset W) : (EdgeSubset.relabelUp e.toEquiv F).boundaryFlags = F.boundaryFlags

The boundary flags are untouched by a relabel.

theorem RS.relabel_pathMatch {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃o β) {W : Fragment α} (F : EdgeSubset W) (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ (EdgeSubset.relabelUp e.toEquiv F).boundaryFlags) (hb' : b ∈ F.boundaryFlags) : (relabelTransUp e.toEquiv F κ).pathMatch b hb = κ.pathMatch b hb'

The path matching is untouched by a relabel: the transported walk agrees step by step, so the transported chain data terminate at the same flag.

theorem RS.pathCanonical_relabelUp {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃o β) {W : Fragment α} (F : EdgeSubset W) {κ : F.RelTransitionSystem} {o : κ.Orientation} (hc : EdgeSubset.PathCanonical o) : EdgeSubset.PathCanonical (relabelOrientUp e.toEquiv F o)

Canonicality transport: the transported orientation of a path-canonical orientation is path-canonical — labels transport monotonically, and every other ingredient is untouched.