The gluing-splitting interface #
The through-independence input (choice elimination for the
corrected constrained value) and the single-pair gluing
decomposition, stated as named interfaces: gluing two boundary
labels decomposes the corrected state-constrained value as a state
sum over the glued interface, weighted by the through-state factor.
The unsigned through-independence is refuted in
ThroughIndCFalse.lean; what the development uses in its place is
the signed path-canonical value of PathCanon.lean, whose
within-pairing independence is PropThreeOpen.lean.
noncomputable def
RS.GenBoundaryState.extendPair
{k ℓ : ℕ}
{α : Type}
(i j : α)
(st : GenBoundaryState k ℓ (Fragment.SurvivingLabel α i j))
(c c' : Fin k ⊕ Fin (2 * ℓ))
:
GenBoundaryState k ℓ α
Extension of a boundary state on the surviving labels to the full label type, prescribing the two glued ends.