A maximal stabilizer label space is self-dual

If $n=0$, then $V=L=L^{\perp }=\{0\}$ and $r=0$, so $\dim L^{\perp }=0=2n-r$, $r\le n$, and $L^{\perp }=L$. Hence the result holds.

Assume now $n\ge 1$. If $v=(x,z)\in V$ pairs to zero with every vector, pairing with $(e_j,0)$ and $(0,e_j)$ gives $z_j=x_j=0$ for every $j$. More generally, for any linear functional $\varphi$ on $V$, set $a_j=\varphi (e_j,0)$ and $b_j=\varphi (0,e_j)$. Then $v=(b,a)$ satisfies $\omega (v,(x^{\mathrm{\prime }},z^{\mathrm{\prime }}))=b\cdot z^{\mathrm{\prime }}+a\cdot x^{\mathrm{\prime }}=\varphi (x^{\mathrm{\prime }},z^{\mathrm{\prime }})$ by linearity. Thus $v\mapsto \omega (v,\cdot )$ is both injective and onto.

Put $r=\dim L$ and choose a basis ${\mathrm{\ell }}_1,\dots ,{\mathrm{\ell }}_r$ of $L$. Extend it to a basis of $V$ using [F3]. For any $y\in {\mathbb{F}}_2^r$, define a linear functional on this basis by $\varphi ({\mathrm{\ell }}_j)=y_j$ and by zero on the added basis vectors. Step 1.2 supplies $v\in V$ with $\omega (v,\cdot )=\varphi$, so $T:V\to {\mathbb{F}}_2^r$, $T(v)=(\omega (v,{\mathrm{\ell }}_j){)}_{j=1}^r$, is onto. Its kernel is $L^{\perp }$, and [F2] gives $\dim L^{\perp }=2n-r$. This includes $r=0$, where both the basis and ${\mathbb{F}}_2^r$ are empty or zero-dimensional.

For $n\ge 1$, isotropy gives $L\subseteq L^{\perp }$. Comparing dimensions with step 2.1 gives $r\le 2n-r$, hence $r\le n$. If $r=n$, both subspaces have dimension $n$, so [F3] gives $L=L^{\perp }$. This argument uses only finite basis extension and no choice principle.

Step 1.1 proves the result for $n=0$, and step 1.2 and step 2.1 and step 3.1 prove it for $n\ge 1$. These cases exhaust all dimensions in the Statement.