LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Dimension of the binary dual code

Statement

For every binary linear code $C \leq F_{2}^{n}$ with $n \geq 1$ , $\dim C^{⊥} = n - \dim C$ . This argument uses no form of the Axiom of Choice.

Facts & Assumptions

Given: A subspace $C \leq F_{2}^{n}$ , its bilinear dual, and the standard coordinate basis of $F_{2}^{n}$ .

[F1]

Bilinear dual of a finite-field linear code: $x \cdot y = \sum_{j < n} x_{j} y_{j}$ and $C^{⊥} = {y : x \cdot y = 0 for every x \in C}$ .

[F2]

The dual family of a finite basis is a basis of the dual space, with the same dimension: the dual family of a finite basis of a vector space is a basis of its algebraic dual, with the same dimension.

[F3]

If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ : a finite-dimensional subspace admits extension of each independent subset to a basis without choice.

[F4]

Rank-nullity: $\dim_{F} V = nullity T + rank T$ : for a linear map with finite-dimensional domain, domain dimension is the sum of kernel dimension and image dimension.

Proof

1.1F1F2construct

Let $e_{0}, \dots, e_{n - 1}$ be the standard basis of $F_{2}^{n}$ . Its coordinate dual basis is $e_{0}^{*}, \dots, e_{n - 1}^{*}$ , and $e_{i} \cdot y = y_{i} = e_{i}^{*} (y)$ for $0 \leq i < n$ by [F1]. Thus the linear map $J : F_{2}^{n} \to (F_{2}^{n})^{*}$ , $J (x) (y) = x \cdot y$ , sends a basis to the dual basis from [F2], so it is an isomorphism.

1.2givenF3construct

Choose a basis $c_{1}, \dots, c_{m}$ of $C$ and extend it to a basis of $F_{2}^{n}$ by [F3]. For every $f \in C^{*}$ , define $\tilde{f}$ on the extended basis by $\tilde{f} (c_{i}) = f (c_{i})$ and value $0$ on each added basis vector, then extend linearly. This is a linear functional on $F_{2}^{n}$ whose restriction to $C$ is $f$ . Hence restriction $(F_{2}^{n})^{*} \to C^{*}$ is onto.

2.1F1F2F4step 1.1step 1.2∎

The composite $T : F_{2}^{n} \overset{J}{\to} (F_{2}^{n})^{*} \to C^{*}$ is onto by the isomorphism in step 1.1 and surjectivity in step 1.2. Its kernel consists exactly of those $x$ for which $x \cdot c = 0$ for all $c \in C$ , namely $C^{⊥}$ by [F1]. Since $\dim C^{*} = \dim C = m$ by [F2], rank-nullity [F4] gives $n = \dim C^{⊥} + m$ . Therefore $\dim C^{⊥} = n - \dim C$ .

Depends on

Used by

Steane seven-qubit CSS code Example
CSS encoding dimension and commutation Theorem
CSS syndrome correction Theorem

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Richard Cleve, Quantum Information Processing course notes, §37.1.1 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 7: Quantum Error Correction (standard reference, not scraped)