RS21's colouring sum

RS21 writes the tensor's colouring sum as

Σ_{ψ ∼ χ₀, φ ∼ χ₁} ∏_{v ∈ V′(F)} h_v( … ),

where ψ colours the edges outside H and φ colours the edges of H — one colour per edge, both of them constrained at the labelled ends by χ. That is the sum named here.

The flag model's vertexSum instead colours the core edges only, leaving the through-edges to the through-edge product. The two agree exactly on the states whose two legs at a through-edge carry one colour, and off those RS21's sum is empty: a colouring gives the through-edge one colour and φ ∼ χ₁ pins it at both ends. So RS21's sum is the flag model's, cut down to the agreeing states — which is what the pairing of two tensors computes.

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

RS21's colouring sum over the colourings of the whole subset.

Equations

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

theorem RS.EdgeSubset.edgeSum_eq_vertexSum {α : Type} {W : Fragment α} (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.RelTransitionSystem} (o : κ.Orientation) (hag : F.ThroughAgree st hbnd) : F.edgeSum h st hbnd o = F.vertexSum h st hbnd o

On an agreeing state RS21's sum is the flag model's.

theorem RS.EdgeSubset.edgeSum_eq_zero_of_not_throughAgree {α : Type} {W : Fragment α} (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.RelTransitionSystem} (o : κ.Orientation) (hag : ¬F.ThroughAgree st hbnd) : F.edgeSum h st hbnd o = 0

A disagreeing state is coloured by nothing.