115 Kikuchi LDC — Decomposition
115.1 Overview
This module covers §6 of the Alrabiah–Guruswami–Kothari–Manohar argument: the hypergraph decomposition step. Given \(3\)-uniform hypergraphs \(H_1, \dots , H_k\) on \(\mathrm{Fin}\, n\) and a threshold \(d\), one isolates the heavy pairs, i.e. the vertex pairs of degree more than \(d\), bounds their number by \(3m/d\), and splits each \(H_i\) into a residual part whose pair-degrees are at most \(d\) and a part carried by the heavy pairs.
115.2 Declarations
For a hypergraph \(H\) on \(\mathrm{Fin}\, n\) and a threshold \(d\), the set of heavy pairs
realised as the collection of two-element sets \(\{ u,v\} \) whose degree in \(H\) exceeds \(d\).
Let \(H\) be a \(3\)-uniform hypergraph on \(\mathrm{Fin}\, n\) and let \(d \gt 0\). Then the number of heavy pairs satisfies
where \(P\) is the set of pairs of degree more than \(d\); equivalently \(\left\lvert P\right\rvert \le 3m/d\) for \(m = \left\lvert H\right\rvert \) edges, since each \(3\)-edge contributes exactly three pairs.
Let \(L\) be a normal form locally decodable code with message length \(k\) and block length \(n\), given by the \(3\)-uniform matchings \(H_i\), and let \(d \gt 0\). Then there is a family of hypergraphs \(H'_i\) on \(\mathrm{Fin}\, n\), indexed by \(i : \mathrm{Fin}\, k\), such that each \(H'_i \subseteq H_i\), each \(H'_i\) is \(3\)-uniform and a matching, and the combined hypergraph \(\bigcup _{i} H'_i\) satisfies the pair-degree bound \(d\).
Placeholder. The Lean statement omits the paper’s counting clause \(|H_i| = |H'_i| + |G_i|\), and without it the empty hypergraph satisfies every remaining clause — which is exactly the witness the proof supplies (use fun _ => \(\emptyset \)). Lemma 6.1’s content is that few edges are removed; that is not formalised here.