A linear code over a finite field 
with 
elements is a linear subspace 
. The vectors
in this subspace are called codewords.
A linear error-correcting code uses a large
minimum Hamming distance between distinct codewords to permit recovery from errors by choosing a
nearest codeword.
The dual code 
consists of the vectors orthogonal
to every codeword of 
.
In a random-access model, encoded coordinates are read independently and uniformly
with replacement. A coordinate is recoverable once its value is determined by the
observed coordinates for every codeword consistent with
those observations. Let 
be the expectation value of the number of reads
needed to recover coordinate 
. A coordinate that is identically
zero is known without any reads, so its recovery time is zero. The linear code is
called recovery balanced when 
is independent of 
(Gruica et al. 2025).
MathIsEvenEasier (2026) reported the identity
 |
where 
is the length of the linear code. It implies that 
is recovery balanced iff its dual
code is recovery balanced, answering Conjecture 1 of Gruica et al. (2025).
For a self-dual linear code, every 
would equal 
. Nonuniform sampling is outside
the identity; requiring at least one read even for an identically zero coordinate
changes its right-hand side. GPT-6 Astra developed the proof and Lean formalization
under human direction. As of Oct. 7, 2026, a public continuous-integration run
had compiled all 13 positive modules, rejected two false controls, and reported only
standard Lean axioms for the final theorem, but independent specialist review had
not been reported (VibeMathed 2026).
A locally correctable code allows a randomized algorithm to recover a requested coordinate of a corrupted codeword from a bounded number of queries (Dvir 2016).
