A repaired system carrying a path-canonical orientation

The worked one-vertex fragment TransposeVerify (internal flags 0–3, boundary flags 4–7) has three perfect matchings of its internal flags. This module builds the second of them as a repair of the first, lvKappa₂R = cKappa.repair 0 1 2 3, together with an orientation lvO₂flip of it: the one obtained from cO by flipping the boundary chain 5–1–3–6.

Against the fixed functional cFunctional, supported on the colour set {0, 5, 2, 7} adapted to cO, that orientation's constrained summand is 0 (lvSummand₂flip): the flipped in-list carries the colours {0, 7, 1, 6} instead. The summand is computed through lvThroughSummand, which is cThroughSummand with the functional freed so that each orientation can be evaluated against its own delta.

ThroughIndCFalse uses exactly this: cKappa and lvKappa₂R both carry path-canonical orientations with trivial chord sign, yet the summands are −1 and 0, so the canonical value depends on the boundary pairing and independence can only be asserted within one.

The repaired system

def RS.TransposeVerify.lvKappa₂R : cSubset.RelTransitionSystem

cKappa repaired along cSquare (0 1 2 3): the matching 0 ↔ 2, 1 ↔ 3, with chords (4,7) and (5,6).

Equations

• RS.TransposeVerify.lvKappa₂R = RS.TransposeVerify.cKappa.repair 0 1 2 3 RS.TransposeVerify.cV RS.TransposeVerify.cSquare

The flipped orientation

def RS.TransposeVerify.lvO₂flip : lvKappa₂R.Orientation

cO with the boundary chain 5–1–3–6 (flags 1, 3) reversed — the chain carrying the colour 3.

Equations

• RS.TransposeVerify.lvO₂flip = { isOut := ![false, false, true, true, false, false, false, false], match_flip := ⋯, pairing_flip := ⋯ }

The generalized two-in-flag summand

cThroughSummand, restated for an arbitrary functional (the original is pinned to cFunctional); the proof is identical.

theorem RS.TransposeVerify.lvThroughSummand (hM : MixedFunctional 0 4) (κ : cSubset.RelTransitionSystem) (o : κ.Orientation) (g₁ g₂ : Fin 8) (hglist : cSubset.relInFlagsAt o cV = [g₁, g₂]) : cSubset.throughSummand hM cState cBnd o 0 = ↑(oddPartnerSign 4 (cColour (κ.match_ g₁)) * oddPartnerSign 4 (cColour (κ.match_ g₂))) * hM.evalOdd (cSubset.evenColoursAt cPsi cV) [cColour g₁, oddPartner 4 (cColour (κ.match_ g₁)), cColour g₂, oddPartner 4 (cColour (κ.match_ g₂))]

The summand over a two-element in-list at an arbitrary functional: cThroughSummand with the functional freed, so each stage can be evaluated against its own adapted delta.

The summand against the fixed functional

theorem RS.TransposeVerify.lvSummand₂flip : cSubset.throughSummand cFunctional cState cBnd lvO₂flip 0 = 0

The flip kills the summand: the in-list colour set is {0, 7, 1, 6}, outside the support {0, 5, 2, 7} of cFunctional.