Products of the block interpolation family

The generators consist of one low-degree monomial per block, optionally multiplied by that block's majority. We only need their spanning property.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.majority_sq {m : ℕ} (x : Finset (Fin (2 * m + 1))) : majority x * majority x = majority x

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.atomWeight_le {m : ℕ} (a : Atom m) : atomWeight a ≤ m + 1

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.lowSpan_map_mem {m : ℕ} {V : Type u_1} [AddCommMonoid V] [Module (ZMod 2) V] (L : (Finset (Fin (2 * m + 1)) → ZMod 2) →ₗ[ZMod 2] V) (W : Submodule (ZMod 2) V) (h : ∀ (a : Low (Fin (2 * m + 1)) m), L (monomial ↑a) ∈ W) {q : Finset (Fin (2 * m + 1)) → ZMod 2} (hq : q ∈ lowSpan m) : L q ∈ W

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.atom_spans {m : ℕ} (f : Finset (Fin (2 * m + 1)) → ZMod 2) : f ∈ Submodule.span (ZMod 2) (Set.range atomEval)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.product_mem_span {k m : ℕ} (f : Fin k → Finset (Fin (2 * m + 1)) → ZMod 2) : (fun (x : BlockCube k m) => ∏ i : Fin k, f i (x i)) ∈ Submodule.span (ZMod 2) (Set.range termEval)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.terms_span {k m : ℕ} (f : BlockCube k m → ZMod 2) : f ∈ Submodule.span (ZMod 2) (Set.range termEval)

The block product family spans every function on the input cube.