The h-generic normal form

The master-sum analogue where an arbitrary mixed functional h is evaluated at the colour-data extractors of the sorted blocks: the per-vertex factor carries a Nodup guard mirroring evalOdd.

This is the first stage of discharging the Eulerian-independence interface: the normal form is manifestly independent of the transition system and orientation.

The h-generic master summand

noncomputable def RS.hMaster {k ℓ : ℕ} (h : MixedFunctional k ℓ) (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) : ℂ

The h-generic master summand: mirrors masterSummand but replaces starCoord with the h-evaluation at the block's colour-data extractors, guarded by the Nodup condition.

Equations

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

Per-vertex value lemmas

theorem RS.hMaster_vertex_nodup {k ℓ : ℕ} (h : MixedFunctional k ℓ) (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) (hnd : (F.oddListAt o φ (blockVertex W v)).Nodup) : (if (oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v)).Nodup then ↑(sortSign (oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v))) * h (evenMultisetOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v)) (oddFinsetOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v)) else 0) = ↑(sortSign (oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v))) * (↑(sortSign (F.oddListAt o φ (blockVertex W v))) * h.evalOdd (F.evenColoursAt ψ (blockVertex W v)) (F.oddListAt o φ (blockVertex W v)))

The per-vertex value (duplicate-free case): the h-generic block factor equals the block sorting sign times the sign-normalised Definition 5 vertex factor.

theorem RS.hMaster_vertex_not_nodup {k ℓ : ℕ} (h : MixedFunctional k ℓ) (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) (hnd : ¬(F.oddListAt o φ (blockVertex W v)).Nodup) : (if (oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v)).Nodup then ↑(sortSign (oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v))) * h (evenMultisetOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v)) (oddFinsetOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v)) else 0) = 0

The per-vertex vanishing (repeated case): a repeated odd value kills the h-generic block factor.

The normal form

noncomputable def RS.defFiveNF {k ℓ : ℕ} (h : MixedFunctional k ℓ) (W : ClosedFragment) (F : EdgeSubset W) : ℂ

The h-generic normal form for the Definition 5 summand: the sum over even/odd colourings of the h-generic master summand at the data colouring.

Equations

• RS.defFiveNF h W F = ∑ ψ : F.EvenColouring k, ∑ φ : F.OddColouring ℓ, RS.hMaster h W (RS.colouringOf W F ψ φ)

theorem RS.defFiveNF_eq_flip {k ℓ : ℕ} (h : MixedFunctional k ℓ) (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : defFiveNF h W F = ∑ ψ : F.EvenColouring k, ∑ φ : F.OddColouring ℓ, hMaster h W (colouringOfFlip W F o ψ φ)

The flip-reindex step: the normal form equals the sum over the flipped data colouring at any orientation.