Through-edges and the corrected constrained value

A participating edge of an open fragment both of whose flags are boundary flags (a through-edge) carries no vertex data; its two ends must take independent state colours, paired by the symplectic copairing — full pairing-constancy of the odd colouring would force the two ends equal, exactly where the symplectic weight vanishes. This file splits the participating flags into core and through parts, restricts the odd colouring to the core, and defines the corrected constrained summand: the core colouring sum times an explicit symplectic factor per through-edge, oriented by the label order.

Even colourings stay fully pairing-constant: the even gluing weight is diagonal, which pairing-constancy implements already.

Core and through flags

noncomputable def RS.EdgeSubset.throughFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) : Finset W.Flag

The through-flags: participating flags on boundary–boundary edges.

Equations

• F.throughFlags = {f ∈ F.flags | (∃ (i : α), W.attach f = Sum.inr i) ∧ ∃ (j : α), W.attach (W.pairing f) = Sum.inr j}

noncomputable def RS.EdgeSubset.coreFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) : Finset W.Flag

The core flags: participating flags on edges with at least one internal end.

Equations

• F.coreFlags = F.flags \ F.throughFlags

theorem RS.EdgeSubset.coreFlags_subset {α : Type} {W : Fragment α} (F : EdgeSubset W) : F.coreFlags ⊆ F.flags

Core flags participate.

theorem RS.EdgeSubset.mem_coreFlags_iff {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} : f ∈ F.coreFlags ↔ f ∈ F.flags ∧ ((∃ (v : W.Vertex), W.attach f = Sum.inl v) ∨ ∃ (v : W.Vertex), W.attach (W.pairing f) = Sum.inl v)

A participating flag is core when it or its edge partner meets a vertex — through-edges, meeting none, are excluded.

theorem RS.EdgeSubset.pairing_mem_coreFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} (hf : f ∈ F.coreFlags) : W.pairing f ∈ F.coreFlags

The pairing preserves the core flags.

theorem RS.EdgeSubset.internalFlags_subset_coreFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) : F.internalFlags ⊆ F.coreFlags

Internal flags are core flags.

The core odd colouring

def RS.EdgeSubset.CoreOddColouring {α : Type} {W : Fragment α} (F : EdgeSubset W) (ℓ : ℕ) : Type

Odd colourings of the core: pairing-constant colours on the participating flags of edges with an internal end.

Equations

• F.CoreOddColouring ℓ = { φ : ↥F.coreFlags → Fin (2 * ℓ) // ∀ (f : ↥F.coreFlags), φ ⟨W.pairing ↑f, ⋯⟩ = φ f }

@[instance_reducible]

noncomputable instance RS.EdgeSubset.CoreOddColouring.instFintype {α : Type} {W : Fragment α} (F : EdgeSubset W) (ℓ : ℕ) : Fintype (F.CoreOddColouring ℓ)

Core odd colourings are finite in number, so the summand's sum over them is a finite sum.

Equations

• RS.EdgeSubset.CoreOddColouring.instFintype F ℓ = id inferInstance

Vertex-local data over the core colouring

noncomputable def RS.EdgeSubset.coreOddPairFn {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} (κ : F.RelTransitionSystem) (φ : F.CoreOddColouring ℓ) (f : ↥F.internalFlags) : List (Fin (2 * ℓ))

The odd pair contributed by an incoming internal flag, from the core colouring.

Equations

• F.coreOddPairFn κ φ f = [↑φ ⟨↑f, ⋯⟩, RS.oddPartner ℓ (↑φ ⟨κ.match_ ↑f, ⋯⟩)]

noncomputable def RS.EdgeSubset.coreOddSignFn {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} (κ : F.RelTransitionSystem) (φ : F.CoreOddColouring ℓ) (f : ↥F.internalFlags) : ℤ

The odd-pairing sign contributed by an incoming internal flag, from the core colouring.

Equations

• F.coreOddSignFn κ φ f = RS.oddPartnerSign ℓ (↑φ ⟨κ.match_ ↑f, ⋯⟩)

noncomputable def RS.EdgeSubset.coreOddListAt {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} {κ : F.RelTransitionSystem} (o : κ.Orientation) (φ : F.CoreOddColouring ℓ) (v : W.Vertex) : List (Fin (2 * ℓ))

The odd-colour list at a vertex, from the core colouring.

Equations

• F.coreOddListAt o φ v = List.flatMap (F.coreOddPairFn κ φ) ((F.relInFlagsAt o v).attachWith (fun (x : W.Flag) => x ∈ F.internalFlags) ⋯)

noncomputable def RS.EdgeSubset.coreOddSignAt {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} {κ : F.RelTransitionSystem} (o : κ.Orientation) (φ : F.CoreOddColouring ℓ) (v : W.Vertex) : ℤ

The odd-pairing sign at a vertex, from the core colouring.

Equations

• F.coreOddSignAt o φ v = (List.map (F.coreOddSignFn κ φ) ((F.relInFlagsAt o v).attachWith (fun (x : W.Flag) => x ∈ F.internalFlags) ⋯)).prod

The through-edge symplectic factor

noncomputable def RS.oddThroughFactor (ℓ : ℕ) (c c' : Fin (2 * ℓ)) : ℂ

The symplectic copairing weight of an odd through-edge: nonzero exactly on partner colours, with the partner sign of the lower-label end. (The sign convention is validated by the strand identity in the gluing decomposition.)

Equations

• RS.oddThroughFactor ℓ c c' = if c' = RS.oddPartner ℓ c then ↑(RS.oddPartnerSign ℓ c) else 0

noncomputable def RS.throughStateFactor {k ℓ : ℕ} (c c' : Fin k ⊕ Fin (2 * ℓ)) : ℂ

The state weight of a through-edge, by the parity of its two end states: diagonal on even colours, symplectic on odd colours, zero on mixed parities.

Equations

• RS.throughStateFactor (Sum.inl a) (Sum.inl a') = if a' = a then 1 else 0
• RS.throughStateFactor (Sum.inr b) (Sum.inr b') = RS.oddThroughFactor ℓ b b'
• RS.throughStateFactor c c' = 0

noncomputable def RS.EdgeSubset.throughProduct {α : Type} {W : Fragment α} [LinearOrder α] {k ℓ : ℕ} (F : EdgeSubset W) (st : GenBoundaryState k ℓ α) : ℂ

The through-edge state weight of an edge subset: each through-edge contributes its state factor exactly once, from its lower-label flag.

Equations

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

def RS.EdgeSubset.coreOddBoundaryMatch {α : Type} {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (st : GenBoundaryState k ℓ α) (φ : F.CoreOddColouring ℓ) : Prop

The core odd boundary constraint: the state's odd colours are imposed on the core boundary flags (through-edges are constrained by the through factor instead).

Equations

• F.coreOddBoundaryMatch st φ = ∀ (i : α) (c : Fin (2 * ℓ)), st i = Sum.inr c → ∀ (hcore : W.boundaryFlag i ∈ F.coreFlags), ↑φ ⟨W.boundaryFlag i, hcore⟩ = c

noncomputable def RS.EdgeSubset.throughSummand {α : Type} {W : Fragment α} [LinearOrder α] (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.RelTransitionSystem} (o : κ.Orientation) (c : ℕ) : ℂ

The corrected constrained summand: circuit sign, through factor, and the core colouring sum.

Equations

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