Paper 2026/858

FRI Soundness Above the Johnson Bound via Threshold Halving

Abstract

We prove the first unconditional soundness theorem above the Johnson bound for FRI, STIR, and WHIR — the proximity-testing protocols underlying every deployed STARK, zkVM, and FRI-based system on Ethereum's roadmap. For $\mathrm{RS}[F, L, k]$ with $k = 2^m$ and $L$ admitting a fixed-point-free involution (standard for deployed FRI, in either characteristic), for every $\delta \in (\delta_J,\, 1-\rho)$: $$\varepsilon_{\mathrm{FRI}} \;\leq\; \frac{nR}{|F|} \;+\; \left(1 - \frac{\delta}{2}\right)^{\!q}.$$ Three results. (A) The bound above, via threshold halving from Rothblum–Vadhan–Wigderson (STOC 2013); the protocol, prover messages, and verifier checks are unchanged — only the query parameter is recalibrated. The argument enters the unique-decoding regime after one round, where BCIKS locks the distance, making it immune to any open-zone counterexample. (B) The ${\sim}2{\times}$ query overhead is optimal within the correlated-agreement (CA) framework: $\varepsilon_{\mathrm{ca}}(C, \delta, \delta) = \binom{n}{w}/|F|$, tight for large fields, exponential in the code length, and vacuous at FRI scale. (C) First $p$-dependent list-size bounds: $\mathbb{E}[M] = \binom{n}{w}/p^c$ at all codimension excesses $c \geq 1$; a sub-Poisson Bernstein tail at $c = 2$; and a phase-diagram conjecture at $c \geq 3$ (the deployment regime) predicting a linear $M_{\mathrm{true}} \leq \lfloor (2D-1)/c \rfloor$. Impact for Ethereum. Every deployed and proposed FRI-based system — SP1, RISC Zero, Plonky3, the ${\sim}30$ zkVMs on EthProofs, Stwo (Mersenne31 / circle FRI), the planned post-quantum signature aggregation layer — now has a positive proven soundness floor in the open zone above Johnson, replacing a conjecture whose up-to-capacity form was disproved in late 2025 by Crites–Stewart and independently by Kambiré. The cost is a factor ${\sim}2$ in queries; the bound holds in characteristic 2 via additive folding, on the unit circle via the Stwo coupling, and compiles to non-interactive knowledge soundness via Fiat–Shamir and DEEP. The half-threshold CA bound is formally verified in Lean 4 with Mathlib.