Universality after exact coordinate serialization

Serializing the whole coordinate vector and embedding the resulting word in a sufficiently wide binary field preserves distinctness. Multiplication and truncation in that field therefore give a universal hash on coordinate vectors. No injectivity of the actual condenser is used.

theorem Algebraic.Cutwidth.Extractor.Internal.serializedBinaryHash_universal {s t m ell : ℕ} [Fintype (AdjoinRoot (binaryModulus t))] (capacity : m * (2 * 3 ^ s) ≤ 2 * 3 ^ t) (width : ell ≤ 2 * 3 ^ t) : UniversalHashFamily fun (coords : Fin m → AdjoinRoot (binaryModulus s)) => binaryFieldHash t ell (BinaryFieldCodec.decode t (encodeCondenserOutput s m coords))