114 Kikuchi LDC — Background Facts

114.1 Overview

This file collects the external background facts used by the Alrabiah–Guruswami–Kothari–Manohar near-cubic lower bound for \(3\)-query locally decodable codes: the reduction of an arbitrary \((q,\delta ,\varepsilon )\)-LDC to normal form (Fact 3.6), the rectangular matrix Khintchine inequality (Fact 4.1), and two-sided bounds on the binomial coefficient ratio \(\binom {n-2q}{\ell -q}/\binom {n}{\ell }\) (Fact 4.2). The first two are recorded in an existential form that fixes the shape of the parameters they supply; the binomial ratio bounds are proved in full.

114.2 Declarations

Theorem 114.1 Reduction to normal form, parameter shell

✓

Fact 3.6 (Yekhanin, Lemma 6.2), in the existential form used downstream: for \(q \ge 2\), \(k, n \gt 0\) and \(\delta , \varepsilon \gt 0\) there exist a length \(n' \le 6n\) and parameters \(\delta ', \varepsilon ' \gt 0\) with

\[ \delta ' \ \ge \ \frac{\varepsilon \, \delta }{3q^2\, 2^{\, q-1}}, \qquad \varepsilon ' \ \ge \ \frac{\varepsilon }{2^{2q}} . \]

These are exactly the parameters of the normally decodable code obtained from a binary \((q,\delta ,\varepsilon )\)-LDC \(C : \{ 0,1\} ^k \to \{ 0,1\} ^n\); the Lean statement asserts only the existence of such \(n', \delta ', \varepsilon '\).

Placeholder. The Lean statement quantifies over parameters only: no code, decoder, or normal-form construction occurs in it, and it is discharged by exhibiting witnesses that make the two inequalities reflexive. It records the shape of Fact 3.6’s output for downstream use and does not formalise the reduction. It must not be cited as a formalisation of that reduction.

Theorem 114.2 Rectangular matrix Khintchine bound

✓

Fact 4.1 (Tropp 2015, Theorem 4.1.1), stated abstractly through the bounding quantity it produces: for \(k \gt 0\), a variance proxy \(\sigma ^2 \gt 0\) and dimensions \(d_1, d_2 \gt 0\) there is a constant \(C_{\mathrm{MK}} \gt 0\) with

\[ C_{\mathrm{MK}} \ \le \ \sqrt{\, 2\, \sigma ^2 \log (d_1 + d_2)\, }. \]

This is the bound the Khintchine inequality supplies for \(\mathbb {E}\bigl[\lVert \sum _i b_i X_i\rVert _2\bigr]\) when the \(b_i\) are i.i.d. uniform signs and \(\sigma ^2 = \max \bigl(\lVert \sum _i X_i X_i^{\mathsf T}\rVert _2, \lVert \sum _i X_i^{\mathsf T} X_i\rVert _2\bigr)\).

Placeholder. No matrices, random signs, or spectral norms appear in the Lean statement: it asserts only that some positive real lies below the stated square root, and is discharged by taking that square root itself. It records the shape of the Khintchine bound for downstream use and does not formalise Tropp’s inequality. It must not be cited as a formalisation of that inequality.

Definition 114.3 Real-valued binomial coefficient

✓

For naturals \(n\) and \(k\), \(\texttt{chooseR}\, n\, k\) is the binomial coefficient \(\binom {n}{k}\) cast into \(\mathbb {R}\).

Theorem 114.4 Binomial ratio bound, upper

✓

Fact 4.2 (upper half). Let \(n, \ell , q\) be naturals with \(n \gt 0\), \(q \gt 0\), \(q \le \ell \), \(2\ell \le n\) and \(2q \le n\). Then

\[ \frac{\binom {n-2q}{\ell -q}}{\binom {n}{\ell }} \ \le \ e^{3q}\left(\frac{\ell }{n}\right)^{q}, \]

where both binomial coefficients are taken in \(\mathbb {R}\) via \(\texttt{chooseR}\).

Theorem 114.5 Binomial ratio bound, lower

✓

Fact 4.2 (lower half). Under the same hypotheses \(n \gt 0\), \(q \gt 0\), \(q \le \ell \), \(2\ell \le n\) and \(2q \le n\),

\[ e^{-3q}\left(\frac{\ell }{n}\right)^{q} \ \le \ \frac{\binom {n-2q}{\ell -q}}{\binom {n}{\ell }}, \]

with the binomial coefficients again read in \(\mathbb {R}\) via \(\texttt{chooseR}\).