The corrected independence interface is refutable across pairings

ThroughIndependenceC quantifies over all pairs of transition systems, including pairs with different boundary pairings. On the worked one-vertex instance the two matchings cKappa (chords (0,1), (2,3)) and its repair (chords (0,3), (1,2)) both carry path-canonical orientations (cO, lvO₂flip), both with trivial chord sign, yet the constrained summands differ: −1 versus 0. The canonical value genuinely depends on the boundary pairing — Proposition 3 for open fragments can only assert independence within a pairing (signedValueAt_samePairing), and the interfaces consuming ThroughIndependenceC must be re-based on the pairing-resolved value.

theorem RS.TransposeVerify.cO_pathCanonical : EdgeSubset.PathCanonical cO

cO is path-canonical: both chains run low-to-high with incoming entry edges (isOut 0 = isOut 3 = false).

theorem RS.TransposeVerify.lvO₂flip_pathCanonical : EdgeSubset.PathCanonical lvO₂flip

lvO₂flip is path-canonical on the repaired system: the repaired chords are (0,3) and (1,2), and both low-end entry edges are incoming (isOut 0 = isOut 1 = false).

theorem RS.TransposeVerify.not_throughIndependenceC : ¬ThroughIndependenceC

The cross-pairing refutation: the corrected independence interface fails between path-canonical data with different boundary pairings — the signed canonical values are −1 and 0.