It is well known that the length $n$ of a binary Type II code is divisible by $8$. The classical proof relies on Gleason's theorem on weight enumerators. Motivated by a question of Vera Pless, we give elementary proofs of this fact that avoid invariant theory. Our main tool is a congruence modulo $8$ for the determinant of the integer Gram matrix $AA^{\mathsf T}$ of a binary orthogonal matrix $A$, obtained directly from the Leibniz expansion. It gives a short proof of a theorem of Janusz: the number of rows of weight congruent to $3 \pmod 4$ in a binary orthogonal matrix is divisible by $4$. From this single statement we derive both the length restriction for Type II codes and the theorem of Conway and Sloane that every vector in the shadow of a binary self-dual code of length $n$ has weight congruent to $n/2 \pmod 4$. We also give two short character-theoretic proofs of the length restriction and explain how all of these arguments detect the Arf invariant of a quadratic form.

翻译：暂无翻译