The super-symmetric form on one leg

The ambient space of the Gram construction is V_k ⊕ V_{2ℓ}, carrying the symmetric form xᵀy on the even summand, the skew-symmetric form xᵀJy on the odd summand with

J = [[0, I], [-I, 0]],

and zero across the two. This file is that form and nothing else, written from the definition rather than assembled out of the partition function's own weights, so that its relation to those weights is a theorem.

The relation is recorded at the end: on the even block the form is the partition function's state factor, and on the odd block it is that factor negated. The negation is the one already visible in the tower's colour kernel, which pairs the odd colours through -oddThroughFactor.

noncomputable def RS.symplecticJ (ℓ : ℕ) (c d : Fin (2 * ℓ)) : ℂ

The symplectic matrix J = [[0, I], [-I, 0]] in coordinates: J c d is 1 when d = c + ℓ, -1 when c = d + ℓ, and 0 otherwise.

Equations

• RS.symplecticJ ℓ c d = if ↑d = ↑c + ℓ then 1 else if ↑c = ↑d + ℓ then -1 else 0

noncomputable def RS.superLeg {k ℓ : ℕ} : Fin k ⊕ Fin (2 * ℓ) → Fin k ⊕ Fin (2 * ℓ) → ℂ

The super form on one leg: the identity on the even colours, J on the odd ones, zero across.

Equations

• RS.superLeg (Sum.inl a) (Sum.inl b) = if a = b then 1 else 0
• RS.superLeg (Sum.inr c) (Sum.inr d) = RS.symplecticJ ℓ c d
• RS.superLeg x✝¹ x✝ = 0

The relation to the partition function's state factor

The through-edge state factor of the mixed partition function is the super form on the even block and its negative on the odd one. Both are recorded as theorems; nothing below assumes them.

theorem RS.eq_oddPartner_iff {ℓ : ℕ} (c d : Fin (2 * ℓ)) : d = oddPartner ℓ c ↔ if ↑c < ℓ then ↑d = ↑c + ℓ else ↑d = ↑c - ℓ

Membership in the odd partner relation, in coordinates.

The dual basis at outgoing ends

RS21 writes the boundary vector at an odd leg as f_c where the arc is incoming and g_c where it is outgoing, and computes ⟨f_c, g_c⟩ = -1 and ⟨g_c, f_c⟩ = 1. In one basis, g_c is the symplectic dual of f_c: the partner colour carrying the partner sign. The two displayed values are recovered below, which is what fixes the convention.

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

The symplectic dual of a colour: the partner colour with the partner sign. This is RS21's g_c written in the basis of the f's.

Equations

• RS.dualSign ℓ c = ↑(RS.oddPartnerSign ℓ c)

theorem RS.dualSign_sq (ℓ : ℕ) (c : Fin (2 * ℓ)) : dualSign ℓ c * dualSign ℓ c = 1

The dual sign squares to one: it is ±1.

theorem RS.oddPartner_val (ℓ : ℕ) (c : Fin (2 * ℓ)) : ↑(oddPartner ℓ c) = if ↑c < ℓ then ↑c + ℓ else ↑c - ℓ

The partner colour in coordinates.

theorem RS.superLeg_f_g (ℓ : ℕ) (c : Fin (2 * ℓ)) : dualSign ℓ c * symplecticJ ℓ c (oddPartner ℓ c) = -1

⟨f_c, g_c⟩ = -1.

The through-edge factor is the dual basis at one end

A through-edge's two legs carry f_{φ(a)} and g_{φ(a)} — the same colour, dual bases. In one basis that says the two legs' colours are partners and the leg holding g contributes its partner sign. The mixed partition function's through-edge factor says exactly that, so it is the dual basis's contribution at those legs rather than an extra weight.

theorem RS.dualSign_oddPartner (ℓ : ℕ) (c : Fin (2 * ℓ)) : dualSign ℓ (oddPartner ℓ c) = -dualSign ℓ c

The dual sign flips at the partner colour.