[proofplan] We exhibit a linear surjection $\gamma: \mathbb{F}_2^n \to \mathbb{F}_2^k$ whose kernel is $C^\perp$, and then apply the rank-nullity theorem. To make the kernel transparent, we first reduce to the case where $C$ has a generator matrix in standard form $G = (I_k \mid B)$ by invoking the [Standard Form of Generator Matrix](/theorems/1661) theorem. Permuting coordinates replaces $C$ by an equivalent code whose dual dimension is unchanged, so this reduction is harmless. The map $\gamma(x) = Gx$ (matrix-vector product with $x$ a column) is surjective because $G$ contains $I_k$ as a block, and has kernel $C^\perp$ because its rows span $C$. Rank-nullity then gives $n = \dim(C^\perp) + k$. [/proofplan] [step:Reduce to the case where $C$ has a generator matrix in standard form] Let $k := \dim_{\mathbb{F}_2}(C)$. By the [Standard Form of Generator Matrix](/theorems/1661) theorem, there is a code $C^*$ equivalent to $C$ — in the sense that $C^*$ is obtained from $C$ by a permutation of coordinates — admitting a generator matrix of the form \begin{align*} G = (I_k \mid B) \in \mathbb{F}_2^{k \times n}, \qquad B \in \mathbb{F}_2^{k \times (n-k)}. \end{align*} We claim $\dim(C) = \dim(C^*)$ and $\dim(C^\perp) = \dim((C^*)^\perp)$. Let $\pi \in S_n$ be the coordinate permutation taking $C$ to $C^*$, and define \begin{align*} P_\pi: \mathbb{F}_2^n &\to \mathbb{F}_2^n \\ (x_1, \ldots, x_n) &\mapsto (x_{\pi^{-1}(1)}, \ldots, x_{\pi^{-1}(n)}). \end{align*} Then $P_\pi$ is a linear isomorphism of $\mathbb{F}_2^n$ with $C^* = P_\pi(C)$. The standard bilinear form is invariant under simultaneous permutation: $P_\pi(x) \cdot P_\pi(y) = \sum_i x_{\pi^{-1}(i)} y_{\pi^{-1}(i)} = \sum_j x_j y_j = x \cdot y$. Hence \begin{align*} (C^*)^\perp = \{x \in \mathbb{F}_2^n : x \cdot P_\pi(c) = 0 \ \forall c \in C\} = P_\pi\big(\{y : P_\pi(y) \cdot P_\pi(c) = 0 \ \forall c\}\big) = P_\pi(C^\perp). \end{align*} Since $P_\pi$ is an isomorphism, $\dim(C^*) = \dim(C) = k$ and $\dim((C^*)^\perp) = \dim(C^\perp)$. Thus proving the formula for $C^*$ proves it for $C$, and we may assume from now on that $C$ itself has generator matrix $G = (I_k \mid B)$. [guided] The dimension formula is a statement about the algebraic structure of $C$ — its dimension and the dimension of its orthogonal complement under the standard bilinear form. Coordinate permutation preserves this structure because it is a linear isomorphism that leaves the bilinear form invariant. Concretely, $P_\pi$ acts diagonally on the standard basis, so it takes orthonormal coordinates to orthonormal coordinates, and orthogonal complements are sent to orthogonal complements. This lets us assume generator matrix in the cleanest possible form without loss of generality. Without this reduction, we would have to argue with an arbitrary generator matrix, which obscures why $\gamma$ below is surjective. [/guided] [/step] [step:Define the evaluation map $\gamma$ and verify linearity] With $G = (I_k \mid B) \in \mathbb{F}_2^{k \times n}$, define the linear map \begin{align*} \gamma: \mathbb{F}_2^n &\to \mathbb{F}_2^k \\ x &\mapsto G x, \end{align*} where $x \in \mathbb{F}_2^n$ is interpreted as a column vector and $Gx$ is the matrix-vector product. Linearity is immediate from the linearity of matrix multiplication: $\gamma(x + y) = G(x + y) = Gx + Gy = \gamma(x) + \gamma(y)$, and similarly for scalar multiples (the scalars here being in $\mathbb{F}_2$). [/step] [step:Show that $\gamma$ is surjective] The matrix $G = (I_k \mid B)$ has $I_k$ as its first $k$ columns. For any $v = (v_1, \ldots, v_k)^\top \in \mathbb{F}_2^k$, the vector $x = (v_1, \ldots, v_k, 0, \ldots, 0)^\top \in \mathbb{F}_2^n$ satisfies \begin{align*} \gamma(x) = G x = I_k \, v + B \cdot 0 = v. \end{align*} Hence $\gamma$ is surjective, so $\dim(\operatorname{Im} \gamma) = k$. [/step] [step:Show that $\ker(\gamma) = C^\perp$] Writing the rows of $G$ as $g_1, \ldots, g_k \in \mathbb{F}_2^n$, the $i$-th component of $Gx$ is $g_i \cdot x$ (with the dot product denoting the standard bilinear form). Therefore \begin{align*} x \in \ker(\gamma) \iff G x = 0 \iff g_i \cdot x = 0 \text{ for each } i \in \{1, \ldots, k\}. \end{align*} We claim this is equivalent to $x \cdot c = 0$ for all $c \in C$. Indeed, the rows $g_1, \ldots, g_k$ span $C$ (by definition of generator matrix), and because $G$ contains $I_k$ as a submatrix, these $k$ rows are linearly independent, hence form a basis of $C$. Let $c \in C$; write $c = \sum_i \lambda_i g_i$ with $\lambda_i \in \mathbb{F}_2$. Then \begin{align*} x \cdot c = x \cdot \sum_i \lambda_i g_i = \sum_i \lambda_i (x \cdot g_i). \end{align*} If $x \cdot g_i = 0$ for all $i$, then $x \cdot c = 0$ for all $c \in C$, i.e.\ $x \in C^\perp$. Conversely, if $x \in C^\perp$, then $x \cdot g_i = 0$ for each basis vector $g_i$, hence $Gx = 0$. Therefore \begin{align*} \ker(\gamma) = C^\perp. \end{align*} [guided] The kernel computation rests on two observations. First, the bilinear form $(x, g) \mapsto x \cdot g$ is linear in $g$, so vanishing on a spanning set implies vanishing on the whole subspace: checking orthogonality against a basis is the same as checking orthogonality against every element. Second, the rows of $G$ form a basis of $C$ — this is why standard form matters. A generator matrix whose rows are merely spanning but not linearly independent would still give $\ker(Gx) = C^\perp$, but then $\gamma$ would not be surjective onto $\mathbb{F}_2^k$; we would have to quotient by the redundancy, leading to a messier dimension count. The $(I_k \mid B)$ form guarantees the rows are a basis (the presence of $I_k$ forces linear independence) and also guarantees surjectivity. [/guided] [/step] [step:Apply the rank-nullity theorem and conclude] The [Rank-Nullity Theorem](/theorems/???) applied to the linear map $\gamma: \mathbb{F}_2^n \to \mathbb{F}_2^k$ gives \begin{align*} n = \dim_{\mathbb{F}_2}(\mathbb{F}_2^n) = \dim_{\mathbb{F}_2}(\ker \gamma) + \dim_{\mathbb{F}_2}(\operatorname{Im} \gamma). \end{align*} By Step 3, $\dim(\operatorname{Im} \gamma) = k = \dim(C)$. By Step 4, $\dim(\ker \gamma) = \dim(C^\perp)$. Substituting, \begin{align*} n = \dim(C^\perp) + \dim(C), \end{align*} as required. [/step]