cronokirby

(2026-05) FRI Soundness Above the Johnson Bound via Threshold Halving

2026-05-01

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 RS[F,L,k]\mathrm{RS}[F, L, k] with k=2mk = 2^m and LL admitting a fixed-point-free involution (standard for deployed FRI, in either characteristic), for every δ∈(δJ,1−ρ)\delta \in (\delta_J,\, 1-\rho): εFRI≤nR∣F∣+(1−δ2)q.\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 ∼2×{\sim}2{\times} query overhead is optimal within the correlated-agreement (CA) framework: εca(C,δ,δ)=(nw)/∣F∣\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 pp-dependent list-size bounds: E[M]=(nw)/pc\mathbb{E}[M] = \binom{n}{w}/p^c at all codimension excesses c≥1c \geq 1; a sub-Poisson Bernstein tail at c=2c = 2; and a phase-diagram conjecture at c≥3c \geq 3 (the deployment regime) predicting a linear Mtrue≤⌊(2D−1)/c⌋M_{\mathrm{true}} \leq \lfloor (2D-1)/c \rfloor.

Impact for Ethereum. Every deployed and proposed FRI-based system — SP1, RISC Zero, Plonky3, the ∼30{\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 ∼2{\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.