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).
