The disjoint-union factorization of the corrected value

The corrected constrained partition value of a disjoint union at a boundary state factors as the product of the componentwise values at the restricted states, with the lexicographic label order on the union. This part supplies the subset and transition-system half; B.lean splits the colourings and the summand, and C.lean migrates canonical data.

The route reindexes the Eulerian subset sum along the componentwise splitting of DisjSubsetSplit, restricts and multiplies boundary-relative transition systems componentwise, adds circuit counts (each component's orbit data is even: the edge-pairing reversal is a fixed-point-free involution on walk orbits), and splits the through product and the colouring sums.

Membership characterizations (any fragment)

Attachment over the union (mirrors DisjSubsetSplit)

theorem RS.attach_inl_eq_inl {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {f : W₁.Flag} {v : W₁.Vertex} : (W₁.disjUnion W₂).attach (Sum.inl f) = Sum.inl (Sum.inl v) ↔ W₁.attach f = Sum.inl v

A left flag attaches to a left vertex over the union exactly when it attaches to that vertex in its own component.

theorem RS.attach_inr_eq_inr {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {f : W₂.Flag} {v : W₂.Vertex} : (W₁.disjUnion W₂).attach (Sum.inr f) = Sum.inl (Sum.inr v) ↔ W₂.attach f = Sum.inl v

The right analogue.

theorem RS.attach_inr_ne_inl {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {f : W₂.Flag} {v : W₁.Vertex} : (W₁.disjUnion W₂).attach (Sum.inr f) ≠ Sum.inl (Sum.inl v)

A right flag never attaches to a left vertex.

theorem RS.attach_inl_ne_inr {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {f : W₁.Flag} {v : W₂.Vertex} : (W₁.disjUnion W₂).attach (Sum.inl f) ≠ Sum.inl (Sum.inr v)

A left flag never attaches to a right vertex.

theorem RS.attach_inl_vertex_iff {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {g : W₁.Flag} : (∃ (v : (W₁.disjUnion W₂).Vertex), (W₁.disjUnion W₂).attach (Sum.inl g) = Sum.inl v) ↔ ∃ (w : W₁.Vertex), W₁.attach g = Sum.inl w

A left flag is internally attached in the union exactly when it is internally attached in the left component.

theorem RS.attach_inr_vertex_iff {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {g : W₂.Flag} : (∃ (v : (W₁.disjUnion W₂).Vertex), (W₁.disjUnion W₂).attach (Sum.inr g) = Sum.inl v) ↔ ∃ (w : W₂.Vertex), W₂.attach g = Sum.inl w

A right flag is internally attached in the union exactly when it is internally attached in the right component.

theorem RS.attach_inl_label_iff {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {g : W₁.Flag} : (∃ (i : α ⊕ β), (W₁.disjUnion W₂).attach (Sum.inl g) = Sum.inr i) ↔ ∃ (i₀ : α), W₁.attach g = Sum.inr i₀

A left flag is boundary over the union exactly when it is boundary in its own component.

theorem RS.attach_inr_label_iff {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {g : W₂.Flag} : (∃ (i : α ⊕ β), (W₁.disjUnion W₂).attach (Sum.inr g) = Sum.inr i) ↔ ∃ (i₀ : β), W₂.attach g = Sum.inr i₀

The right analogue.

theorem RS.pairing_inl {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (g : W₁.Flag) : (W₁.disjUnion W₂).pairing (Sum.inl g) = Sum.inl (W₁.pairing g)

The union's edge pairing on a left flag is the left component's, injected.

theorem RS.pairing_inr {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (g : W₂.Flag) : (W₁.disjUnion W₂).pairing (Sum.inr g) = Sum.inr (W₂.pairing g)

The right analogue.

The component edge subsets

noncomputable def RS.leftSub {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) : EdgeSubset W₁

The left component of an edge subset of a disjoint union.

Equations

• RS.leftSub F = { flags := RS.leftPart F.flags, pairing_mem := ⋯ }

noncomputable def RS.rightSub {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} (F : EdgeSubset (W₁.disjUnion W₂)) : EdgeSubset W₂

The right component of an edge subset of a disjoint union.

Equations

• RS.rightSub F = { flags := RS.rightPart F.flags, pairing_mem := ⋯ }

theorem RS.mem_leftSub_flags {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {g : W₁.Flag} : g ∈ (leftSub F).flags ↔ Sum.inl g ∈ F.flags

Membership in the left component subset.

theorem RS.mem_rightSub_flags {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {g : W₂.Flag} : g ∈ (rightSub F).flags ↔ Sum.inr g ∈ F.flags

Membership in the right component subset.

theorem RS.inl_mem_internal {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {g : W₁.Flag} : Sum.inl g ∈ F.internalFlags ↔ g ∈ (leftSub F).internalFlags

Internality is componentwise on the left.

theorem RS.inr_mem_internal {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {g : W₂.Flag} : Sum.inr g ∈ F.internalFlags ↔ g ∈ (rightSub F).internalFlags

Internality is componentwise on the right.

theorem RS.inl_mem_core {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {g : W₁.Flag} : Sum.inl g ∈ F.coreFlags ↔ g ∈ (leftSub F).coreFlags

Being a core flag is componentwise on the left.

theorem RS.inr_mem_core {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {g : W₂.Flag} : Sum.inr g ∈ F.coreFlags ↔ g ∈ (rightSub F).coreFlags

Being a core flag is componentwise on the right.

Parity of the open orbit data

The edge pairing reverses walk orbits: it is a fixed-point-free involution of the periodic flags conjugating the walk permutation to its inverse. Consequently both the nontrivial cycles and the fixed points of the walk permutation pair up, and the orbit total entering openCircuitCount is even.

Componentwise relative transition systems

Restriction to the components

noncomputable def RS.leftDescend {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ : F.RelTransitionSystem) (g : W₁.Flag) : W₁.Flag

Restrict a union matching to a left flag, fixing it if the image lies on the right.

Equations

• RS.leftDescend κ g = Sum.elim id (fun (x : W₂.Flag) => g) (κ.match_ (Sum.inl g))

noncomputable def RS.rightDescend {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ : F.RelTransitionSystem) (g : W₂.Flag) : W₂.Flag

Restrict a union matching to a right flag, fixing it if the image lies on the left.

Equations

• RS.rightDescend κ g = Sum.elim (fun (x : W₁.Flag) => g) id (κ.match_ (Sum.inr g))

theorem RS.leftDescend_spec {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ : F.RelTransitionSystem) {g : W₁.Flag} (hg : g ∈ (leftSub F).internalFlags) : κ.match_ (Sum.inl g) = Sum.inl (leftDescend κ g)

On an internal left flag, the union system's match is the left descent, injected.

theorem RS.rightDescend_spec {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ : F.RelTransitionSystem) {g : W₂.Flag} (hg : g ∈ (rightSub F).internalFlags) : κ.match_ (Sum.inr g) = Sum.inr (rightDescend κ g)

On an internal right flag, the union system's match is the right descent, injected.

theorem RS.leftDescend_mem {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ : F.RelTransitionSystem) {g : W₁.Flag} (hg : g ∈ (leftSub F).internalFlags) : leftDescend κ g ∈ (leftSub F).internalFlags

The left descent of an internal left flag is again internal.

theorem RS.rightDescend_mem {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ : F.RelTransitionSystem) {g : W₂.Flag} (hg : g ∈ (rightSub F).internalFlags) : rightDescend κ g ∈ (rightSub F).internalFlags

The right descent of an internal right flag is again internal.

noncomputable def RS.leftRel {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ : F.RelTransitionSystem) : (leftSub F).RelTransitionSystem

The restriction of a transition system on the union to its left component: the matching never crosses between components, so it restricts.

Equations

• RS.leftRel κ = { match_ := RS.leftDescend κ, match_invol := ⋯, match_ne := ⋯, match_mem := ⋯, match_vertex := ⋯ }

noncomputable def RS.rightRel {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ : F.RelTransitionSystem) : (rightSub F).RelTransitionSystem

The restriction to the right component.

Equations

• RS.rightRel κ = { match_ := RS.rightDescend κ, match_invol := ⋯, match_ne := ⋯, match_mem := ⋯, match_vertex := ⋯ }

The product system

noncomputable def RS.prodRel {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) : F.RelTransitionSystem

The product of two componentwise transition systems: a system on the union, inverse to the two restrictions.

Equations

• RS.prodRel κ₁ κ₂ = { match_ := Sum.map κ₁.match_ κ₂.match_, match_invol := ⋯, match_ne := ⋯, match_mem := ⋯, match_vertex := ⋯ }

noncomputable def RS.prodOrient {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {κ₁ : (leftSub F).RelTransitionSystem} {κ₂ : (rightSub F).RelTransitionSystem} (o₁ : κ₁.Orientation) (o₂ : κ₂.Orientation) : (prodRel κ₁ κ₂).Orientation

The product of two componentwise orientations.

Equations

• RS.prodOrient o₁ o₂ = { isOut := Sum.elim o₁.isOut o₂.isOut, match_flip := ⋯, pairing_flip := ⋯ }

Circuit count additivity

theorem RS.iterWalk_prodRel_inl {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) (g : W₁.Flag) (n : ℕ) : EdgeSubset.iterWalk (prodRel κ₁ κ₂) (Sum.inl g) n = Sum.inl (EdgeSubset.iterWalk κ₁ g n)

A walk of the product system started at a left flag stays left and tracks the left component's walk.

theorem RS.iterWalk_prodRel_inr {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) (g : W₂.Flag) (n : ℕ) : EdgeSubset.iterWalk (prodRel κ₁ κ₂) (Sum.inr g) n = Sum.inr (EdgeSubset.iterWalk κ₂ g n)

The right analogue.

theorem RS.inl_mem_periodic {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {κ₁ : (leftSub F).RelTransitionSystem} {κ₂ : (rightSub F).RelTransitionSystem} {g : W₁.Flag} : Sum.inl g ∈ (prodRel κ₁ κ₂).periodicFlags ↔ g ∈ κ₁.periodicFlags

A left flag is periodic for the product system exactly when it is periodic for the left factor: the walk never crosses components.

theorem RS.inr_mem_periodic {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {κ₁ : (leftSub F).RelTransitionSystem} {κ₂ : (rightSub F).RelTransitionSystem} {g : W₂.Flag} : Sum.inr g ∈ (prodRel κ₁ κ₂).periodicFlags ↔ g ∈ κ₂.periodicFlags

A right flag is periodic for the product system exactly when it is periodic for the right factor.

noncomputable def RS.periodicSumEquiv {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) : ↥(prodRel κ₁ κ₂).periodicFlags ≃ ↥κ₁.periodicFlags ⊕ ↥κ₂.periodicFlags

The product system's periodic flags are the disjoint sum of the two factors' periodic flags.

Equations

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

theorem RS.walkPermPeriodic_prodRel {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) : (prodRel κ₁ κ₂).walkPermPeriodic = (periodicSumEquiv κ₁ κ₂).symm.permCongr (Equiv.sumCongr κ₁.walkPermPeriodic κ₂.walkPermPeriodic)

Under that identification the product system's walk permutation is the sum of the two factors' walk permutations.

theorem RS.openCircuitCount_prodRel {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) : (prodRel κ₁ κ₂).openCircuitCount = κ₁.openCircuitCount + κ₂.openCircuitCount

Circuit counts add: the product system's open circuit count is the sum of the two components'. Each component's orbit data is even, so no halving correction survives the split.

The through-product factorization