The final chain: assembling the factorization

The closing assembly of the converse, built entirely from unconditional inputs: the closed identification. On a closed fragment every subset is all-internal, so its chord diagram is empty (labelChords_of_allInternal) — one fibre — and the canonical choice value agrees with the choice-free Definition 5 value (EdgeSubset.throughValueC_eq_mixedValue). Independence across boundary pairings is not needed, there being no boundary.

The closed identification, unconditional

theorem RS.EdgeSubset.throughValueC_eq_mixedValue {W : ClosedFragment} (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ (Fin 0)) (hbnd : genBoundarySubsetMatches W F.flags st) (hE : F.Eulerian) (hint : ∀ f ∈ F.flags, ∃ (v : W.Vertex), W.attach f = Sum.inl v) : F.throughValueC h st hbnd = F.mixedValue h

The canonical constrained value agrees with the Definition 5 value on closed Eulerian subsets — unconditionally: closed chord diagrams are empty, so all canonical data share one fibre.

Membership characterizations (any fragment)

theorem RS.mem_internalFlags_iff {γ : Type} {W : Fragment γ} {F : EdgeSubset W} {f : W.Flag} : f ∈ F.internalFlags ↔ f ∈ F.flags ∧ ∃ (v : W.Vertex), W.attach f = Sum.inl v

Membership in the internal flags, unfolded: a participating flag attached to a vertex.

The canonical-value migration

The corrected (canonical) constrained value pins a path-canonical orientation and weights it by the Pfaffian chord-diagram sign. The factorization migrates: the product of two path-canonical component orientations is path-canonical for the union (chains stay componentwise), and cross-component chords never interleave under any order placing every left label below every right label, so the crossing count — hence the path sign — is additive.

The product system's chain matching

theorem RS.boundaryLabel_inl {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {g : W₁.Flag} (hb : Sum.inl g ∈ F.boundaryFlags) (hb' : g ∈ (leftSub F).boundaryFlags) : F.boundaryLabel hb = Sum.inl ((leftSub F).boundaryLabel hb')

The boundary label of a left-summand boundary flag.

theorem RS.boundaryLabel_inr {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {F : EdgeSubset (W₁.disjUnion W₂)} {g : W₂.Flag} (hb : Sum.inr g ∈ F.boundaryFlags) (hb' : g ∈ (rightSub F).boundaryFlags) : F.boundaryLabel hb = Sum.inr ((rightSub F).boundaryLabel hb')

The boundary label of a right-summand boundary flag.