Orientation invariance of the constrained summand: circuit flips

For a fixed boundary-relative transition system κ, the corrected constrained summand throughSummand is invariant under changing the orientation, provided every internal flag on which the two orientations disagree has an internal pairing partner — that is, the difference set is supported on fully internal edges (equivalently, on closed circuits; flips of path components are excluded).

The proof

The difference set orientDiff o o' of two orientations is closed under the matching (from both match_flips) and — under the pairing-internality hypothesis — under the edge pairing (from both pairing_flips). The colouring reindexing flipColouring applies the odd-partner involution ∂ edge-wise on the difference set; it is an involution of the core odd colourings fixing all boundary flags, so the odd boundary constraint is preserved. At each vertex the in-flags under o' are the unflipped in-flags under o together with the matches of the flipped ones; each flipped visit contributes a reversed pair block (one adjacent-swap sign) and trades the sign factor ∂-partner-sign of the outgoing colour for that of the incoming one. The two (−1)s per visit cancel, and the leftover ratio sign(in) · sign(out) telescopes over the whole vertex product to ∏_{f ∈ diff} sign(φ f), which is 1 because the difference set is a disjoint union of full edges and the colouring is pairing-constant.

Why the hypothesis is necessary

Unrestricted orientation invariance is false. Counterexample (ℓ = 2): one vertex v with two pendant edges {f₁, b₁}, {f₂, b₂} to boundary labels i₁, i₂, the matching f₁ ↔ f₂, and odd state colours st i₁ = 0, st i₂ = 1. The boundary constraint pins the unique contributing colouring, and the two orientations of the path give summands proportional to −h(μ, {0, 3}) and −h(μ, {1, 2}) respectively — different for generic h. The per-visit sign ratio sign(x)·sign(y) telescopes to 1 only around closed circuits; on a path it leaves the pinned end-colour signs, and the ∂-reindexing moreover violates the pinned boundary values. Consequently any orientation-independence interface must restrict to circuit-supported differences (or fix path orientations by convention).

Bool helpers

The difference set of two orientations

noncomputable def RS.EdgeSubset.orientDiff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) : Finset W.Flag

The internal flags on which two orientations of the same relative transition system disagree.

Equations

• RS.EdgeSubset.orientDiff o o' = {f ∈ F.internalFlags | o.isOut f ≠ o'.isOut f}

theorem RS.EdgeSubset.mem_orientDiff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o' : κ.Orientation} {f : W.Flag} : f ∈ orientDiff o o' ↔ f ∈ F.internalFlags ∧ o.isOut f ≠ o'.isOut f

Membership in the difference set: an internal flag the two orientations direct oppositely.

theorem RS.EdgeSubset.orientDiff_subset_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) {f : W.Flag} (hf : f ∈ orientDiff o o') : f ∈ F.internalFlags

The difference set consists of internal flags.

theorem RS.EdgeSubset.isOut_eq_of_notMem_orientDiff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o' : κ.Orientation} {f : W.Flag} (hf : f ∈ F.internalFlags) (hnot : f ∉ orientDiff o o') : o.isOut f = o'.isOut f

Off the difference set, internal flags are oriented identically.

theorem RS.EdgeSubset.match_mem_orientDiff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o' : κ.Orientation} {f : W.Flag} (hf : f ∈ orientDiff o o') : κ.match_ f ∈ orientDiff o o'

The difference set is closed under the matching.

theorem RS.EdgeSubset.match_notMem_orientDiff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o' : κ.Orientation} {f : W.Flag} (hf : f ∈ F.internalFlags) (hnot : f ∉ orientDiff o o') : κ.match_ f ∉ orientDiff o o'

The complement of the difference set is closed under the matching on internal flags.

theorem RS.EdgeSubset.pairing_mem_orientDiff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o' : κ.Orientation} (hpair : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) {f : W.Flag} (hf : f ∈ orientDiff o o') : W.pairing f ∈ orientDiff o o'

Under the pairing-internality hypothesis, the difference set is closed under the edge pairing.

theorem RS.EdgeSubset.pairing_notMem_orientDiff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o' : κ.Orientation} (hpair : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) {f : W.Flag} (hnot : f ∉ orientDiff o o') : W.pairing f ∉ orientDiff o o'

The complement of the difference set is closed under the pairing.

theorem RS.EdgeSubset.boundaryFlag_notMem_orientDiff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (i : α) : W.boundaryFlag i ∉ orientDiff o o'

Boundary flags are never in the difference set.

The colouring reindexing

noncomputable def RS.EdgeSubset.flipColouring {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hpair : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) : F.CoreOddColouring ℓ

The ∂-flip of a core odd colouring on the edges of the difference set: the crux bijection for orientation invariance.

Equations

• RS.EdgeSubset.flipColouring o o' hpair φ = ⟨fun (g : ↥F.coreFlags) => if ↑g ∈ RS.EdgeSubset.orientDiff o o' then RS.oddPartner ℓ (↑φ g) else ↑φ g, ⋯⟩

theorem RS.EdgeSubset.flipColouring_val_of_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hpair : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) (g : ↥F.coreFlags) (hg : ↑g ∈ orientDiff o o') : ↑(flipColouring o o' hpair φ) g = oddPartner ℓ (↑φ g)

On the difference set the colouring is ∂-flipped.

theorem RS.EdgeSubset.flipColouring_val_of_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hpair : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) (g : ↥F.coreFlags) (hg : ↑g ∉ orientDiff o o') : ↑(flipColouring o o' hpair φ) g = ↑φ g

Off it the colouring is unchanged.

theorem RS.EdgeSubset.inSign_flipColouring_of_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hpair : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) {g : W.Flag} (hg : g ∈ orientDiff o o') : inSign (flipColouring o o' hpair φ) g = -inSign φ g

The flip negates the incoming sign on the difference set: the flip colouring is the colour flip on orientDiff o o'.

theorem RS.EdgeSubset.inSign_flipColouring_of_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hpair : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) {g : W.Flag} (hg : g ∉ orientDiff o o') : inSign (flipColouring o o' hpair φ) g = inSign φ g

The flip leaves the incoming sign off the difference set alone.

theorem RS.EdgeSubset.flipColouring_involutive {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hpair : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) {ℓ : ℕ} : Function.Involutive (flipColouring o o' hpair)

The flip is an involution, so it is a bijection of the colouring sum.

theorem RS.EdgeSubset.coreOddBoundaryMatch_flipColouring {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {k ℓ : ℕ} (st : GenBoundaryState k ℓ α) (o o' : κ.Orientation) (hpair : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) (φ : F.CoreOddColouring ℓ) : F.coreOddBoundaryMatch st (flipColouring o o' hpair φ) ↔ F.coreOddBoundaryMatch st φ

The reindexing preserves the odd boundary constraint.

Vertex-local in-sets

Signs as finset products

The global sign telescopes

The pair-list reindexing

Assembly

The orientation-invariance theorems

theorem RS.EdgeSubset.throughSummand_orientation_invariant {α : Type} {W : Fragment α} [LinearOrder α] (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hpair : ∀ f ∈ F.internalFlags, o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags) (c : ℕ) : F.throughSummand h st hbnd o c = F.throughSummand h st hbnd o' c

Invariance under circuit flips: for a fixed relative transition system, the corrected constrained summand is invariant under changing the orientation, provided every internal flag on which the orientations disagree lies on a fully internal edge. (Unrestricted invariance is false: flipping a boundary-to-boundary path changes the summand — see the module docstring.)

Necessity of the hypothesis: a path-flip counterexample

One vertex with two pendant edges to boundary labels 0 < 1, the matching joining the two internal flags, and odd state colours 0 and 1 (with ℓ = 2). The odd boundary constraint pins the unique contributing colouring; the two orientations of the resulting boundary-to-boundary path give summands −1 and 0 for the functional supported on the colour set {0, 3}.