35 Thm 10: Gilbert–Varshamov Plus

Lemma 422 GV Threshold Positivity

✓

Let $\delta \in \mathbb {R}$ with $0 {\lt} \delta {\lt} 11/100$. Then

\[ 0 {\lt} \frac{2}{1/2 - h(\delta )}, \]

where $h(\delta )$ denotes the binary entropy function.

Proof ▶

We first obtain $h(\delta ) {\lt} 1/2$ by applying $\texttt{binaryEntropy\_ lt\_ half}$ to the hypotheses $0 {\lt} \delta $ and $\delta {\lt} 11/100$. The result then follows by positivity of the numerator $2 {\gt} 0$ (by numerical computation) and positivity of the denominator $1/2 - h(\delta ) {\gt} 0$ (by linear arithmetic from $h(\delta ) {\lt} 1/2$).

Lemma 423 GV Lower Bound on $n$

✓

Let $\delta \in \mathbb {R}$ with $0 {\lt} \delta {\lt} 11/100$, and let $n \in \mathbb {N}$. If

\[ n {\gt} \frac{2}{1/2 - h(\delta )}, \]

then $(1/2 - h(\delta )) \cdot n {\gt} 2$.

Proof ▶

From $\texttt{binaryEntropy\_ lt\_ half}$ applied to $0 {\lt} \delta $ and $\delta {\lt} 11/100$, we have $h(\delta ) {\lt} 1/2$, so the gap $0 {\lt} 1/2 - h(\delta )$ holds by linear arithmetic. Rewriting the hypothesis $n {\gt} 2/(1/2 - h(\delta ))$ via $\texttt{div\_ lt\_ iff}$ using this positivity, we obtain $2 {\lt} (1/2 - h(\delta )) \cdot n$, and the conclusion follows by linear arithmetic.

Lemma 424 Existence of $k$ in GV Range

✓

Let $\delta \in \mathbb {R}$ with $0 {\lt} \delta {\lt} 11/100$, and let $n \in \mathbb {N}$ with $n {\gt} 2/(1/2 - h(\delta ))$. Then there exists $k \in \mathbb {N}$ such that:

\[ \frac{n}{2} {\lt} k, \quad k + 1 {\lt} (1 - h(\delta ))\cdot n, \quad k {\lt} n. \]

Proof ▶

We set $k = \lfloor n/2 \rfloor + 1$. From $\texttt{binaryEntropy\_ lt\_ half}$ we have $h(\delta ) {\lt} 1/2$, and by Lemma 423 we have $(1/2 - h(\delta )) \cdot n {\gt} 2$, which gives $n/2 + 1 {\lt} (1 - h(\delta ))\cdot n - 1$, hence $n/2 + 1 + 1 {\lt} (1 - h(\delta )) \cdot n$.

We verify each condition for $k = \lfloor n/2 \rfloor + 1$:

Lower bound: Using $\lfloor n/2 \rfloor \leq n/2$ (from $\texttt{Nat.cast\_ div\_ le}$) and $n {\lt} 2(\lfloor n/2 \rfloor + 1)$ (by integer arithmetic), pushing casts and applying linear arithmetic yields $n/2 {\lt} k$.

Upper bound: By the same cast inequalities and the gap $n/2 + 1 {\lt} (1-h(\delta )) \cdot n - 1$, linear arithmetic gives $k + 1 {\lt} (1 - h(\delta )) \cdot n$.

Strict bound $k {\lt} n$: We argue by contradiction. If $n \leq k$, then integer arithmetic gives $n \leq 2$. One then shows $h(\delta ) {\gt} 0$ (by expanding the definition: since $0 {\lt} \delta {\lt} 1/2$, both $\log _2 \delta {\lt} 0$ and $\log _2(1-\delta ) {\lt} 0$, so $h(\delta ) = -\delta \log _2 \delta - (1-\delta )\log _2(1-\delta ) {\gt} 0$ via nonlinear arithmetic). With $n \leq 2$, we get $(1/2 - h(\delta )) \cdot n \leq 1$, contradicting $(1/2 - h(\delta )) \cdot n {\gt} 2$.

Definition 425 Evaluation Linear Map

✓

For $n, r \in \mathbb {N}$ and a vector $v \in \mathbb {F}_2^n$, the evaluation map at $v$ is the linear map

\[ \operatorname {eval}_v : \operatorname {Hom}_{\mathbb {F}_2}(\mathbb {F}_2^n, \mathbb {F}_2^r) \to \mathbb {F}_2^r, \quad \phi \mapsto \phi (v). \]

This is given by $\texttt{LinearMap.apply$_l$}\; v$.

Lemma 426 Evaluation Map Application

✓

For $v \in \mathbb {F}_2^n$ and $\phi \in \operatorname {Hom}_{\mathbb {F}_2}(\mathbb {F}_2^n, \mathbb {F}_2^r)$, we have $\operatorname {eval}_v(\phi ) = \phi (v)$.

Proof ▶

This follows immediately by unfolding the definition of $\operatorname {eval}_v$ as $\texttt{LinearMap.apply$_l$}\; v$ and simplifying.

Lemma 427 Surjectivity of Evaluation Map

✓

For $v \in \mathbb {F}_2^n$ with $v \neq 0$, the evaluation map $\operatorname {eval}_v$ is surjective.

Proof ▶

Let $w \in \mathbb {F}_2^r$ be arbitrary. Since $v \neq 0$, there exists an index $j$ with $v_j \neq 0$. By case analysis on $\mathbb {F}_2$ (using $\texttt{decide}$), every element of $\mathbb {F}_2$ is $0$ or $1$, so $v_j = 1$.

We construct $\phi = (\texttt{LinearMap.proj}\; j) \cdot _r w$, i.e. the linear map sending $e_j \mapsto w$ and all other standard basis vectors to $0$. Then $\phi (v) = v_j \cdot w = 1 \cdot w = w$, so $\operatorname {eval}_v(\phi ) = w$.

Lemma 428 Kernel Rank of Evaluation Map

✓

For $v \in \mathbb {F}_2^n$ with $v \neq 0$,

\[ \operatorname {finrank}_{\mathbb {F}_2}(\ker \operatorname {eval}_v) = nr - r. \]

Proof ▶

By Lemma 427, $\operatorname {eval}_v$ is surjective. Applying the rank–nullity theorem ($\texttt{LinearMap.finrank\_ range\_ add\_ finrank\_ ker}$), we have

\[ \operatorname {finrank}(\operatorname {range}(\operatorname {eval}_v)) + \operatorname {finrank}(\ker \operatorname {eval}_v) = \operatorname {finrank}(\operatorname {Hom}(\mathbb {F}_2^n, \mathbb {F}_2^r)). \]

Since $\operatorname {eval}_v$ is surjective, $\operatorname {range}(\operatorname {eval}_v) = \mathbb {F}_2^r$ so its rank is $r$. By the formula for the finrank of a Hom space ($\texttt{Module.finrank\_ linearMap}$) the total dimension is $nr$. Hence $\operatorname {finrank}(\ker \operatorname {eval}_v) = nr - r$, which follows by integer arithmetic.

Lemma 429 Cardinality of Kernel of Evaluation Map

✓

For $v \in \mathbb {F}_2^n$ with $v \neq 0$,

\[ |\ker \operatorname {eval}_v| \cdot 2^r = |\operatorname {Hom}_{\mathbb {F}_2}(\mathbb {F}_2^n, \mathbb {F}_2^r)|. \]

Proof ▶

We apply $\texttt{Module.card\_ eq\_ pow\_ finrank}$ to both sides. For the kernel, its cardinality is $2^{nr - r}$ by Lemma 428. For the Hom space, its cardinality is $2^{nr}$. Thus the left side is $2^{nr - r} \cdot 2^r = 2^{nr}$. We verify that $r \leq nr$ (since $n {\gt} 0$, which follows from $v \neq 0$ implying $n$ is a singleton or larger), and conclude by integer arithmetic that $nr - r + r = nr$.

Theorem 430 Axiom: Existence of Good Linear Map

✓

red[UNPROVEN AXIOM]

Let $n, r \in \mathbb {N}$ with $0 {\lt} r \leq n$, and let $t \in \mathbb {R}$. Suppose

\[ \bigl|\operatorname {Ball}(n, t-1)\bigr| {\lt} 2^r. \]

Then there exists a linear map $\phi : \mathbb {F}_2^n \to \mathbb {F}_2^r$ such that for every nonzero $v \in \mathbb {F}_2^n$ with $\operatorname {wt}(v) {\lt} t$, we have $\phi (v) \neq 0$.

Note: This is stated as an axiom because the full probabilistic counting argument was not completed in the formalization. The argument follows the probabilistic method: a uniformly random linear map avoids each bad vector $v$ with probability $1 - 2^{-r}$, and a union bound over the $|\operatorname {Ball}(n,t-1)|$ bad vectors yields existence of a good map when the ball is smaller than $2^r$.

Theorem 431 Axiom: Existence of Good Surjective Map with Both Distance Bounds

✓

red[UNPROVEN AXIOM]

Let $n, r \in \mathbb {N}$ with $0 {\lt} r \leq n$, and let $t \in \mathbb {R}$. Suppose

\[ \bigl|\operatorname {Ball}(n, t-1)\bigr| {\lt} 2^r \quad \text{and} \quad \bigl|\operatorname {Ball}(n, t-1)\bigr| {\lt} 2^{n-r}. \]

Then there exists a surjective linear map $\phi : \mathbb {F}_2^n \to \mathbb {F}_2^r$ such that:

For every nonzero $v \in \mathbb {F}_2^n$ with $\operatorname {wt}(v) {\lt} t$, we have $\phi (v) \neq 0$.
For every $w \in (\ker \phi )^\perp $ with $w \neq 0$, we have $\operatorname {wt}(w) \geq t$.

Note: This extends exists_good_map by simultaneously bounding both the distance and the dual-distance conditions via a union bound: the probability of a bad distance event plus the probability of a bad dual-distance event is less than $1$, and any map satisfying the dual condition is automatically surjective (otherwise some nonzero $y$ has $\phi ^\top (y) = 0$, which has weight $0 {\lt} t$).

Lemma 432 Distance Lower Bound from Weight Condition

✓

Let $\mathcal{C}$ be a classical code of length $n$, let $t \in \mathbb {R}$. Suppose every nonzero codeword $v \in \mathcal{C}$ satisfies $\operatorname {wt}(v) \geq t$, and suppose $\mathcal{C}$ contains at least one nonzero element. Then $d(\mathcal{C}) \geq t$.

Proof ▶

Unfolding the definition of distance, let $S = \{ w \in \mathbb {N} \mid \exists \, x \in \mathcal{C},\; x \neq 0,\; \operatorname {wt}(x) = w\} $. From the hypothesis there exists a nonzero codeword, so $S$ is nonempty.

For each $w' \in S$, write $w' = \operatorname {wt}(x')$ for some nonzero $x' \in \mathcal{C}$. By the weight hypothesis, $\operatorname {wt}(x') \geq t$, hence $\lceil t \rceil \leq w'$.

Applying $\texttt{le\_ csInf}$ to the nonemptiness and this lower bound, we get $\inf S \geq \lceil t \rceil $. Casting to reals:

\[ d(\mathcal{C}) = \inf S \geq \lceil t \rceil \geq t, \]

where the last inequality is $\texttt{Nat.le\_ ceil}$.

Lemma 433 Existence of Submodule of Prescribed Dimension

✓

Let $W$ be a submodule of $\mathbb {F}_2^n$, and let $k \leq \operatorname {finrank}_{\mathbb {F}_2}(W)$. Then there exists a submodule $W' \leq W$ with $\operatorname {finrank}_{\mathbb {F}_2}(W') = k$.

Proof ▶

Since $k \leq \operatorname {finrank}(W) = |\text{ChooseBasisIndex}(W)|$ (by $\texttt{Module.finrank\_ eq\_ card\_ chooseBasisIndex}$), we apply $\texttt{Finset.exists\_ subset\_ card\_ eq}$ to obtain a subset $s$ of the basis index set of cardinality $k$.

Let $B$ be the chosen basis of $W$ and define $W'_\text {sub} = \operatorname {span}_{\mathbb {F}_2}\{ B(i) \mid i \in s\} $ as a submodule of $W$. Let $W' = W'_\text {sub}$ mapped along the inclusion $W \hookrightarrow \mathbb {F}_2^n$.

We verify $W' \leq W$ by tracing elements through the map. For the dimension: since $B$ is a basis, the restriction to $s$ gives a linearly independent family (by $\texttt{LinearIndependent.comp}$ with the injective coercion). Thus $\operatorname {finrank}(W'_\text {sub}) = |s| = k$ by $\texttt{finrank\_ span\_ eq\_ card}$. Finally, $\texttt{Submodule.finrank\_ map\_ subtype\_ eq}$ gives $\operatorname {finrank}(W') = \operatorname {finrank}(W'_\text {sub}) = k$.

Lemma 434 Existence of Code with Good Distance

✓

Let $\delta \in \mathbb {R}$ with $0 {\lt} \delta \leq 1/2$, and $n, k \in \mathbb {N}$ with $0 {\lt} n$, $0 {\lt} k$, $k {\lt} n$, and

\[ k + 1 {\lt} (1 - h(\delta )) \cdot n. \]

Then there exists a classical code $\mathcal{C}$ of length $n$ with $\dim (\mathcal{C}) = k$ and $d(\mathcal{C}) \geq \delta n$.

Proof ▶

Set $r = n - k$. Then $0 {\lt} r$ and $r \leq n$. From the hypothesis $k + 1 {\lt} (1-h(\delta ))n$, we get $h(\delta ) \cdot n {\lt} n - k = r$.

Hamming ball bound: We show $|\operatorname {Ball}(n, \delta n - 1)| {\lt} 2^r$.

Case $\delta n {\lt} 1$: Then $\delta n - 1 {\lt} 0$, so $\operatorname {Ball}(n, \delta n - 1) = \emptyset $ by Lemma 271, and the bound is trivial.

Case $\delta n \geq 1$: Set $d' = \lfloor \delta n \rfloor - 1$. We verify $d' + 1 \leq \delta n$ using $\lfloor \delta n \rfloor \geq 1$ and the floor inequality. We also show $\operatorname {Ball}(n, \delta n - 1) \subseteq \operatorname {Ball}(n, d')$ by Theorem 270: for any $v$ with $\operatorname {wt}(v) {\lt} \delta n - 1 {\lt} \lfloor \delta n \rfloor $, we have $\operatorname {wt}(v) \leq \lfloor \delta n \rfloor - 1 = d'$ by integer arithmetic. Then:

\[ |\operatorname {Ball}(n, \delta n - 1)| \leq |\operatorname {Ball}(n, d')| \leq 2^{h(\delta ) \cdot n} {\lt} 2^r, \]

where the middle inequality uses Theorem 276 with $d' + 1 \leq \delta n$, and the last uses $h(\delta ) \cdot n {\lt} r$.

Obtaining the map: By Theorem 430, there exists $\phi : \mathbb {F}_2^n \to \mathbb {F}_2^r$ such that every nonzero $v$ with $\operatorname {wt}(v) {\lt} \delta n$ satisfies $\phi (v) \neq 0$.

Dimension of kernel: By rank–nullity, $\operatorname {finrank}(\operatorname {range}(\phi )) + \operatorname {finrank}(\ker \phi ) = n$. Since $\operatorname {finrank}(\operatorname {range}(\phi )) \leq r$, we get $\operatorname {finrank}(\ker \phi ) \geq n - r = k$.

Subcode: By Lemma 433, there exists $W \leq \ker \phi $ with $\operatorname {finrank}(W) = k$. The associated code $\mathcal{C} = \langle W \rangle $ has $\dim (\mathcal{C}) = k$.

Good distance: For any nonzero $v \in W$, we have $v \in \ker \phi $, so $\phi (v) = 0$. If $\operatorname {wt}(v) {\lt} \delta n$, then the property of $\phi $ would require $\phi (v) \neq 0$, a contradiction. Hence $\operatorname {wt}(v) \geq \delta n$.

Nonemptiness: Since $\operatorname {finrank}(W) = k \geq 1$, $W$ is nontrivial (as $k {\gt} 0$), so it contains a nonzero element.

By Lemma 432, $d(\mathcal{C}) \geq \delta n$.

Lemma 435 Satisfiability of Good Distance Premises

✓

There exist $\delta \in \mathbb {R}$ and $n, k \in \mathbb {N}$ satisfying all premises of Lemma 434: $0 {\lt} \delta $, $\delta \leq 1/2$, $0 {\lt} n$, $0 {\lt} k$, $k {\lt} n$, and $k + 1 {\lt} (1 - h(\delta )) \cdot n$.

Proof ▶

We exhibit the witness $\delta = 1/100$, $n = 1000$, $k = 498$. The numerical conditions $0 {\lt} 1/100$, $1/100 \leq 1/2$, $0 {\lt} 1000$, $0 {\lt} 498$, $498 {\lt} 1000$ are verified by numerical computation ($\texttt{norm\_ num}$). For the bound $499 {\lt} (1 - h(1/100)) \cdot 1000$: we first obtain $h(1/100) {\lt} 1/2$ from $\texttt{binaryEntropy\_ lt\_ half}$, then apply nonlinear arithmetic ($\texttt{nlinarith}$) after pushing casts.

Lemma 436 Double Dual Code Identity

✓

For any classical code $\mathcal{C}$ of length $n$,

\[ ((\mathcal{C}^\perp )^\perp ) = \mathcal{C}. \]

Proof ▶

We work over the finite-dimensional space $\mathbb {F}_2^n$. By extensionality, it suffices to show that for every $w \in \mathbb {F}_2^n$, $w \in ((\mathcal{C}^\perp )^\perp )$ if and only if $w \in \mathcal{C}$.

($\Leftarrow $): Suppose $w \in \mathcal{C}$. By Theorem 256, we must show that for every $c \in \mathcal{C}^\perp $, $c \cdot w = 0$. But by definition of the dual code (Theorem 256 applied to $c$), we have $c \cdot w = 0$ for all $w \in \mathcal{C}$; since $w \in \mathcal{C}$ and dot product is commutative, $c \cdot w = w \cdot c = 0$.

($\Rightarrow $): Suppose $w \in ((\mathcal{C}^\perp )^\perp )$, i.e. for all $c \in \mathcal{C}^\perp $, $c \cdot w = 0$. We assume for contradiction $w \notin \mathcal{C}$. By $\texttt{Submodule.exists\_ dual\_ map\_ eq\_ bot\_ of\_ notMem}$ (applied to the finite-dimensional setting), there exists a linear functional $f : \mathbb {F}_2^n \to \mathbb {F}_2$ with $f(w) \neq 0$ and $f|_{\mathcal{C}} = 0$. Via the dot-product equivalence $e : \operatorname {Hom}(\mathbb {F}_2^n, \mathbb {F}_2) \cong \mathbb {F}_2^n$, let $c = e^{-1}(f)$.

Since $f|_{\mathcal{C}} = 0$, we have $f(v) = c \cdot v = 0$ for all $v \in \mathcal{C}$, so $c \in \mathcal{C}^\perp $ by Theorem 256. But then the assumption $w \in ((\mathcal{C}^\perp )^\perp )$ gives $c \cdot w = 0$, which under $e$ reads $f(w) = 0$, contradicting $f(w) \neq 0$.

Lemma 437 Distance of Double Dual

✓

For any classical code $\mathcal{C}$ of length $n$,

\[ d((\mathcal{C}^\perp )^\perp ) = d(\mathcal{C}). \]

Proof ▶

Unfolding the definition of distance, both sides are $\inf \{ w \in \mathbb {N} \mid \exists \, x, x \in \mathcal{C} \text{ (or } ((\mathcal{C}^\perp )^\perp )\text{)},\; x \neq 0,\; \operatorname {wt}(x) = w\} $. By Lemma 436, $((\mathcal{C}^\perp )^\perp ) = \mathcal{C}$, so the index sets are equal. The result follows by congruence.

Lemma 438 Existence of Code with Good Dual Distance

✓

Let $\delta \in \mathbb {R}$ with $0 {\lt} \delta \leq 1/2$, and $n, k \in \mathbb {N}$ with $0 {\lt} n$, $0 {\lt} k$, $k {\lt} n$, and

\[ n - k + 1 {\lt} (1 - h(\delta )) \cdot n. \]

Then there exists a classical code $\mathcal{C}$ of length $n$ with $\dim (\mathcal{C}) = k$ and $d(\mathcal{C}^\perp ) \geq \delta n$.

Proof ▶

Let $r = n - k$. Then $0 {\lt} r$ and $r {\lt} n$. We convert the hypothesis: $(n-k) + 1 = (r : \mathbb {R}) + 1 {\lt} (1-h(\delta ))n$. By Lemma 434 applied to $\delta $, $n$, $r$ (with $r$ in place of $k$), there exists a code $D$ of length $n$ with $\dim (D) = r$ and $d(D) \geq \delta n$.

Set $\mathcal{C} = D^\perp $. By Theorem 259,

\[ \dim (\mathcal{C}) = \dim (D^\perp ) = n - \dim (D) = n - r = k. \]

For the dual distance:

\[ d(\mathcal{C}^\perp ) = d((D^\perp )^\perp ) = d(D) \geq \delta n, \]

where we apply Lemma 437.

Lemma 439 Satisfiability of Good Dual Distance Premises

✓

There exist $\delta \in \mathbb {R}$ and $n, k \in \mathbb {N}$ satisfying all premises of Lemma 438: $0 {\lt} \delta $, $\delta \leq 1/2$, $0 {\lt} n$, $0 {\lt} k$, $k {\lt} n$, and $n - k + 1 {\lt} (1-h(\delta )) \cdot n$.

Proof ▶

We exhibit the witness $\delta = 1/100$, $n = 1000$, $k = 502$. All numerical conditions are verified by $\texttt{norm\_ num}$. The bound $499 {\lt} (1-h(1/100)) \cdot 1000$ follows from $h(1/100) {\lt} 1/2$ (via $\texttt{binaryEntropy\_ lt\_ half}$) and $\texttt{nlinarith}$.

Lemma 440 Key Natural Number Inequality

✓

$100^{100} {\lt} 2^{10} \cdot 99^{99}$.

Proof ▶

This is verified by computation ($\texttt{native\_ decide}$).

Lemma 441 Key Fractional Inequality

✓

$100 \cdot \left(\dfrac {100}{99}\right)^{99} {\lt} 2^{10}$.

Proof ▶

We rewrite: $100 \cdot (100/99)^{99} = 100^{100}/99^{99}$, so the inequality is equivalent (after clearing the denominator $99^{99} {\gt} 0$) to $100^{100} {\lt} 2^{10} \cdot 99^{99}$. We cast to naturals: $100^{100} = \uparrow (100^{100} : \mathbb {N}) {\lt} \uparrow (2^{10} \cdot 99^{99})$, which holds by Lemma 440.

Lemma 442 Binary Entropy at $1/100$ is Less Than $1/10$

✓

$h(1/100) {\lt} 1/10$.

Proof ▶

We expand $h(1/100) = -(1/100)\log _2(1/100) - (99/100)\log _2(99/100)$. We compute:

\[ \log _2(1/100) = -\log _2(100), \qquad \log _2(99/100) = -\log _2(100/99), \]

so $h(1/100) = (1/100)\log _2(100) + (99/100)\log _2(100/99)$.

To prove this is less than $1/10$, it suffices to show:

\[ \log _2(100) + 99 \cdot \log _2(100/99) {\lt} 10. \]

We bound the left side: by the logarithm identity,

\[ \log _2\! \bigl(100 \cdot (100/99)^{99}\bigr) = \log _2(100) + 99\log _2(100/99). \]

Since $100 \cdot (100/99)^{99} {\lt} 2^{10}$ by Lemma 441, and $\log _2$ is strictly increasing ($\texttt{Real.logb\_ lt\_ logb}$), we get $\log _2(100 \cdot (100/99)^{99}) {\lt} \log _2(2^{10}) = 10$. The conclusion follows by linear arithmetic, using positivity of $\log _2(100) {\gt} 0$ and $\log _2(100/99) {\gt} 0$.

Lemma 443 Binary Entropy at $1/100$ Tight Bound

✓

$h(1/100) {\lt} 499/1000$.

Proof ▶

This follows immediately from Lemma 442: $h(1/100) {\lt} 1/10 = 100/1000 {\lt} 499/1000$.

Lemma 444 Hamming Ball Bound Below Power of Two

✓

Let $\delta \in \mathbb {R}$ with $0 {\lt} \delta \leq 1/2$, $n \in \mathbb {N}$ with $0 {\lt} n$, and $m \in \mathbb {N}$ with $h(\delta ) \cdot n {\lt} m$. Then

\[ \bigl|\operatorname {Ball}(n, \delta n - 1)\bigr| {\lt} 2^m. \]

Proof ▶

Case $\delta n {\lt} 1$: Then $\delta n - 1 {\lt} 0$, so $\operatorname {Ball}(n, \delta n - 1) = \emptyset $ by Lemma 271, and $0 {\lt} 2^m$.

Case $\delta n \geq 1$: Set $d' = \lfloor \delta n \rfloor - 1$. We verify $d' + 1 \leq \delta n$ using $\lfloor \delta n \rfloor \geq 1$ and the floor estimate. We show $\operatorname {Ball}(n, \delta n - 1) \subseteq \operatorname {Ball}(n, d')$ using Theorem 270: for $v \in \operatorname {Ball}(n, \delta n - 1)$ we have $\operatorname {wt}(v) {\lt} \delta n - 1 {\lt} \lfloor \delta n \rfloor $, so $\operatorname {wt}(v) \leq d'$. Then:

\[ |\operatorname {Ball}(n, \delta n - 1)| \leq |\operatorname {Ball}(n, d')| \leq 2^{h(\delta ) \cdot n} {\lt} 2^{(m:\mathbb {R})} = 2^m, \]

where the second inequality is Theorem 276 (since $d' + 1 \leq \delta n$), the third uses $h(\delta ) \cdot n {\lt} m$ and strict monotonicity of $x \mapsto 2^x$.

Lemma 445 Existence of Code with Both Good Distance and Dual Distance

✓

Let $\delta \in \mathbb {R}$ with $0 {\lt} \delta \leq 1/2$, and $n, k \in \mathbb {N}$ with $0 {\lt} n$, $0 {\lt} k$, $k {\lt} n$. Suppose

\[ k + 1 {\lt} (1 - h(\delta )) \cdot n \quad \text{and} \quad n - k + 1 {\lt} (1 - h(\delta )) \cdot n. \]

Then there exists a classical code $\mathcal{C}$ of length $n$ with $\dim (\mathcal{C}) = k$, $d(\mathcal{C}) \geq \delta n$, and $d(\mathcal{C}^\perp ) \geq \delta n$.

Proof ▶

orange[Uses unproven axiom: thm:exists_good_surjective_map]

Set $r = n - k$, so $0 {\lt} r \leq n$ and $n - r = k$.

Ball bounds: From $k + 1 {\lt} (1-h(\delta ))n$ we get $h(\delta ) \cdot n {\lt} r$, so by Lemma 444:

\[ |\operatorname {Ball}(n, \delta n - 1)| {\lt} 2^r. \]

From $n - k + 1 {\lt} (1-h(\delta ))n$ we get $h(\delta ) \cdot n {\lt} k = n - r$, so similarly:

\[ |\operatorname {Ball}(n, \delta n - 1)| {\lt} 2^{n-r}. \]

Applying the axiom: By Theorem 431, there exists a surjective $\phi : \mathbb {F}_2^n \to \mathbb {F}_2^r$ with: (i) every nonzero $v$ with $\operatorname {wt}(v) {\lt} \delta n$ satisfies $\phi (v) \neq 0$; (ii) every $w \in (\ker \phi )^\perp $ with $w \neq 0$ satisfies $\operatorname {wt}(w) \geq \delta n$.

Let $\mathcal{C} = \texttt{ofParityCheck}(\phi ) = \ker \phi $.

Dimension: Since $\phi $ is surjective, $\operatorname {finrank}(\operatorname {range}(\phi )) = r$ (the range equals $\mathbb {F}_2^r$). By rank–nullity, $\operatorname {finrank}(\ker \phi ) = n - r = k$.

Distance: For nonzero $v \in \ker \phi = \mathcal{C}$, we have $\phi (v) = 0$. If $\operatorname {wt}(v) {\lt} \delta n$, property (i) would give $\phi (v) \neq 0$, a contradiction. Hence $\operatorname {wt}(v) \geq \delta n$. Since $\operatorname {finrank}(\ker \phi ) = k \geq 1$, $\mathcal{C}$ is nontrivial ($\texttt{Module.finrank\_ pos\_ iff}$), so there exists a nonzero codeword. By Lemma 432, $d(\mathcal{C}) \geq \delta n$.

Dual distance: By Theorem 259 and Theorem 48, we compute $\dim (\mathcal{C}^\perp ) = n - k = r \geq 1$, so $\mathcal{C}^\perp $ is nontrivial. Property (ii) gives that every nonzero $w \in \mathcal{C}^\perp $ has $\operatorname {wt}(w) \geq \delta n$. By Lemma 432, $d(\mathcal{C}^\perp ) \geq \delta n$.

Lemma 446 Satisfiability of Both Distance Premises

✓

There exist $\delta \in \mathbb {R}$ and $n, k \in \mathbb {N}$ satisfying all premises of Lemma 445: $0 {\lt} \delta $, $\delta \leq 1/2$, $0 {\lt} n$, $0 {\lt} k$, $k {\lt} n$, $k + 1 {\lt} (1-h(\delta ))n$, and $n - k + 1 {\lt} (1-h(\delta ))n$.

Proof ▶

We exhibit the witness $\delta = 1/100$, $n = 1000$, $k = 500$. All numerical bounds are checked by $\texttt{norm\_ num}$. Both inequalities $501 {\lt} (1-h(1/100)) \cdot 1000$ and $501 {\lt} (1-h(1/100)) \cdot 1000$ follow from $h(1/100) {\lt} 499/1000$ (Lemma 443) by linear arithmetic.

Theorem 447 Gilbert–Varshamov Plus

✓

Let $\delta \in \mathbb {R}$ with $0 {\lt} \delta {\lt} 11/100$, and let $n \in \mathbb {N}$ with $0 {\lt} n$ and

\[ n {\gt} \frac{2}{1/2 - h(\delta )}. \]

Then there exists a classical code $\mathcal{C}$ of length $n$ such that:

$\dim (\mathcal{C}) {\gt} n/2$,
$d(\mathcal{C}) \geq \delta n$,
$d(\mathcal{C}^\perp ) \geq \delta n$.

Proof ▶

orange[Uses unproven axiom: thm:exists_good_surjective_map (via Lemma 445)]

From $\texttt{binaryEntropy\_ lt\_ half}$ applied to $0 {\lt} \delta $ and $\delta {\lt} 11/100$, we have $h(\delta ) {\lt} 1/2$, so $\delta \leq 1/2$ by linear arithmetic.

Finding $k$: By Lemma 424, there exists $k \in \mathbb {N}$ with

\[ n/2 {\lt} k, \quad k + 1 {\lt} (1 - h(\delta )) \cdot n, \quad k {\lt} n. \]

Positivity of $k$: We show $0 {\lt} k$ by contradiction. If $k = 0$, then the lower bound gives $n/2 {\lt} 0$, contradicting $n/2 \geq 0$.

Lower bound for dual condition: By Lemma 423, $(1/2 - h(\delta )) \cdot n {\gt} 2$. Hence:

\[ n - k + 1 {\lt} n - n/2 + 1 = n/2 + 1 {\lt} (1 - h(\delta )) \cdot n, \]

where the last step uses $n/2 + 1 {\lt} (1-h(\delta )) \cdot n$, which follows from $(1/2 - h(\delta )) \cdot n {\gt} 2$ by linear arithmetic.

Applying the combined existence lemma: By Lemma 445 (with $\delta $, $n$, $k$ as above), there exists $\mathcal{C}$ with $\dim (\mathcal{C}) = k$, $d(\mathcal{C}) \geq \delta n$, and $d(\mathcal{C}^\perp ) \geq \delta n$.

Conclusion: We have $\dim (\mathcal{C}) = k {\gt} n/2$ (casting to reals from the bound on $k$), together with the two distance bounds.