117 Kikuchi LDC — High Value
117.1 Overview
This module records the high-value observation (Lemma 5.1) of the Alrabiah–Guruswami–Kothari–Manohar near-cubic lower bound for \(3\)-query locally decodable codes: if \(C\) is \((3,\delta ,\varepsilon )\)-normally decodable, then the XOR instances \(\psi _b\) attached to \(C\) have large value, \(\mathbb {E}_b[\mathrm{val}(\psi _b)] \ge 2\varepsilon \). It is formalised here in the existential form asserting a single message and assignment on which the XOR polynomial already reaches \(2\varepsilon \).
117.2 Declarations
Let \(L\) be a normal form \((3,\delta ,\varepsilon )\)-decodable code with message length \(k \gt 0\), block length \(n \gt 0\) and at least one constraint, i.e. \(m \gt 0\), and suppose the advantage satisfies \(\varepsilon \le 1/2\). Then there are a message \(b : \mathrm{Fin}\, k \to \mathbb {Z}\) and an assignment \(x : \mathrm{Fin}\, n \to \mathbb {Z}\), both taking values in \(\{ -1,1\} \), such that the XOR polynomial of \(L\) satisfies
Placeholder. The paper’s Lemma 5.1 bounds the expectation \(\mathbb {E}_b[\mathrm{val}(\psi _b)] \ge 2\varepsilon \); the Lean statement asserts only that some \(b\) and \(x\) achieve the bound, and is discharged by the constant all-ones witness. The expectation bound is not formalised here.