Boolean Möbius reconstruction

A polynomial of degree at most q, evaluated at a Boolean assignment, is reconstructed from its values on subsets of at most q coordinates. Summing this identity permits the polynomial to depend on the original assignment. Coefficients may lie in any commutative ring.

The proof uses the existing Boolean low-degree span; it introduces no multilinear polynomial representation. It follows Lemma 3.3, equation (3.10), p24 of OpenAI, The Exponential Time Hypothesis is False.

Main results

• Cslib.BitString.lowDegree_reconstruction: pointwise reconstruction in the existing span.
• Cslib.BitString.sum_eval_eq_restricted_subsets: the assignment-dependent polynomial sum.

theorem Cslib.BitString.lowDegree_reconstruction {ι : Type u_1} {R : Type u_2} [CommRing R] [Fintype ι] {q : ℕ} {f : (ι → Bool) → R} (hf : f ∈ lowDegree R ι q) (x : ι → Bool) : f x = ∑ E ∈ Finset.univ.powerset with E.card ≤ q, if ∀ i ∈ E, x i = true then ∑ U ∈ E.powerset, (-1) ^ (E.card - U.card) * f fun (i : ι) => decide (i ∈ U) else 0

A low-degree function on the cube is reconstructed from its subset evaluations.

theorem Cslib.BitString.sum_eval_eq_restricted_subsets {ι : Type u_1} {R : Type u_2} [CommRing R] [Fintype ι] (q : ℕ) (p : (ι → Bool) → MvPolynomial ι R) (hp : ∀ (x : ι → Bool), (p x).totalDegree ≤ q) : ∑ x : ι → Bool, (MvPolynomial.eval fun (i : ι) => bitVal R (x i)) (p x) = ∑ E ∈ Finset.univ.powerset with E.card ≤ q, ∑ U ∈ E.powerset, (-1) ^ (E.card - U.card) * ∑ x : ι → Bool with ∀ i ∈ E, x i = true, (MvPolynomial.eval fun (i : ι) => bitVal R (decide (i ∈ U))) (p x)

Boolean Möbius reconstruction for an assignment-dependent polynomial family, over any commutative ring (Lemma 3.3, equation (3.10) of the cited manuscript). The polynomial evaluated at 1_U is still p x, indexed by the original assignment in the restricted inner sum.