PaperlayerView exact revision on arXiv

Source-linked AI summary

A proof of the generalized packing-covering conjecture

Gianira N. Alfarano, Giuseppe Marino, Alessandro Neri, Rocco Trombetti

arXiv:2609.34910v1cs.ITmath.COmath.IT

TL;DR

The generalized packing–covering conjecture asks whether d_t(C) ≤ 2R_t(C) + 2 for every linear code and admissible order, a claim not implied by the classical inequality on an extended code. The paper combines parity-check and length bounds with successive puncturing and exact computation to prove the conjecture for all such codes and orders.

  • Problem

    The generalized packing–covering conjecture asks whether d_t(C) ≤ 2R_t(C) + 2 for every linear code and admissible order; the classical inequality on C ⊗ F_{q^t} does not establish it because that code’s minimum distance is d_1(C), not d_t(C).

    Source: §1 · p. 2

  • Method

    The proof reformulates the conjecture using parity-check columns, bounds the length of putative counterexamples, and repeatedly punctures supports found through Hamming-ball arguments.

    Source: §1 · p. 2, §3.2 · pp. 7–8, §3.3 · p. 9

  • Results

    For every [n, k]_q linear code and admissible t, d_t(C) ≤ 2R_t(C) + 2; exact calculations exclude all 59,086 remaining admissible tuples without enumerating codes.

    Source: §1 · p. 2, §4.1 · p. 12

  • Takeaways & Limitations

    The conjectured bound holds for every linear code over every finite field and every admissible order.

    Source: §1 · p. 2

    The stated result concerns admissible orders 1 ≤ t ≤ min{k, ρ}.

    Source: §2.1 · p. 4

Abstract

from arXiv · show

The generalized packing--covering conjecture of Elimelech, Firer and Schwartz asserts that, for every linear code $\mathcal{C}$ and every admissible order $t$, the $t$-th generalized Hamming weight $d_t(\mathcal{C})$ and the $t$-th generalized covering radius $R_t(\mathcal{C})$ satisfy $d_t(\mathcal{C})\le 2R_t(\mathcal{C})+2$. We give a computer-assisted proof of the conjecture for every linear code over every finite field and every admissible order. Combining a parity-check reformulation of the conjecture, bounds on the length of putative counterexamples, and successive puncturing arguments, we settle all orders $t\ge 32$ and reduce the remaining orders to finitely many parameter tuples, which we exclude by an exact computer verification.

1 Introduction

The paper proves the generalized packing–covering conjecture for every linear code over every finite field and every admissible order. Its proof combines parity-check reformulations, length bounds, puncturing, and exact computation to eliminate possible counterexamples.

1 Introduction

  • The generalized packing–covering conjecture compares the generalized packing radius ⌊(d_t(C) − 1)/2⌋ with R_t(C), but does not follow by applying the classical inequality to C ⊗ F_{q^t}.That extended code has covering radius R_t(C) but minimum distance d_1(C), not d_t(C).Source: §1 · p. 2
  • For every [n, k]_q linear code and 1 ≤ t ≤ min{k, n − k}, d_t(C) ≤ 2R_t(C) + 2.This is the conjectured bound proved in full.Source: §1 · p. 2

Outline of the proof

  • A putative counterexample must satisfy a lower length bound from Hamming-ball covering and an upper bound from restrictions on parity-check columns.If the lower bound exceeds the explicit upper bound M(q, ρ, t, r), that parameter choice is excluded.Source: Outline of the proof · p. 2
  • Exact computation handles redundancy ρ ≤ 50 and the remaining finite parameter tuples after the general bounds and puncturing steps.For each remaining tuple, the proof checks incompatible length bounds or applies Theorem 3.12 at a fixed test length, then uses Lemma 3.11 for larger lengths; the computations check inequalities and never enumerate codes.Source: Outline of the proof · pp. 2–3, Table 1 · p. 3
  • For t ≥ 32, redundancy and successive puncturing bounds settle the large-order cases, with a finite computer check for gaps 6 ≤ r − t ≤ 9.The puncturing argument finds small-support subcodes repeatedly; small orders 3 ≤ t ≤ 31 require sharper estimates, with t = 3 needing separate arguments.Source: Outline of the proof · pp. 2–3

2 Preliminaries

The preliminaries define the code parameters used in the conjecture and collect known cases and a covering bound. These tools provide conditions and length estimates used later in the proof.

2.1 Linear codes, generalized Hamming weights and covering radii

  • For a linear code, d_t(C) is the minimum support size of a t-dimensional subcode, generalizing minimum distance d(C) = d_1(C).The generalized Singleton bound is also recalled for these weights.Source: §2.1 · pp. 3–4
  • R_t(C) is the least coordinate-set size that lets each of any t vectors agree with some codeword outside that set; equivalently, it is the covering radius of C ⊗ F_{q^t}.The conjecture asserts d_t(C) ≤ 2R_t(C) + 2 for admissible t; the paper assumes t ≤ min{k, ρ} and writes r = R_t(C).Source: §2.1 · p. 4

2.2 Known cases of the conjecture and the covering bound

  • Known cases include t ≤ 2, r = t, t ≥ ρ − 4, k ≤ 5t − 2, 3r ≥ 2ρ, and k/n ≤ 3/5; q ≥ r gives the stronger d_t(C) ≤ 2r + 1.The listed small parameter pairs are (t, r) ∈ {(3, 4), (3, 5), (4, 5), (4, 6)}.Source: §2.2 · p. 5
  • The generalized ball-covering bound counts representatives for all t-tuples of syndromes inside a radius-r Hamming ball, yielding lower bounds on a putative counterexample’s length.There are q^(tρ) possible syndrome tuples; the resulting estimates are used with Hamming-ball volume bounds.Source: §2.2 · p. 5

3 Putative codes violating the conjecture

The section reformulates putative conjecture violations using parity-check columns, derives length bounds, and develops Hamming-ball and successive-puncturing bounds on generalized Hamming weights. These tools constrain the remaining cases and establish the desired inequality when earlier bounds do not suffice.

3.1 Parity-check formulation and nullity

  • dt(C) ≤ m + t holds exactly when some m-dimensional parity-check subspace contains at least m + t columns, counted with multiplicity.For a counterexample with m = 2r − t + 2, every m-dimensional subspace contains at most 2r + 1 columns.Source: §3.1 · pp. 6–7

3.2 Upper bounds on the length of a putative counterexample

  • For an [n, k]q linear code C with redundancy ρ, t ∈ [min{k, ρ}], and r = Rt(C), if dt(C) ≥ 2r + 3, then n ≤ 2r − t + Uq(ρ − 2r + t, t + 1).Source: §3.2 · p. 8

3.3 Hamming-ball bounds and puncturing

  • If volq(N, ℓ) > q^(h+s−1), then an [N, N − h]q code satisfies ds(D) ≤ (s + 1)ℓ.The argument finds s + 1 affinely independent vectors with the same syndrome inside a Hamming ball; their differences span a subcode supported on at most (s + 1)ℓ coordinates.Source: §3.3 · p. 9
  • Puncturing the support of a minimum-support s-dimensional subcode yields a code D with ds+u(C) ≤ ds(C) + du(D).The section also gives a way to enlarge a set while preserving its nullity, and to shorten a code to fixed length N while retaining an upper bound on dt for the original code.Source: §3.3 · pp. 9–10
  • Repeatedly applying the Hamming-ball bound after puncturing each obtained support provides a framework for bounding dt(C) from a sequence of pairs (ℓi, si).The theorem’s stated hypotheses include that the si sum to t and the accumulated support bound is at most B.Source: §3.3 · p. 10
  • Successive puncturing builds a kernel of dimension t supported on at most B coordinates, yielding d_t(C) ≤ B.At each step, the selected support has nullity s_i; when needed, it is enlarged so puncturing increases the kernel dimension by exactly s_i.Source: §3.3 · pp. 10–11
  • If t ≤ A(2L − 1), n > 2t + 2L, and vol_q(n − 2t − 2L, 2) > q^(ρ + A − 1), then d_t(C) ≤ 2t + 2L.The corollary applies to an [n, n − ρ]_q linear code with t ∈ [n − ρ] and L, A ≥ 1.Source: §3.3 · p. 11
  • The resulting upper bound on counterexample length is compared with lower bounds, and Theorem 3.12 and Corollary 3.13 can prove d_t(C) ≤ 2r + 2 when those bounds do not contradict.Source: §3.3 · p. 11

4 Reduction to finitely many parameters

This section reduces putative counterexamples to finite parameter ranges using length and redundancy bounds and puncturing, settling small redundancy and radius gaps before treating orders t ≥ 32. For t ≥ 32, it rules out counterexamples through finite step schedules or puncturing and staged Hamming-radius steps, according to a = r − t.

4.1 Initial reductions

  • For redundancy ρ ≤ 50, d_t(C) ≤ 2R_t(C) + 2; exact calculations exclude all 59,086 admissible parameter tuples without enumerating codes.The calculation excludes 39,627 tuples by a length comparison and 19,459 by generalized-weight bounds.Source: §4.1 · p. 12

4.2 Large redundancy and small radius gaps

  • For a = r − t ≥ 1, t ≥ max{132, 5a^2} implies d_t(C) ≤ 2r + 2.Thus a counterexample with fixed gap a cannot have arbitrarily large order.Source: §4.2 · p. 12
  • For each fixed pair (t, r) with 3 ≤ t ≤ min{k, ρ}, the theorem gives a threshold D(t, r) above which ρ implies d_t(C) ≤ 2r + 2.The result uses a single Hamming ball and establishes ℓ_t > r for its chosen radius parameter.Source: §4.2 · p. 14
  • If R_t(C) ≤ t + 5, then d_t(C) ≤ 2R_t(C) + 2 for every admissible order t.The proof combines the large-order and small-redundancy results with an exact check of the remaining finite parameter tuples.Source: §4.2 · pp. 14–15

4.3 The case t ≥32

  • For t ≥ 32 and r ≤ 2t, d_t(C) ≤ 2r + 2.This proposition treats one of the ranges used to prove the conjecture for orders t ≥ 32.Source: §4.3 · pp. 15, 17
  • For t ≥ 32 and a = r − t ≥ 6, a counterexample must have ρ/r > 2; under ℓt ≥ r and 12ℓ ≤ r, vol_q(n − 2r − 2, ℓ) > q^(ρ+ℓ(t+1)−2r).The volume bound supports puncturing arguments by estimating Hamming balls after up to 2r + 2 coordinates are removed.Source: §4.3 · pp. 15–16
  • For 6 ≤ a ≤ 9, finite (t, a) cases are checked using Theorem 3.12 step schedules, yielding d_t(C) ≤ B and contradicting the assumed counterexample.For each pair, the input records specify positive-integer steps (ℓ_i, s_i), which the program checks against the theorem’s conditions.Source: §4.3 · p. 17
  • For a ≥ 10 and t ≥ 3a, puncturing a 3a-coordinate support set and applying Corollary 3.13 yields a t-dimensional subcode supported on at most B coordinates, contradicting d_t(C) > B.The initial subcode has dimension a − 1; the punctured code supplies the remaining nullity u = t − a + 1.Source: §4.3 · p. 18
  • For a ≥ 10 and t < 3a, the proof uses radius-4 steps to reach nullity c, radius-3 steps to reach a, and radius-2 steps to reach t.At each step it chooses s = min{d, ℓ(t + 1) − 2r + 1 + W − S}; the resulting support bound is W = 2t + a + c + 4L4 + 3L3 + 2L2.Source: §4.3 · pp. 18–19

Appendix A.2 proves that the steps chosen by (35) satisfy

This section develops puncturing arguments and bounds on possible counterexamples to establish the generalized packing-covering inequality across the stated order and radius ranges. It also gives exponential and exact rational estimates for punctured Hamming balls used in finite parameter checks and large-radius thresholds.

Appendix A.2 proves that the steps chosen by (35) satisfy

  • For 32 ≤ t ≤ min{k, ρ}, d_t(C) ≤ 2R_t(C) + 2, proved by puncturing in cases determined by the radius.The argument handles r − t ≤ 5 separately, then uses Propositions 4.7–4.9 for r ≤ 2t, 2t ≤ r ≤ 3t, and r ≥ 3t; the puncturing steps meet the volume and support bounds needed by Theorem 3.12.Source: Appendix A.2 · pp. 20–21

4.4 The case 3 ≤t ≤31

  • For 3 ≤ t ≤ 31, the argument seeks explicit upper bounds on the radius of a possible counterexample, using separate estimates for t = 3 and larger orders.For 4 ≤ t ≤ 31, it uses the implication ρ > 2r when r > 2t to sharpen Hamming-ball estimates, then returns to large-radius cases for t = 3.Source: §4.4 · p. 22

4.4.1 A preliminary estimate for t = 3

  • For t = 3, d_3(C) ≤ 2r + 2 if ρ ≤ 2r + 2 over every finite field, or if ρ ≤ 2r + 3 over the binary field.The proof bounds Hamming-ball volumes to contradict the counterexample assumption.Source: §4.4.1 · p. 22

4.4.2 Redundancy of a putative counterexample

  • If a code is a counterexample for order t and r = R_t(C) > 2t, then its redundancy satisfies ρ > 2r.The lemma covers 3 ≤ t ≤ min{k, ρ}.Source: §4.4.2 · p. 23

4.4.3 Hamming balls after puncturing

  • For t ≤ 31, the section derives a sharper lower bound for ordinary Hamming balls after puncturing using a covering lower bound on n and an elementary binomial-coefficient estimate.Source: §4.4.3 · p. 24
  • The puncturing estimate uses β_q(W, ℓ) to measure losses and yields an exponential Hamming-ball bound when that quantity is sufficiently large.Lemma 4.14 applies under stated conditions on the code and parameters; its conclusions also extend to every q ≥ q0 when the β condition holds at q0.Source: §4.4.3 · p. 25
  • An exact rational version avoids the factorial approximation and lets the required inequalities be checked with integer arithmetic.Lemma 4.15 gives this alternative estimate for q ≥ q0 when λ = ρ/r > 2 and ℓt ≥ r.Source: §4.4.3 · p. 26
  • The estimates yield an explicit large-radius threshold for each order 4 ≤ t ≤ 31.The lemma hypotheses can be checked using integer arithmetic after clearing denominators.Source: §4.4.3 · p. 27

4.4.4 The case of large r for 4 ≤t ≤31

For orders 4 ≤ t ≤ 31, this section establishes radius bounds and reduces possible counterexamples to finite parameter sets, which are excluded by exact computation to prove the conjecture. It also uses known explicit weight hierarchies to derive lower bounds on generalized covering radii for several code families.

4.4.4 The case of large r for 4 ≤t ≤31

  • For 4 ≤ t ≤ min{k, ρ, 31}, r ≥ r0(t) implies d_t(C) ≤ 2r + 2.The thresholds r0(t) are specified in Table 2.Source: §4.4.4 · p. 28

4.4.5 The case of large r for t = 3

  • For t = 3, the conjectured bound holds when q = 3 and r ≥ 48, q ≥ 4 and r ≥ 26, or q = 2 and r ≥ 192.These results bound r for every field size when t = 3.Source: §4.4.5 · pp. 28–30

4.5 The remaining parameter set

  • 619,126 tuples in the residual parameter range were eliminated by lower bounds on n or verified puncturing arguments, leaving no counterexample.The checks split into 154,813 cases contradicted by a lower bound on n, 158,985 handled using Lemma A.2, and 305,328 handled using Theorem 3.12.Source: §4.5 · p. 31

4.6 The remaining finite cases

  • 65,360 numerical tuples were excluded in the final finite-case verification, with every comparison checked exactly.Of these, 1,216 had a lower bound on n exceeding M(q, ρ, t, r), and the other 64,144 were settled by puncturing sequences.Source: §4.6 · p. 32

4.7 Proof of the conjecture

  • For every linear code C and admissible 1 ≤ t ≤ min{k, n − k}, the paper proves d_t(C) ≤ 2R_t(C) + 2.The proof completes the conjecture after excluding all infinite parameter ranges and the remaining finite set.Source: §4.7 · p. 32

4.4.4 The case of large r for 4 ≤t ≤31

  • For 4 ≤ t ≤ 31, Theorem 4.16 excludes r ≥ r0(t); for t = 3, Theorems 4.17 and 4.18 exclude r ≥ 48 when q = 3, r ≥ 26 when q ≥ 4, and r ≥ 192 when q = 2.Source: §4.7 · p. 33
  • Theorem 4.20 rules out every tuple satisfying Eq. (54), so no counterexample remains and dt(C) ≤ 2Rt(C) + 2.Source: §4.7 · p. 33
  • Explicit weight hierarchies for cyclic, q-ary Reed–Muller, affine Cartesian, and other code families give explicit lower bounds on their generalized covering radii.Source: §4.7 · p. 33

Declaration on the use of AI

The authors describe a proof strategy developed by the authors, with ChatGPT 6-Astra assisting its refinement, computational treatment, exposition, and program writing; the authors reviewed and verified the paper’s content and take responsibility for it.

Declaration on the use of AI

  • The authors proposed the proof strategy and developed the parity-check reformulation and length-bound comparison with ChatGPT 6-Astra through iterative discussion.The tool also helped refine intermediate estimates, identify parameter ranges requiring computation, and organize the exposition.Source: Declaration on the use of AI · p. 33
  • ChatGPT 6-Astra assisted with writing the search and verification programs described in Appendix A and with technical writing in Section 4.Source: Declaration on the use of AI · p. 33
  • The authors state that they reviewed and verified all content, claims, and conclusions and take full responsibility for them.Source: Declaration on the use of AI · p. 33

A Bounds and computer calculations

The appendix presents generalized-weight bounds, explains the parameter checks and programs, and states that the comparisons use exact integer or rational arithmetic.

A Bounds and computer calculations

A.1 Generalized-weight bounds

This appendix constructs recursive bounds on generalized Hamming weights for codes with prescribed length, field, and redundancy. The resulting bounds apply to every code with those parameters and use necessary conditions rather than asserting code existence.

A.1 Generalized-weight bounds

  • The recursion combines ordinary distance bounds with Lemma 3.8 to bound several generalized Hamming weights at one prescribed length.Source: §A.1 · p. 35
  • For N > h ≥ 0, A_q(N, h) is defined as the largest integer d in [1, h + 1] satisfying three necessary conditions.Source: §A.1 · p. 35
  • The puncturing condition and Griesmer bound are necessary tests only; satisfying them does not assert that a code exists.The puncturing condition reduces length and distance by one while preserving dimension.Source: §A.1 · p. 35
  • The finite recursion yields B_t(q, N, h), and every [N, N − h]_q code satisfies d_t ≤ B_t(q, N, h) for admissible t.The construction maximizes over possible intermediate generalized weights so the bound does not depend on their unknown actual values.Source: §A.1 · pp. 35–36

A.2 Step counts for successive puncturing

The appendix bounds the steps in successive puncturing and uses those bounds to establish the required margin for every order t ≥ 32. Orders 32 ≤ t < 64 are checked finitely, while analytic inequalities cover t ≥ 64.

A.2 Step counts for successive puncturing

  • The recurrence for G_ℓ has base value G_ℓ(0, A) = 0 and satisfies G_ℓ(L, A) = ℓG_ℓ(L − 1, A) + A + ℓ(L − 1).For the a ≤ t/2 case, the resulting inequalities include 3 + 2 ≤ a + 2 and 2 + 4/3 < a − c + 2.Source: §A.2 · pp. 36–37
  • If G_ℓ(L, A) ≥ t and the stated length and volume conditions hold, Lemma A.2 gives d_t(C) ≤ ℓ(t + L).Its proof bounds the number of puncturing steps by L and applies Theorem 3.12.Source: §A.2 · p. 36
  • In Proposition 4.7, L_4, L_3, and L_2 bound the steps in three phases, using G_ℓ with starting parameters 5, 4, and 3.The per-step nullity recurrence yields at least G_ℓ(i, A_ℓ) after i uncapped steps.Source: §A.2 · p. 36
  • For t ≥ 64, the elementary inequalities are checked at 64 ≤ t < 128 and propagated to larger orders, proving the required margin.When a ≤ t/2, c = L4 = 0; under doubling or incrementing t, the ceiling terms grow more slowly than the corresponding right sides.Source: §A.2 · pp. 36–37
  • For 32 ≤ t < 64, the minimum margin over t/3 < a ≤ t is nonnegative for every order, as recorded in Table 3.The minima are recomputed by the independent audit code.Source: §A.2 · p. 36, Table 3 · p. 37

A.3 The finite parameter ranges

The appendix specifies finite parameter ranges for the programs and reports their tuple counts. The final range is excluded using symbolic puncturing for some pairs and numerical enumeration for the remaining cases.

A.3 The finite parameter ranges

  • An input record specifies necessary counterexample parameters, not the existence of a code with those parameters.The programs derive expected tuples from the displayed ranges and reject missing or repeated tuples; overlapping ranges do not affect each program's check.Source: §A.3 · p. 37
  • The three earlier programs check 59,086 tuples, 2,396,360 tuples, and 619,126 tuples, respectively, across their displayed parameter ranges.The third range has 3 ≤ t ≤ 31 and t + 1 ≤ r ≤ max{2t, t + 15}.Source: §A.3 · p. 37
  • The final range excludes 454 pairs (t, r) by symbolic puncturing and checks 65,360 numerical tuples for the remaining t = 3 or t = 4 cases.The 454 pairs comprise 54 with t = 4 and 400 with 5 ≤ t ≤ 31; the numerical enumeration is finite under the stated bounds on r and ρ.Source: §A.3 · p. 37

A.4 Lower bounds on the test length

The appendix bounds the length of a putative counterexample and tests whether that lower bound exceeds an upper bound. When direct comparisons are insufficient, it applies further sufficient tests, including a radius-two argument.

A.4 Lower bounds on the test length

  • For fixed (q, ρ, t, r), a proved lower bound n ≥ N excludes the tuple if N > M(q, ρ, t, r); otherwise it suffices to bound d_t for every [N, N − ρ]_q code.Lemma 3.11 transfers that bound to the original length, even though the shortened code need not have generalized covering radius r.Source: §A.4 · p. 37
  • The programs use volume-based lower bounds on n, including vol_q(n, t) ≥ q^(tρ), and compare a proposed test length N with the resulting bounds.For the strict volume test, increasing volume in the length ensures n ≥ N; the comparison distinguishes boundary cases and uses no floating-point root approximation.Source: §A.4 · pp. 37–38
  • When direct tests do not suffice, rank-x incidence and weighted-line bounds provide alternative upper bounds, and a radius-two calculation can establish d_t ≤ 2r + 2.The radius-two test uses L = a + 1 and B = 2(t + L) = 2r + 2, then applies Lemma A.2 under its stated volume and length conditions.Source: §A.4 · pp. 37–38

A.5 Checking the generalized-weight bounds

The programs verify generalized-weight records using a set of sufficient justifications and recursively checked bounds. A worked example illustrates how a bound at one order and puncturing support a bound at a higher order.

A.5 Checking the generalized-weight bounds

  • A record asserting d_j ≤ b must satisfy basic parameter checks and one of five justifications, including the Singleton bound or necessary-condition tests when j = 1.Other justifications use volume bounds, Lemma A.2, or recursive puncturing bounds.Source: §A.5 · p. 38
  • Recursive justification requires a previously verified bound on d_s and verified child bounds for every possible value of d_s.The program processes records in order and checks that records are neither duplicated nor missing and that each retained record is reachable from a root.Source: §A.5 · p. 38
  • For (q, ρ, t, r) = (2, 16, 3, 6), the record obtains d_3 ≤ 13 at length 96, meeting 2r + 2 = 14.It first proves d_2 ≤ 9, then checks each possible d_2 value from 2 through 9 by puncturing and bounding d_1; Lemma 3.11 covers every larger length.Source: §A.5 · p. 38
  • For (q, ρ, t, r) = (2, 10, 5, 6), the lower bound n ≥ 34 exceeds M(2, 10, 5, 6) = 21, excluding the tuple without a weight record.The same passage contrasts this with the (2, 16, 3, 6) example, where the length bounds are inconclusive.Source: §A.5 · p. 38

A.6 Checking the puncturing steps

The appendix checks puncturing sequences and symbolic inequalities with exact arithmetic across the remaining parameter ranges. It verifies that the recorded conditions imply the required generalized-weight bounds.

A.6 Checking the puncturing steps

  • The 1,022 symbolic sequences cover 6 ≤ a ≤ 9 and 32 ≤ t < 5a^2, with Eq. (32) checked at every step.The last inequality is checked after clearing the denominator 5a.Source: §A.6 · p. 39
  • At each puncturing step, the checks enforce the stated radius and nullity conditions, then require Sv = t and Wv ≤ 2r + 2 for Theorem 3.12.For fixed test length N, the additional condition Wv − t < ρ applies when padding to the prescribed support size is used; the resulting strict inequalities imply dt ≤ 2r + 2.Source: §A.6 · p. 39
  • The final range (54) excludes 454 pairs (t, r) independently of q and ρ through stepwise checks using K2(Wi−1, ℓi).Lemma 4.15 with q0 = 2 supplies the strict ball inequality; the records cover 400 pairs for 5 ≤ t ≤ 31 and 54 pairs for t = 4.Source: §A.6 · p. 39
  • 1,216 length contradictions and 64,144 puncturing arguments cover the numerical tuples in (54), after a volume check when N exceeds the elementary lower bound.For each tuple, the program checks either N > M(q, ρ, t, r) or every step of a puncturing sequence at N.Source: §A.6 · p. 39
  • For 4 ≤ t ≤ 31, the infinite-radius checks establish five inequalities for every integer r ≥ r0(t), rather than sampling finitely many radii.For each affine expression f(r) = αr + β, the program checks f(r0(t)) ≥ 0 and α ≥ 0; it also checks the order-three endpoint and propagation comparisons exactly.Source: §A.6 · p. 39

A.7 Programs and input files

The verification is provided as SageMath programs and input records. Separate range-checking programs use exact arithmetic, while an independently written audit rechecks totals and records.

A.7 Programs and input files

  • Running sage verify.sage unpacks the records, runs all five checking programs, and reports ALL COMPUTATIONAL CHECKS PASSED if every check succeeds.With SageMath 10.8, the complete run takes about two minutes on a standard computer.Source: §A.7 · p. 40
  • Four programs independently enumerate their parameter ranges and check every stated inequality with exact integer or rational arithmetic.They cover ρ ≤ 50, 1 ≤ r − t ≤ 5, Eq. (53), and Eq. (54) together with the large-radius bounds.Source: §A.7 · p. 40
  • A separately written audit uses none of the other programs and rechecks parameter totals, puncturing sequences, symbolic and large-radius inequalities, step counts, and record usage.The programs and records are available in the cited repository and run with SageMath 10 or later.Source: §A.7 · pp. 39–40
  • The example file demonstrates length and generalized-weight calculations for (q, ρ, t, r) = (2, 16, 3, 6), and no linear codes are enumerated.The input-record format is documented in docs/verification.md.Source: §A.7 · p. 40
Loading 2609.34910v1…