The transpose ledger: the explicit two-path transform factor

The two-path separated move transforms the constrained summand by an explicit factor T. This file pins T down, for the separated orientation class over the transported orientation:

T = twoPathTransformFactor = −1,

independent of the boundary state, of the ∂-data at the four re-paired ends, and of the transition system beyond the two-chain separated configuration. The decomposition behind the constant:

• the vertex bookkeeping contributes the alternating-evaluation transposition sign of the two re-paired pair-blocks at the square's vertex (MixedFunctional.evalOdd_transpose, the engine inside throughSummand_transportRepair): −1;
• the oddPartnerSign factors at the two changed blocks merely commute (+1);
• the colour re-routing between the two chains is, at the sum level, the identity reindexing of the φ-sum: the transported orientation keeps isOut, each repaired chain still carries its boundary colour data along the same strand segments, and only the partner entries of the two vertex blocks swap. So the state-dependent piece is +1 for every boundary state — the colour sets the functional is evaluated on change, but the colourings themselves are not re-indexed.

Main results

• EdgeSubset.twoPathTransformFactor — the explicit factor, (-1 : ℂ) (twoPathTransformFactor_eq_neg_one).
• EdgeSubset.twoPath_transform — the two-path transform: on a two-chain (non-localized) separated square, throughSummand (transportRepair o) (count κ') = T * throughSummand o (count κ) (count invariance openCircuitCount_repair_of_not_localized plus the vertex ledger throughSummand_transportRepair); twoPath_transform_exp is the fixed-exponent form, showing T is exponent-independent.
• TransposeVerify — a worked instance carrying the vocabulary concretely, and the value cSummand_O = −1 that ThroughIndCFalse.lean compares against.

noncomputable def RS.EdgeSubset.twoPathTransformFactor : ℂ

The two-path transform factor: the explicit T of the separated two-path move over the transported orientation. It is the transposition sign of the alternating evaluation at the square's vertex; the oddPartnerSign commutation and the colour re-routing contribute +1 each, so T is constant — independent of the boundary state, the ∂-data at the four re-paired ends, and the transition system.

Equations

• RS.EdgeSubset.twoPathTransformFactor = -1

theorem RS.EdgeSubset.twoPathTransformFactor_eq_neg_one : twoPathTransformFactor = -1

The factor unfolded.

theorem RS.EdgeSubset.twoPath_transform_exp {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (hsq : RepairSquare κ a b c d v) (o : κ.Orientation) (hflip : o.isOut c = !o.isOut a) (n : ℕ) : F.throughSummand hM st hbnd (RelTransitionSystem.Orientation.transportRepair hsq o hflip) n = twoPathTransformFactor * F.throughSummand hM st hbnd o n

The fixed-exponent transform: at every circuit exponent the transported summand is T times the old summand — T is exponent-independent (restating the vertex ledger with the explicit factor).

theorem RS.EdgeSubset.twoPath_transform {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (hsq : RepairSquare κ a b c d v) (o : κ.Orientation) (hflip : o.isOut c = !o.isOut a) (hnl : ¬SquareLocalized κ a b c d) : F.throughSummand hM st hbnd (RelTransitionSystem.Orientation.transportRepair hsq o hflip) (κ.repair a b c d v hsq).openCircuitCount = twoPathTransformFactor * F.throughSummand hM st hbnd o κ.openCircuitCount

The two-path transform: a repair at a two-chain square (twoChains_of_not_localized configuration), separated class, over the transported orientation, transforms the constrained summand at the open circuit counts by the explicit factor T = twoPathTransformFactor = −1 — the circuit count is unchanged and the vertex transposition supplies the sign; the state-dependent ∂-piece of the colour re-routing is trivial at the sum level.

The worked instance

One vertex carrying two boundary-to-boundary paths with disjoint boundary chords: labels 0 < 1 < 2 < 3, chain (0,1) through the matched pair 0 ↔ 1, chain (2,3) through 2 ↔ 3 (flags 0–3 internal, flags 4–7 at the boundary labels), edge assignment pairing = ![4,5,7,6,0,1,3,2]. The square 0 ↔ 1, 2 ↔ 3 is non-localized, the orientation ![F,T,T,F] is separated (isOut 2 = !isOut 0), both circuit counts are 0, and both chord-crossing counts are 0, so both path signs are trivial (cChord_kappa, cPathSign_kappa).

Against the functional supported on the colour set {0,5,2,7} the constrained summand is −1 (cSummand_O). LoopVerify.lean computes the same summand for a repaired system at a flipped orientation, and ThroughIndCFalse.lean reads the two values off to refute independence across boundary pairings.

@[reducible]

def RS.TransposeVerify.cFragment : Fragment (Fin 4)

One vertex, four pendant edges: flags 0–3 at the vertex, flags 4–7 at boundary labels 0–3; edges {0,4}, {1,5}, {3,6}, {2,7}.

Equations

• One or more equations did not get rendered due to their size.

def RS.TransposeVerify.cV : cFragment.Vertex

The unique vertex.

Equations

• RS.TransposeVerify.cV = ()

def RS.TransposeVerify.cSubset : EdgeSubset cFragment

The full edge subset.

Equations

• RS.TransposeVerify.cSubset = { flags := Finset.univ, pairing_mem := RS.TransposeVerify.cSubset._proof_1 }

def RS.TransposeVerify.cMatch : Fin 8 → Fin 8

The verification instance's matching: 0 ↔ 1, 2 ↔ 3 at the single vertex, boundary flags fixed.

Equations

• RS.TransposeVerify.cMatch = ![1, 0, 3, 2, 4, 5, 6, 7]

theorem RS.TransposeVerify.cInternal_cases {f : Fin 8} (hf : f ∈ cSubset.internalFlags) : f = 0 ∨ f = 1 ∨ f = 2 ∨ f = 3

The instance's internal flags are exactly 0–3.

theorem RS.TransposeVerify.cMem_internal {f : Fin 8} (hf : f = 0 ∨ f = 1 ∨ f = 2 ∨ f = 3) : f ∈ cSubset.internalFlags

Each of 0–3 is an internal flag.

theorem RS.TransposeVerify.cMem_boundary {f : Fin 8} (i : Fin 4) (h : cFragment.attach f = Sum.inr i) : f ∈ cSubset.boundaryFlags

A boundary-attached flag is a boundary flag.

theorem RS.TransposeVerify.cBoundary_cases {f : Fin 8} (hf : f ∈ cSubset.boundaryFlags) : f = 4 ∨ f = 5 ∨ f = 6 ∨ f = 7

The instance's boundary flags are exactly 4–7.

def RS.TransposeVerify.cKappa : cSubset.RelTransitionSystem

The matching 0 ↔ 1, 2 ↔ 3: two boundary chains with disjoint chords (0,1) and (2,3).

Equations

• RS.TransposeVerify.cKappa = { match_ := RS.TransposeVerify.cMatch, match_invol := ⋯, match_ne := ⋯, match_mem := ⋯, match_vertex := ⋯ }

theorem RS.TransposeVerify.cSquare : EdgeSubset.RepairSquare cKappa 0 1 2 3 cV

The square 0 ↔ 1, 2 ↔ 3 at the vertex.

def RS.TransposeVerify.cO : cKappa.Orientation

The separated, path-canonical orientation: both chains enter the vertex through their low-label ends.

Equations

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

def RS.TransposeVerify.cState : GenBoundaryState 0 4 (Fin 4)

The boundary state: odd colours 0, 1, 2, 3 at labels 0, 1, 2, 3.

Equations

• RS.TransposeVerify.cState = ![Sum.inr 0, Sum.inr 1, Sum.inr 2, Sum.inr 3]

theorem RS.TransposeVerify.cBnd : genBoundarySubsetMatches cFragment cSubset.flags cState

The state matches the fragment's boundary: each of the four legs carries the colour the state names.

noncomputable def RS.TransposeVerify.cFunctional : MixedFunctional 0 4

The functional supported on the colour set {0, 5, 2, 7} (the odd-list set of the original summand).

Equations

• RS.TransposeVerify.cFunctional x✝ s = if s = {0, 5, 2, 7} then 1 else 0

theorem RS.TransposeVerify.cFunctional_apply (μ : Multiset (Fin 0)) (s : Finset (Fin (2 * 4))) : cFunctional μ s = if s = {0, 5, 2, 7} then 1 else 0

The functional's values, unfolded: 1 at the original summand's odd-list set and 0 elsewhere.

The pinned core colouring

theorem RS.TransposeVerify.cCoreFlags : cSubset.coreFlags = Finset.univ

Every flag is a core flag.

theorem RS.TransposeVerify.cThroughFlags : cSubset.throughFlags = ∅

No flag is a through flag: both boundary chains pass through the vertex.

theorem RS.TransposeVerify.cThroughProduct : cSubset.throughProduct cState = 1

With no through flags the through product is 1, so it drops out of both summands being compared.

def RS.TransposeVerify.cColour : Fin 8 → Fin (2 * 4)

The edge colours: edge {0,4} gets 0, {1,5} gets 1, {3,6} gets 2, {2,7} gets 3.

Equations

• RS.TransposeVerify.cColour = ![0, 1, 3, 2, 0, 1, 2, 3]

noncomputable def RS.TransposeVerify.cPhi : cSubset.CoreOddColouring 4

The pinned core odd colouring.

Equations

• RS.TransposeVerify.cPhi = ⟨fun (g : ↥RS.TransposeVerify.cSubset.coreFlags) => RS.TransposeVerify.cColour ↑g, ⋯⟩

instance RS.TransposeVerify.instIsEmptySubtypeFlagFinOfNatNatCFragmentNotMemFinsetFlagsCSubset : IsEmpty { f : cFragment.Flag // f ∉ cSubset.flags }

Every flag participates, so there are no non-participating flags to colour.

noncomputable def RS.TransposeVerify.cPsi : cSubset.EvenColouring 0

The unique (empty) even colouring.

Equations

• RS.TransposeVerify.cPsi = ⟨fun (f : { f : RS.TransposeVerify.cFragment.Flag // f ∉ RS.TransposeVerify.cSubset.flags }) => isEmptyElim f, RS.TransposeVerify.cPsi._proof_2⟩

instance RS.TransposeVerify.instSubsingletonEvenColouringFinOfNatNatCSubset : Subsingleton (cSubset.EvenColouring 0)

The even colouring is unique: there is nothing to choose.

theorem RS.TransposeVerify.cEvenMatch : genEvenBoundaryMatch cSubset cState cBnd cPsi

The empty even colouring matches the state's even part: with k = 0 there is nothing to check.

theorem RS.TransposeVerify.cOddMatch : cSubset.coreOddBoundaryMatch cState cPhi

The pinned colouring is boundary-matched.

theorem RS.TransposeVerify.cPhi_unique (φ : cSubset.CoreOddColouring 4) (hB : cSubset.coreOddBoundaryMatch cState φ) : φ = cPhi

The colouring is forced: every boundary-matched core odd colouring is the pinned one, so each summand is a single term.

Two-element in-lists

theorem RS.TransposeVerify.list_pair_cases {γ : Type} {x y : γ} {l : List γ} (hxy : x ≠ y) (hnd : l.Nodup) (hmem : ∀ (g : γ), g ∈ l ↔ g = x ∨ g = y) : l = [x, y] ∨ l = [y, x]

A duplicate-free list whose members are exactly two distinct elements is one of the two orderings of that pair.

theorem RS.TransposeVerify.cRelIn_pair {κ : cSubset.RelTransitionSystem} (o : κ.Orientation) {i0 i1 i2 i3 : Bool} (h0 : o.isOut 0 = i0) (h1 : o.isOut 1 = i1) (h2 : o.isOut 2 = i2) (h3 : o.isOut 3 = i3) (g₁ g₂ : Fin 8) (hne : g₁ ≠ g₂) (hpat : ∀ (g : Fin 8), g = 0 ∧ i0 = false ∨ g = 1 ∧ i1 = false ∨ g = 2 ∧ i2 = false ∨ g = 3 ∧ i3 = false ↔ g = g₁ ∨ g = g₂) : cSubset.relInFlagsAt o cV = [g₁, g₂] ∨ cSubset.relInFlagsAt o cV = [g₂, g₁]

The in-flag list at the vertex, up to order, read off an orientation's isOut table: the two flags oriented inwards.

The summand over a two-element in-list

theorem RS.TransposeVerify.cCoreOddSignAt (κ : cSubset.RelTransitionSystem) (o : κ.Orientation) (g₁ g₂ : Fin 8) (hglist : cSubset.relInFlagsAt o cV = [g₁, g₂]) : cSubset.coreOddSignAt o cPhi cV = oddPartnerSign 4 (cColour (κ.match_ g₁)) * oddPartnerSign 4 (cColour (κ.match_ g₂))

The vertex sign over a two-element in-list: the product of the two entry partners' oddPartnerSigns.

theorem RS.TransposeVerify.cCoreOddListAt (κ : cSubset.RelTransitionSystem) (o : κ.Orientation) (g₁ g₂ : Fin 8) (hglist : cSubset.relInFlagsAt o cV = [g₁, g₂]) : cSubset.coreOddListAt o cPhi cV = [cColour g₁, oddPartner 4 (cColour (κ.match_ g₁)), cColour g₂, oddPartner 4 (cColour (κ.match_ g₂))]

The vertex odd list over a two-element in-list: each in-flag's colour followed by its match's partner colour.

theorem RS.TransposeVerify.cThroughSummand (κ : cSubset.RelTransitionSystem) (o : κ.Orientation) (g₁ g₂ : Fin 8) (hglist : cSubset.relInFlagsAt o cV = [g₁, g₂]) : cSubset.throughSummand cFunctional cState cBnd o 0 = ↑(oddPartnerSign 4 (cColour (κ.match_ g₁)) * oddPartnerSign 4 (cColour (κ.match_ g₂))) * cFunctional.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: with the colouring forced and the through product trivial, the whole summand is the single vertex factor.

Open circuit counts

theorem RS.TransposeVerify.cPeriodic_empty (κ : cSubset.RelTransitionSystem) : κ.periodicFlags = ∅

No system on this instance has periodic flags: every flag lies on a boundary-to-boundary chain.

theorem RS.TransposeVerify.cNot_periodic (κ : cSubset.RelTransitionSystem) (f : Fin 8) : ¬κ.PeriodicFlag f

Pointwise form of cPeriodic_empty.

theorem RS.TransposeVerify.cCount_zero (κ : cSubset.RelTransitionSystem) : κ.openCircuitCount = 0

Every system on this instance has open circuit count 0, so the original and repaired summands are compared at the same loop weight.

Path matchings and chord-crossing counts

theorem RS.TransposeVerify.cPathMatch_eval (κ : cSubset.RelTransitionSystem) {β x g : Fin 8} (hβ : β ∈ cSubset.boundaryFlags) (h1 : cFragment.pairing β = x) (hx : x ∈ cSubset.internalFlags) (h2 : cFragment.pairing (κ.match_ x) = g) (hg : g ∈ cSubset.boundaryFlags) : κ.pathMatch β hβ = g

Path-match evaluation along a one-internal-step chain: enter at β, cross to x, match, leave at g.

theorem RS.TransposeVerify.cPM_4 (h : 4 ∈ cSubset.boundaryFlags) : cKappa.pathMatch 4 h = 5

The original system's chain from 4 ends at 5.

theorem RS.TransposeVerify.cPM_5 (h : 5 ∈ cSubset.boundaryFlags) : cKappa.pathMatch 5 h = 4

The original system's chain from 5 ends at 4.

theorem RS.TransposeVerify.cPM_6 (h : 6 ∈ cSubset.boundaryFlags) : cKappa.pathMatch 6 h = 7

The original system's chain from 6 ends at 7.

theorem RS.TransposeVerify.cPM_7 (h : 7 ∈ cSubset.boundaryFlags) : cKappa.pathMatch 7 h = 6

The original system's chain from 7 ends at 6.

theorem RS.TransposeVerify.cPM'_4 (h : 4 ∈ cSubset.boundaryFlags) : (cKappa.repair 0 1 2 3 cV cSquare).pathMatch 4 h = 7

The repaired system re-pairs the boundary: its chain from 4 ends at 7, not 5.

theorem RS.TransposeVerify.cPM'_5 (h : 5 ∈ cSubset.boundaryFlags) : (cKappa.repair 0 1 2 3 cV cSquare).pathMatch 5 h = 6

The repaired system's chain from 5 ends at 6.

theorem RS.TransposeVerify.cPM'_6 (h : 6 ∈ cSubset.boundaryFlags) : (cKappa.repair 0 1 2 3 cV cSquare).pathMatch 6 h = 5

The repaired system's chain from 6 ends at 5.

theorem RS.TransposeVerify.cPM'_7 (h : 7 ∈ cSubset.boundaryFlags) : (cKappa.repair 0 1 2 3 cV cSquare).pathMatch 7 h = 4

The repaired system's chain from 7 ends at 4.

theorem RS.TransposeVerify.cChord_label {κ : cSubset.RelTransitionSystem} {x g : Fin 8} {hx : x ∈ cSubset.boundaryFlags} {i j : Fin 4} (hpm : κ.pathMatch x hx = g) (h1 : cFragment.attach x = Sum.inr i) (h2 : cFragment.attach (κ.pathMatch x hx) = Sum.inr j) {i0 j0 : Fin 4} (hxa : cFragment.attach x = Sum.inr i0) (hga : cFragment.attach g = Sum.inr j0) : i = i0 ∧ j = j0

Reading a chord's two labels off a chain: the labels recorded by attach at the chain's ends are the chord's.

theorem RS.TransposeVerify.cChord_empty (κ : cSubset.RelTransitionSystem) (hpair : ∀ (x : Fin 8) (hx : x ∈ cSubset.boundaryFlags) (i j : Fin 4), cFragment.attach x = Sum.inr i → cFragment.attach (κ.pathMatch x hx) = Sum.inr j → i = 0 ∧ j = 1 ∨ i = 1 ∧ j = 0 ∨ i = 2 ∧ j = 3 ∨ i = 3 ∧ j = 2 ∨ i = 0 ∧ j = 3 ∨ i = 3 ∧ j = 0 ∨ i = 1 ∧ j = 2 ∨ i = 2 ∧ j = 1) : EdgeSubset.chordCrossingCount κ = 0

A system whose chords all join adjacent labels has no interleaving pair, hence crossing count 0.

theorem RS.TransposeVerify.cChord_kappa : EdgeSubset.chordCrossingCount cKappa = 0

The original system's chords (0,1) and (2,3) are disjoint: crossing count 0.

theorem RS.TransposeVerify.cChord_repair : EdgeSubset.chordCrossingCount (cKappa.repair 0 1 2 3 cV cSquare) = 0

The repaired system's chords (0,3) and (1,2) nest: crossing count 0 as well.

theorem RS.TransposeVerify.cPathSign_kappa : EdgeSubset.pathSign cKappa = 1

The original path sign is 1.

theorem RS.TransposeVerify.cPathSign_repair : EdgeSubset.pathSign (cKappa.repair 0 1 2 3 cV cSquare) = 1

The repaired path sign is 1 too — so the factor the two summands differ by is not the chord sign.

The two summand values

theorem RS.TransposeVerify.cSummand_O : cSubset.throughSummand cFunctional cState cBnd cO 0 = -1

The original summand is −1.