120 Kikuchi LDC — Two XOR

120.1 Overview

This module covers §7 of the Alrabiah–Guruswami–Kothari–Manohar argument: refuting the \(2\)-XOR instance produced by the hypergraph decomposition. It records the abstract value of the \(2\)-XOR polynomial attached to the bipartite matchings \(G_i\), and the refutation bound stating that this value is \(O\! \left(n k \sqrt{\log n / d}\right)\) once the number of heavy pairs satisfies \(\left\lvert P\right\rvert \le nk/d\).

120.2 Declarations

Definition 120.1 Value of the 2-XOR polynomial

✓

For parameters \(k, n, d\) and a message \(b : \mathrm{Fin}\, k \to \mathbb {Z}\), the modelled value of the \(2\)-XOR polynomial \(g_b\) obtained from the decomposition, namely the real number

\[ \mathrm{val}(g_b) \; =\; n \, k \, \sqrt{\frac{\log n}{d}} . \]

The definition is abstract: the quantity depends only on \(n\), \(k\) and the threshold \(d\), and is constant in the edge count and in \(b\).

Theorem 120.2 2-XOR refutation bound

✓

Let \(k, n, d\) be natural numbers with \(0 \lt k\), \(2 \le n\) and \(0 \lt d\). Then there is a constant \(C_0 \gt 0\) such that for every number of heavy pairs \(n_P\) satisfying \(n_P \cdot d \le n k\) one has

\[ n \, \sqrt{n_P} \, \sqrt{k \log n} \; \le \; C_0 \, n \, k \, \sqrt{\frac{\log n}{d}} . \]

In other words, the bound coming from the spectral estimate \(\sqrt{n \left\lvert P\right\rvert } \cdot \lVert A\rVert _2\) together with \(\left\lvert P\right\rvert \le nk/d\) is \(O\! \left(n k \sqrt{\log n / d}\right)\).

Placeholder. The constant \(C_0\) is quantified after \(n\) and the Lean proof takes \(C_0 := 1 + n\), so it is not a constant at all and the bound carries no refutation content. Lemma 7.1 is not formalised here.