Unconditional independence on all-internal subsets

On an all-internal edge subset every participating flag is periodic, so every repair square is localized and the single-step ledger connects any two transition systems: the constrained summand at the open circuit count is independent of all choices — Proposition 3 for the boundary-free sector, as a theorem.

theorem RS.EdgeSubset.squareLocalized_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) : SquareLocalized κ a b c d

On an all-internal subset every repair square is localized: both principal flags are periodic.

theorem RS.EdgeSubset.matchPreservingStep_of_allInternal {α : Type} {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) {κ₁ κ₂ : F.RelTransitionSystem} (h : IsRepairStep κ₁ κ₂) : MatchPreservingStep κ₁ κ₂

On an all-internal subset every repair step preserves the (empty) boundary pairing.

theorem RS.EdgeSubset.throughSummand_independence_of_allInternal {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} (hall : F.allInternal) (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (κ κ' : F.RelTransitionSystem) (o : κ.Orientation) (o' : κ'.Orientation) : F.throughSummand hM st hbnd o κ.openCircuitCount = F.throughSummand hM st hbnd o' κ'.openCircuitCount

Unconditional independence on all-internal subsets: the constrained summand at the open circuit count is independent of the transition system and orientation. (Canonicality is vacuous and the path sign is trivial without boundary flags.)