The Regts–Sevenster functional

The coordinates of the star vectors in the colouring model, and the mixed functional at the canonical colouring. The accompanying paper calls this witness h^ξ (§5.4). Its mate-based functional satisfies h^RS = h^ξ ∘ Sym_s(Ψ), where Ψ fixes the even basis and sends ξ_i to η_i. Lemma 5.6 gives the coordinate dictionary; Lemma 5.7 proves the change of basis and the invariance of the partition function under the isometry Ψ.

noncomputable def RS.starCoord {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (d : ℕ) (c : MixedColouring k ℓ d) : ℂ

The star coordinate: the vertex star vector transported to the colouring model, read at a colouring; zero on odd-parity colourings.

Equations

• RS.starCoord f P e' d c = if hc : c.IsEven then (RS.colourPowerEquiv k ℓ d).evenEquiv ((RS.stdFromOmega f P e' d).evenMap (RS.starVec f P d)) ⟨c, hc⟩ else 0

theorem RS.starCoord_odd {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (d : ℕ) (c : MixedColouring k ℓ d) (hc : ¬c.IsEven) : starCoord f P e' d c = 0

Star coordinates vanish on odd-parity colourings.

noncomputable def RS.hRS {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) : MixedFunctional k ℓ

The Regts–Sevenster functional: the star coordinate at the canonical colouring, the paper's witness h^ξ (§5.4).

Equations

• RS.hRS f P e' μm F = RS.starCoord f P e' (μm.card + F.card) (RS.canonColouring μm F)

theorem RS.evalOdd_hRS_nodup {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (μm : Multiset (Fin k)) (w : List (Fin (2 * ℓ))) (hw : w.Nodup) : (hRS f P e').evalOdd μm w = ↑(sortSign w) * starCoord f P e' (μm.card + w.toFinset.card) (canonColouring μm w.toFinset)

The alternating evaluation on a duplicate-free list is the sorting sign times the star coordinate at the canonical colouring.