The two-path non-separated transform

The value transformation of the constrained summand under a non-localized repair square whose orientation is non-separated (o.isOut c = o.isOut a). The transported orientation flips the whole boundary chain of c, which is legal because the chain's two ends carry unconstrained boundary partners, and then transports across the now-separated square.

The chain flip is not a scalar at a fixed state: the ∂-reindex of the colour sum meets the boundary at the chain's two end labels, so the flipped summand is a signed summand at a modified state, the two end labels' odd colours replaced by their ∂-partners. Composing with the separated ledger gives the transform, whose factor is minus the product of the two end colours' odd-partner signs.

The two-label ∂-relabel of a boundary state

noncomputable def RS.stateOddFlip {k ℓ : ℕ} {α : Type} (st : GenBoundaryState k ℓ α) (i₁ i₂ : α) : GenBoundaryState k ℓ α

Apply the odd-partner involution to the (odd) state entries at two labels, leaving all other labels untouched.

Equations

• RS.stateOddFlip st i₁ i₂ i = if i = i₁ ∨ i = i₂ then Sum.map id (RS.oddPartner ℓ) (st i) else st i

theorem RS.stateOddFlip_of_ne {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {i₁ i₂ i : α} (h1 : i ≠ i₁) (h2 : i ≠ i₂) : stateOddFlip st i₁ i₂ i = st i

Away from the two labels the state is unchanged.

theorem RS.stateOddFlip_left {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {i₁ i₂ : α} : stateOddFlip st i₁ i₂ i₁ = Sum.map id (oddPartner ℓ) (st i₁)

At the first label the state entry is ∂-flipped.

theorem RS.stateOddFlip_right {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {i₁ i₂ : α} : stateOddFlip st i₁ i₂ i₂ = Sum.map id (oddPartner ℓ) (st i₂)

At the second label likewise.

theorem RS.stateOddFlip_left_odd {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {i₁ i₂ : α} {c : Fin (2 * ℓ)} (hc : st i₁ = Sum.inr c) : stateOddFlip st i₁ i₂ i₁ = Sum.inr (oddPartner ℓ c)

At the first label, on an odd entry: the colour is replaced by its odd partner.

theorem RS.stateOddFlip_right_odd {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {i₁ i₂ : α} {c : Fin (2 * ℓ)} (hc : st i₂ = Sum.inr c) : stateOddFlip st i₁ i₂ i₂ = Sum.inr (oddPartner ℓ c)

At the second label likewise.

theorem RS.stateOddFlip_isInr {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {i₁ i₂ : α} (i : α) : (∃ (c : Fin (2 * ℓ)), stateOddFlip st i₁ i₂ i = Sum.inr c) ↔ ∃ (c : Fin (2 * ℓ)), st i = Sum.inr c

The relabel preserves odd-ness of every entry.

theorem RS.stateOddFlip_isInl {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {i₁ i₂ : α} (i : α) (a : Fin k) : stateOddFlip st i₁ i₂ i = Sum.inl a ↔ st i = Sum.inl a

The relabel fixes every even entry.

theorem RS.genBoundarySubsetMatches_stateOddFlip {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {W : Fragment α} {s : Finset W.Flag} (hbnd : genBoundarySubsetMatches W s st) (i₁ i₂ : α) : genBoundarySubsetMatches W s (stateOddFlip st i₁ i₂)

The boundary-membership constraint transfers across the relabel.

theorem RS.stateOddFlip_stateOddFlip {k ℓ : ℕ} {α : Type} {st : GenBoundaryState k ℓ α} {i₁ i₂ : α} : stateOddFlip (stateOddFlip st i₁ i₂) i₁ i₂ = st

The relabel is an involution.

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

The summand only reads the state and the proof of the boundary constraint is irrelevant: propositionally equal states give equal summands over any proofs.

The ported flip set and the chain-flipped orientation

structure RS.EdgeSubset.PortedFlipSet {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (S : Finset W.Flag) (p₁ p₂ : W.Flag) (i₁ i₂ : α) : Prop

The ported flip set: a set of internal flags closed under the matching and closed under the edge pairing except at two ports p₁, p₂, whose edge partners are the boundary flags of the labels i₁, i₂. The internal-flag support of a full boundary chain is the motivating instance (exists_chainPortedFlipSet).

• int_of_mem (f : W.Flag) : f ∈ S → f ∈ F.internalFlags
• match_mem (f : W.Flag) : f ∈ S → κ.match_ f ∈ S
• pairing_mem (f : W.Flag) : f ∈ S → f ≠ p₁ → f ≠ p₂ → W.pairing f ∈ S
• hp₁S : p₁ ∈ S
• hp₂S : p₂ ∈ S
• hp₁₂ : p₁ ≠ p₂
• hσ₁ : W.pairing p₁ = W.boundaryFlag i₁
• hσ₂ : W.pairing p₂ = W.boundaryFlag i₂

theorem RS.EdgeSubset.PortedFlipSet.hlab {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) : i₁ ≠ i₂

The two port labels are distinct.

theorem RS.EdgeSubset.PortedFlipSet.match_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) {f : W.Flag} (hf : f ∈ F.internalFlags) (hfS : f ∉ S) : κ.match_ f ∉ S

The complement of the flip set is closed under the matching.

theorem RS.EdgeSubset.PortedFlipSet.bF₁_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) : W.pairing (W.boundaryFlag i₁) = p₁

The edge partner of the first port is the first boundary flag.

theorem RS.EdgeSubset.PortedFlipSet.bF₂_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) : W.pairing (W.boundaryFlag i₂) = p₂

The edge partner of the second port is the second boundary flag.

theorem RS.EdgeSubset.PortedFlipSet.attach_inr_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) {f : W.Flag} {i : α} (hat : W.attach f = Sum.inr i) : f ∉ S

Boundary-attached flags are not in the flip set.

theorem RS.EdgeSubset.PortedFlipSet.boundaryFlag_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (i : α) : W.boundaryFlag i ∉ S

Boundary flags are not in the flip set.

theorem RS.EdgeSubset.PortedFlipSet.pairing_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) {f : W.Flag} (hfS : f ∉ S) (h1 : f ≠ W.boundaryFlag i₁) (h2 : f ≠ W.boundaryFlag i₂) : W.pairing f ∉ S

The complement of the flip set is closed under the pairing away from the two boundary ends.

theorem RS.EdgeSubset.PortedFlipSet.int_ne_boundaryFlag {α : Type} {W : Fragment α} {F : EdgeSubset W} {f : W.Flag} (hf : f ∈ F.internalFlags) (i : α) : f ≠ W.boundaryFlag i

Internal flags are never the boundary flags of the ports.

theorem RS.EdgeSubset.PortedFlipSet.p₁_core {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) : p₁ ∈ F.coreFlags

The ports are core flags.

theorem RS.EdgeSubset.PortedFlipSet.p₂_core {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) : p₂ ∈ F.coreFlags

The second port is a core flag.

theorem RS.EdgeSubset.PortedFlipSet.bF₁_core {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) : W.boundaryFlag i₁ ∈ F.coreFlags

The port boundary flags are core flags.

theorem RS.EdgeSubset.PortedFlipSet.bF₂_core {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) : W.boundaryFlag i₂ ∈ F.coreFlags

The second port's boundary end is a core flag — the colour reindexing needs a value there.

noncomputable def RS.EdgeSubset.RelTransitionSystem.Orientation.portFlip {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (o : κ.Orientation) (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) : κ.Orientation

The chain-flipped orientation of the same system: negate isOut exactly on the flip set. The flip is legal at the two ports because their edge partners are boundary flags, whose orientation is unconstrained.

Equations

• o.portFlip h = { isOut := fun (f : W.Flag) => if f ∈ S then !o.isOut f else o.isOut f, match_flip := ⋯, pairing_flip := ⋯ }

theorem RS.EdgeSubset.portFlip_isOut_of_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (o : κ.Orientation) (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) {f : W.Flag} (hf : f ∈ S) : (o.portFlip h).isOut f = !o.isOut f

On the flip set the orientation reverses.

theorem RS.EdgeSubset.portFlip_isOut_of_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (o : κ.Orientation) (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) {f : W.Flag} (hf : f ∉ S) : (o.portFlip h).isOut f = o.isOut f

Off the flip set the orientation is unchanged.

The chain-flip value ledger

The pairing-closed colour-flip core

noncomputable def RS.EdgeSubset.portFlipCore {α : Type} {W : Fragment α} (S : Finset W.Flag) (i₁ i₂ : α) : Finset W.Flag

The flip set together with the two boundary ends: the pairing-closed support of the colour reindexing.

Equations

• RS.EdgeSubset.portFlipCore S i₁ i₂ = insert (W.boundaryFlag i₁) (insert (W.boundaryFlag i₂) S)

theorem RS.EdgeSubset.mem_portFlipCore {α : Type} {W : Fragment α} {S : Finset W.Flag} {i₁ i₂ : α} {f : W.Flag} : f ∈ portFlipCore S i₁ i₂ ↔ f = W.boundaryFlag i₁ ∨ f = W.boundaryFlag i₂ ∨ f ∈ S

Membership in the colour-flip core: the flip set plus the two chain-end boundary flags.

theorem RS.EdgeSubset.mem_portFlipCore_of_mem {α : Type} {W : Fragment α} {S : Finset W.Flag} {i₁ i₂ : α} {f : W.Flag} (hf : f ∈ S) : f ∈ portFlipCore S i₁ i₂

The flip set sits inside its colour-flip core.

theorem RS.EdgeSubset.PortedFlipSet.flipCore_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (f : W.Flag) : f ∈ portFlipCore S i₁ i₂ → W.pairing f ∈ portFlipCore S i₁ i₂

The colour-flip core is fully pairing-closed.

theorem RS.EdgeSubset.PortedFlipSet.mem_flipCore_int {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} : PortedFlipSet κ S p₁ p₂ i₁ i₂ → ∀ {g : W.Flag} (hg : g ∈ F.internalFlags), g ∈ portFlipCore S i₁ i₂ ↔ g ∈ S

On internal flags the colour-flip core is the flip set.

theorem RS.EdgeSubset.PortedFlipSet.mem_flipCore_boundaryFlag {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (i : α) : W.boundaryFlag i ∈ portFlipCore S i₁ i₂ ↔ i = i₁ ∨ i = i₂

On boundary flags the colour-flip core is the two end labels.

The colour reindexing

noncomputable def RS.EdgeSubset.portColourFlip {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {ℓ : ℕ} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (φ : F.CoreOddColouring ℓ) : F.CoreOddColouring ℓ

The ∂-flip of a core odd colouring on the flip set together with the two chain-end edges.

Equations

• RS.EdgeSubset.portColourFlip h φ = RS.EdgeSubset.segFlipColouring ⋯ φ

theorem RS.EdgeSubset.portColourFlip_val {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {ℓ : ℕ} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (φ : F.CoreOddColouring ℓ) (g : ↥F.coreFlags) : ↑(portColourFlip h φ) g = if ↑g ∈ portFlipCore S i₁ i₂ then oddPartner ℓ (↑φ g) else ↑φ g

The reindexed colouring, unfolded: ∂-flipped on the core, unchanged off it.

theorem RS.EdgeSubset.portColourFlip_val_of_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {ℓ : ℕ} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (φ : F.CoreOddColouring ℓ) (g : ↥F.coreFlags) (hg : ↑g ∈ S) : ↑(portColourFlip h φ) g = oddPartner ℓ (↑φ g)

On the flip set the colour is ∂-flipped.

theorem RS.EdgeSubset.portColourFlip_val_int_of_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {ℓ : ℕ} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (φ : F.CoreOddColouring ℓ) (g : ↥F.coreFlags) (hgint : ↑g ∈ F.internalFlags) (hg : ↑g ∉ S) : ↑(portColourFlip h φ) g = ↑φ g

On an internal flag off the flip set the colour is unchanged.

theorem RS.EdgeSubset.portColourFlip_val_bF₁ {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {ℓ : ℕ} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (φ : F.CoreOddColouring ℓ) (hcore : W.boundaryFlag i₁ ∈ F.coreFlags) : ↑(portColourFlip h φ) ⟨W.boundaryFlag i₁, hcore⟩ = oddPartner ℓ (↑φ ⟨W.boundaryFlag i₁, hcore⟩)

At the first chain end the colour is ∂-flipped: this is where the reindexing meets the boundary, and why the transform relabels the state.

theorem RS.EdgeSubset.portColourFlip_val_bF₂ {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {ℓ : ℕ} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (φ : F.CoreOddColouring ℓ) (hcore : W.boundaryFlag i₂ ∈ F.coreFlags) : ↑(portColourFlip h φ) ⟨W.boundaryFlag i₂, hcore⟩ = oddPartner ℓ (↑φ ⟨W.boundaryFlag i₂, hcore⟩)

At the second chain end likewise.

theorem RS.EdgeSubset.portColourFlip_val_bF_of_ne {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {ℓ : ℕ} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (φ : F.CoreOddColouring ℓ) {i : α} (hi₁ : i ≠ i₁) (hi₂ : i ≠ i₂) (hcore : W.boundaryFlag i ∈ F.coreFlags) : ↑(portColourFlip h φ) ⟨W.boundaryFlag i, hcore⟩ = ↑φ ⟨W.boundaryFlag i, hcore⟩

At every other boundary flag the colour is unchanged: only the two chain-end labels move.

theorem RS.EdgeSubset.portColourFlip_involutive {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {ℓ : ℕ} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) : Function.Involutive (portColourFlip h)

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

theorem RS.EdgeSubset.coreOddBoundaryMatch_portColourFlip {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {k ℓ : ℕ} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (st : GenBoundaryState k ℓ α) (φ : F.CoreOddColouring ℓ) : F.coreOddBoundaryMatch st (portColourFlip h φ) ↔ F.coreOddBoundaryMatch (stateOddFlip st i₁ i₂) φ

The boundary-constraint exchange: the flipped colouring matches the original state exactly when the original colouring matches the ∂-relabelled state.

The pairing sign as a total function

Vertex-local in-sets

The flip set split by vertex

The port telescoping

The per-vertex sign identity

The per-vertex list identity

The vertex product and the colouring sum

Pinning the port signs by the boundary constraint

The colouring-sum and even-sum identities

The through product is untouched

The chain-flip ledger

theorem RS.EdgeSubset.psiSum_portFlip {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {k ℓ : ℕ} (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {c₁ c₂ : Fin (2 * ℓ)} (hc₁ : st i₁ = Sum.inr c₁) (hc₂ : st i₂ = Sum.inr c₂) (o : κ.Orientation) : (∑ ψ : F.EvenColouring k, if genEvenBoundaryMatch F st hbnd ψ then ∑ φ : F.CoreOddColouring ℓ, if F.coreOddBoundaryMatch st φ then ∏ vv : W.Vertex, ↑(F.coreOddSignAt (o.portFlip h) φ vv) * hM.evalOdd (F.evenColoursAt ψ vv) (F.coreOddListAt (o.portFlip h) φ vv) else 0 else 0) = ↑(oddPartnerSign ℓ c₁ * oddPartnerSign ℓ c₂) * ∑ ψ : F.EvenColouring k, if genEvenBoundaryMatch F (stateOddFlip st i₁ i₂) ⋯ ψ then ∑ φ : F.CoreOddColouring ℓ, if F.coreOddBoundaryMatch (stateOddFlip st i₁ i₂) φ then ∏ vv : W.Vertex, ↑(F.coreOddSignAt o φ vv) * hM.evalOdd (F.evenColoursAt ψ vv) (F.coreOddListAt o φ vv) else 0 else 0

The chain-flip ledger at the colouring sum: flipping the orientation of a ported chain multiplies the sum over colourings by the two chain-end colour signs and flips the state there. This is the vertex-sum form of the ledger; the through-edge product is untouched, so the constrained summand's form follows.

theorem RS.EdgeSubset.throughSummand_portFlip {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {k ℓ : ℕ} [LinearOrder α] (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (o : κ.Orientation) (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) {c₁ c₂ : Fin (2 * ℓ)} (hc₁ : st i₁ = Sum.inr c₁) (hc₂ : st i₂ = Sum.inr c₂) (n : ℕ) : F.throughSummand hM st hbnd (o.portFlip h) n = ↑(oddPartnerSign ℓ c₁ * oddPartnerSign ℓ c₂) * F.throughSummand hM (stateOddFlip st i₁ i₂) ⋯ o n

The chain-flip ledger: flipping the orientation of a ported flip set (a full boundary chain) multiplies the constrained summand by the two chain-end colour signs and ∂-relabels the state at the two end labels — the local system acts on states. Valid at every circuit exponent.

The boundary chain as a ported flip set

theorem RS.EdgeSubset.exists_chainPortedFlipSet {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {β : W.Flag} (hβ : β ∈ F.boundaryFlags) {kc : ℕ} (hcont : ∀ j < kc, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ β kc) ∈ F.boundaryFlags) (hk : 1 ≤ kc) {iβ iγ : α} (hiβ : W.attach β = Sum.inr iβ) (hiγ : W.attach (W.pairing (iterWalk κ β kc)) = Sum.inr iγ) : ∃ (S : Finset W.Flag), PortedFlipSet κ S (W.pairing β) (iterWalk κ β kc) iβ iγ ∧ (∀ f ∈ S, OnBoundaryChain κ β f) ∧ ∀ f ∈ F.internalFlags, OnBoundaryChain κ β f → f ∈ S

The chain flip set: the internal flags of a full boundary-terminated chain form a ported flip set whose ports are the two chain-end entry flags and whose labels are the chain's two boundary labels.

The two-path non-separated transform

noncomputable def RS.EdgeSubset.twoPathNonSepFactor (ℓ : ℕ) (c₁ c₂ : Fin (2 * ℓ)) : ℂ

The two-path non-separated transform factor: minus the product of the ∂-signs of the two chain-end colours of the original state. Unlike the separated factor −1, it depends on the boundary state (only through those two signs), and the transform additionally ∂-relabels the state at the two chain-end labels.

Equations

• RS.EdgeSubset.twoPathNonSepFactor ℓ c₁ c₂ = -↑(RS.oddPartnerSign ℓ c₁ * RS.oddPartnerSign ℓ c₂)

theorem RS.EdgeSubset.twoPathNonSepFactor_eq (ℓ : ℕ) (c₁ c₂ : Fin (2 * ℓ)) : twoPathNonSepFactor ℓ c₁ c₂ = -↑(oddPartnerSign ℓ c₁ * oddPartnerSign ℓ c₂)

The factor unfolded: minus the product of the two chain-end colours' odd-partner signs.

theorem RS.EdgeSubset.twoPathNonSepFactor_mul_self (ℓ : ℕ) (c₁ c₂ : Fin (2 * ℓ)) : twoPathNonSepFactor ℓ c₁ c₂ * twoPathNonSepFactor ℓ c₁ c₂ = 1

The factor is an involution: the two signs are each ±1.

theorem RS.EdgeSubset.portFlip_separated {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (o : κ.Orientation) (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) {a c : W.Flag} (hsame : o.isOut c = o.isOut a) (hcS : c ∈ S) (haS : a ∉ S) : (o.portFlip h).isOut c = !(o.portFlip h).isOut a

The chain flip separates a non-separated square when c is on the flipped chain and a is off it.

theorem RS.EdgeSubset.twoPathNonSep_transform_exp {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {k ℓ : ℕ} [LinearOrder α] (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) (o : κ.Orientation) (hsame : o.isOut c = o.isOut a) (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (hcS : c ∈ S) (haS : a ∉ S) {c₁ c₂ : Fin (2 * ℓ)} (hc₁ : st i₁ = Sum.inr c₁) (hc₂ : st i₂ = Sum.inr c₂) (n : ℕ) : F.throughSummand hM st hbnd (RelTransitionSystem.Orientation.transportRepair hsq (o.portFlip h) ⋯) n = twoPathNonSepFactor ℓ c₁ c₂ * F.throughSummand hM (stateOddFlip st i₁ i₂) ⋯ o n

The two-path non-separated transform, fixed exponent: with the transported chain-flip orientation, the repaired summand at any circuit exponent is twoPathNonSepFactor times the original summand at the ∂-relabelled state.

theorem RS.EdgeSubset.twoPathNonSep_transform {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {k ℓ : ℕ} [LinearOrder α] (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) (o : κ.Orientation) (hsame : o.isOut c = o.isOut a) (hnl : ¬SquareLocalized κ a b c d) (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) (hcS : c ∈ S) (haS : a ∉ S) {c₁ c₂ : Fin (2 * ℓ)} (hc₁ : st i₁ = Sum.inr c₁) (hc₂ : st i₂ = Sum.inr c₂) : F.throughSummand hM st hbnd (RelTransitionSystem.Orientation.transportRepair hsq (o.portFlip h) ⋯) (κ.repair a b c d v hsq).openCircuitCount = twoPathNonSepFactor ℓ c₁ c₂ * F.throughSummand hM (stateOddFlip st i₁ i₂) ⋯ o κ.openCircuitCount

The two-path non-separated transform (parametric form): for a non-localized square with non-separated orientation, flipping the ported chain of c and transporting across the repair transforms the constrained summand at the open circuit counts by the explicit factor twoPathNonSepFactor ℓ c₁ c₂ = −(sign c₁ · sign c₂) — evaluated at the ∂-relabelled state. The state relabel is intrinsic: the chain flip meets the boundary at the chain's two end labels, so no state-preserving scalar form of the move exists.