Paper 2026/2424

Counterexamples to Beyond-Johnson Proximity Gaps over Binary Fields

Abstract

Many hash-based proof systems check that committed words are close to Reed–Solomon codewords by testing one random combination of them. Their soundness analysis uses a *proximity gap*: if the combination agrees with a codeword on many positions, so do the original words, on the same positions, except for a few *exceptional* challenges. Such gaps are known above the Johnson threshold, about $\sqrt\rho$ for rate $\rho$, and extending them below it would shrink proofs. Recent work does so in large characteristic, but not for the additive domains used over binary fields, where some of the fastest proof systems run. We show that on these domains, beyond-Johnson proximity gaps fail. Our first construction applies to any additive domain (a linear subspace) filling a constant fraction of a containing binary field, such as the length-$2^{27}$ domain of Binius64. Over a suitable extension challenge field and at rate $1/4$, it gives two words that can simultaneously match codewords on at most $25\%$ of the positions, while their combinations approach the $50\%$ Johnson threshold for superpolynomially many challenges. This rules out any $\mathrm{poly}(N)/|\mathbb F|$ bound on the exceptional probability below Johnson. The construction also rules out polynomial-size decoding lists below Johnson: one word agrees with superpolynomially many codewords at agreement approaching $50\%$. Earlier superpolynomial lists needed the rate, or the agreement–rate gap, to vanish. Our second and third constructions cover every additive domain, including the sparse domains used by LeanVM and Flock. At rate $1/16$, the second gives $(N-1)(N-2)/6$ exceptional challenges at the Johnson threshold itself, when the domain lies in a proper subfield of the challenge field. The third construction trades agreement for larger exception counts: at rate $1/2$ and length $2^{22}$, its combinations reach $53.125\%$ agreement from common agreement $50\%$, with probability at least $2^{-20}$ over a $192$-bit challenge field. Finally, at every fixed rate, some constant agreement above the rate makes every challenge exceptional, over $\mathrm{poly}(N)$-size challenge fields. All of our results are formally verified in Lean.

Note: This revision improves the exposition; the results and theorem numbering are unchanged. - Rewrote the introduction and technical overview, and expanded the comparison with related and concurrent work. - Moved the deployed-system bounds to a new Section 7 and longer proofs to a new Appendix A. - Updated the Lean formalization to Lean v4.35.0 and current ArkLib.