Invariance of the constrained summand under the repair move

What one elementary 2-opt re-pairing move (RelTransitionSystem.repair) does to the corrected constrained summand (throughSummand).

Main results

• MixedFunctional.evalOdd_transpose — transposing two entries of an odd list (at arbitrary positions) negates the alternating evaluation, unconditionally.
• EdgeSubset.openCircuitCount_matchEq and EdgeSubset.throughSummand_ofMatchEq — matching-equal systems have equal open circuit counts and equal summands (over the transported orientation).
• EdgeSubset.throughSummand_transportRepair — the vertex-v ledger: in the separated case (isOut c = !isOut a, where the orientation transports unchanged), one repair move negates the constrained summand at every fixed circuit exponent. The two changed pair-blocks at v swap their partner entries — one list transposition — while the sign factors merely commute.
• EdgeSubset.throughSummand_repair — the move preserves the summand at the open circuit counts whenever the count parity flips (Odd (count κ + count κ')), by the ledger above.

Why the count-parity hypothesis is needed

The count-parity hypothesis of throughSummand_repair cannot be dropped. A move whose four flags lie on two distinct boundary-terminated paths leaves openCircuitCount unchanged while the ledger still negates the summand, so on such squares the per-move invariance fails. It fails for the reason orientation invariance is restricted to differences on fully internal edges (throughSummand_orientation_invariant in OrientationFlip.lean): a two-path square re-pairs which boundary ends chain together, and the two pairings differ in sign. The two-path squares are handled instead by the pathSign-corrected ledger of PathLedger.lean, whose statements weigh the summand by the boundary pairing's chord sign.

List helpers

The transposition lemma for the alternating evaluation

theorem RS.MixedFunctional.evalOdd_transpose {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (μ : Multiset (Fin k)) (l₂ l₁ l₃ : List (Fin (2 * ℓ))) (x y : Fin (2 * ℓ)) : hM.evalOdd μ (l₁ ++ y :: (l₂ ++ x :: l₃)) = -hM.evalOdd μ (l₁ ++ x :: (l₂ ++ y :: l₃))

Transposing two entries of an odd list, at arbitrary positions, negates the alternating evaluation. Unconditional: when the two entries are equal both sides vanish on the duplicate.

The two-block swap ledger

Orientation-local congruence for the vertex data

theorem RS.EdgeSubset.relInFlagsAt_congr {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} {o₁ : κ₁.Orientation} {o₂ : κ₂.Orientation} (hiso : o₁.isOut = o₂.isOut) (vv : W.Vertex) : F.relInFlagsAt o₁ vv = F.relInFlagsAt o₂ vv

The in-flag list depends on the orientation only through isOut.

theorem RS.EdgeSubset.coreOddListAt_congr {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {κ₁ κ₂ : F.RelTransitionSystem} {o₁ : κ₁.Orientation} {o₂ : κ₂.Orientation} (hiso : o₁.isOut = o₂.isOut) (hmatch : ∀ f ∈ F.internalFlags, κ₁.match_ f = κ₂.match_ f) (φ : F.CoreOddColouring ℓ) (vv : W.Vertex) : F.coreOddListAt o₁ φ vv = F.coreOddListAt o₂ φ vv

The vertex odd list depends only on isOut and the matching at internal flags.

theorem RS.EdgeSubset.coreOddSignAt_congr {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {κ₁ κ₂ : F.RelTransitionSystem} {o₁ : κ₁.Orientation} {o₂ : κ₂.Orientation} (hiso : o₁.isOut = o₂.isOut) (hmatch : ∀ f ∈ F.internalFlags, κ₁.match_ f = κ₂.match_ f) (φ : F.CoreOddColouring ℓ) (vv : W.Vertex) : F.coreOddSignAt o₁ φ vv = F.coreOddSignAt o₂ φ vv

The vertex sign depends only on isOut and the matching at internal flags.

theorem RS.EdgeSubset.throughSummand_congr {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ₁ κ₂ : F.RelTransitionSystem} {o₁ : κ₁.Orientation} {o₂ : κ₂.Orientation} (hiso : o₁.isOut = o₂.isOut) (hmatch : ∀ f ∈ F.internalFlags, κ₁.match_ f = κ₂.match_ f) (n : ℕ) : F.throughSummand hM st hbnd o₁ n = F.throughSummand hM st hbnd o₂ n

The through summand depends only on isOut, the matching at internal flags, and the circuit exponent.

The MatchEq layer

theorem RS.EdgeSubset.iterWalk_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} (heq : κ₁.MatchEq κ₂) {f : W.Flag} (hper : κ₁.PeriodicFlag f) (j : ℕ) : iterWalk κ₂ f j = iterWalk κ₁ f j

Along a κ₁-periodic walk, matching-equal systems walk identically.

theorem RS.EdgeSubset.RelTransitionSystem.PeriodicFlag.matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} (heq : κ₁.MatchEq κ₂) {f : W.Flag} (hper : κ₁.PeriodicFlag f) : κ₂.PeriodicFlag f

Periodicity transfers across matching equality.

theorem RS.EdgeSubset.periodicFlags_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} (heq : κ₁.MatchEq κ₂) : κ₁.periodicFlags = κ₂.periodicFlags

Matching-equal systems have the same periodic flags.

noncomputable def RS.EdgeSubset.periodicEquivMatchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} (heq : κ₁.MatchEq κ₂) : ↥κ₁.periodicFlags ≃ ↥κ₂.periodicFlags

The carrier equivalence of periodicFlags_matchEq.

Equations

• RS.EdgeSubset.periodicEquivMatchEq heq = Equiv.subtypeEquivRight ⋯

theorem RS.EdgeSubset.walkPermPeriodic_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} (heq : κ₁.MatchEq κ₂) : κ₂.walkPermPeriodic = (periodicEquivMatchEq heq).permCongr κ₁.walkPermPeriodic

The periodic walk permutations agree across matching equality.

theorem RS.EdgeSubset.openCircuitCount_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} (heq : κ₁.MatchEq κ₂) : κ₂.openCircuitCount = κ₁.openCircuitCount

Matching-equal systems have equal open circuit counts.

theorem RS.EdgeSubset.throughSummand_ofMatchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ₁ κ₂ : F.RelTransitionSystem} (heq : κ₁.MatchEq κ₂) (o : κ₁.Orientation) (n : ℕ) : F.throughSummand hM st hbnd (RelTransitionSystem.Orientation.ofMatchEq heq o) n = F.throughSummand hM st hbnd o n

Matching-equal systems have equal summands over the transported orientation, at every circuit exponent.

The repair ledger at the vertex

The summand under one separated move

theorem RS.EdgeSubset.throughSummand_transportRepair {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] {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 = -F.throughSummand hM st hbnd o n

The separated-case ledger: one repair move negates the constrained summand at every fixed circuit exponent, over the transported orientation.

theorem RS.EdgeSubset.throughSummand_exp {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] {k ℓ : ℕ} {κ : F.RelTransitionSystem} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (o : κ.Orientation) (n : ℕ) : F.throughSummand hM st hbnd o n = (-1) ^ n * F.throughSummand hM st hbnd o 0

The summand at exponent n factors through exponent 0.

theorem RS.EdgeSubset.throughSummand_repair {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] {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) (hodd : Odd (κ.openCircuitCount + (κ.repair a b c d v hsq).openCircuitCount)) : F.throughSummand hM st hbnd (RelTransitionSystem.Orientation.transportRepair hsq o hflip) (κ.repair a b c d v hsq).openCircuitCount = F.throughSummand hM st hbnd o κ.openCircuitCount

The separated repair step (target shape): when the circuit-count parity flips across the move, the summand at the open circuit counts is preserved, over the transported orientation.