Documentation

LeanPool.RegtsSevenster.RS.Classical.Super.ColourFormMatch

The colour form entries are the standard form #

The single-position layer of the accompanying paper's Lemma 5.1(a): the pinned colour form entry agrees with the standard super form on the corresponding basis vectors — the orthonormal pairing on even colours, the symplectic pairing on odd colours.

theorem RS.colourFormEntry_even (k ℓ : ℕ) (i j : Fin k) :
colourFormEntry k ℓ (Sum.inl i) (Sum.inl j) = stdFormEven k (stdE k i) (stdE k j)

On even colours the entry is the orthonormal pairing.

theorem RS.colourFormEntry_odd (k ℓ : ℕ) (a b : Fin (2 * ℓ)) :
colourFormEntry k ℓ (Sum.inr a) (Sum.inr b) = stdFormOdd ℓ (stdF ℓ a) (stdF ℓ b)

On odd colours it is the symplectic one.