Let \(k \gt 0\), \(n \ge 2\), and let \(\delta , \varepsilon \in (0,1]\). Let \(L\) be a normal form \((3,\delta ,\varepsilon )\)-decodable code with message length \(k\) and block length \(n\), whose parameters are \(\delta \) and \(\varepsilon \). Then there is a constant \(C \gt 0\) with

Placeholder — the statement carries no lower-bound content. The constant \(C\) is quantified after \(k\), \(n\), \(\delta \), \(\varepsilon \) and the code \(L\), so it may depend on all of them; the Lean proof takes \(C = (k^3\varepsilon ^{16}\delta ^{16} + 1)/(n\log ^6 n)\), which satisfies the displayed inequality for every choice of parameters. The intended Theorem 9.1 of Alrabiah–Guruswami–Kothari–Manohar requires an absolute \(C\), quantified before the instance, and would yield \(n = \Omega (k^3/\log ^6 k)\); that theorem is not formalised here, and this entry must not be cited as a formalisation of it.

Let \(q\) be even with \(q \ge 2\), let \(k \gt 0\) and \(n \ge 2\), and let \(\delta , \varepsilon \gt 0\). Then there is a constant \(C \gt 0\) with

Placeholder — the statement carries no lower-bound content. As with the \(3\)-query case, \(C\) is quantified after all parameters and the Lean proof takes \(C = k\varepsilon ^{4}\delta ^{2}/(n^{1-2/q}\log n) + 1\), so the inequality holds for every choice of parameters. Note also that no code or decoder occurs in the hypotheses — the statement quantifies over \(q, k, n, \delta , \varepsilon \) alone. Theorem 10.1 of Alrabiah–Guruswami–Kothari–Manohar is not formalised here.