Polynomial correlation: definitions

We use the set of true coordinates to encode a Boolean block. A block has odd length 2 * m + 1, and majority is one exactly when its cardinality exceeds m. The result being formalized is Theorem 1.1 of Chattopadhyay, Hatami, Lee, Lovett, Tal, and Viola, Exponential Correlation Bounds for Polynomials (2026), https://arxiv.org/abs/2609.28839.

def Complexity.BooleanAnalysis.PolynomialCorrelation.monomial {ι : Type u_1} [DecidableEq ι] (a x : Finset ι) : ZMod 2

Boolean monomials, evaluated on the set of true coordinates.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.monomial a x = if a ⊆ x then 1 else 0

@[reducible, inline]

abbrev Complexity.BooleanAnalysis.PolynomialCorrelation.Low (ι : Type u_1) (m : ℕ) : Type u_1

Squarefree monomials of degree at most m.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.Low ι m = { a : Finset ι // a.card ≤ m }

def Complexity.BooleanAnalysis.PolynomialCorrelation.lowSpan {ι : Type u_1} [DecidableEq ι] (m : ℕ) : Submodule (ZMod 2) (Finset ι → ZMod 2)

The low-degree space on a single Boolean block.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Complexity.BooleanAnalysis.PolynomialCorrelation.BlockCube (k m : ℕ) : Type

An input consisting of k disjoint blocks of odd length 2 * m + 1.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.BlockCube k m = (Fin k → Finset (Fin (2 * m + 1)))

def Complexity.BooleanAnalysis.PolynomialCorrelation.majority {m : ℕ} (x : Finset (Fin (2 * m + 1))) : ZMod 2

Strict majority on a block of odd length.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.majority x = if m < x.card then 1 else 0

def Complexity.BooleanAnalysis.PolynomialCorrelation.xorMajority {k m : ℕ} (x : BlockCube k m) : ZMod 2

XOR of the majorities of the disjoint blocks.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.xorMajority x = ∑ i : Fin k, Complexity.BooleanAnalysis.PolynomialCorrelation.majority (x i)

def Complexity.BooleanAnalysis.PolynomialCorrelation.blockBits {k m : ℕ} (x : BlockCube k m) (ij : Fin k × Fin (2 * m + 1)) : ZMod 2

Read the individual bits from a block input.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.blockBits x ij = if ij.2 ∈ x ij.1 then 1 else 0

def Complexity.BooleanAnalysis.PolynomialCorrelation.bitsToBlocks {k m : ℕ} (x : Fin k × Fin (2 * m + 1) → ZMod 2) : BlockCube k m

Collect the true coordinates of each block of a binary assignment.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.bitsToBlocks x i = {j : Fin (2 * m + 1) | x (i, j) = 1}

def Complexity.BooleanAnalysis.PolynomialCorrelation.xorMajorityBits {k m : ℕ} (x : Fin k × Fin (2 * m + 1) → ZMod 2) : ZMod 2

XOR of block majorities on ordinary ZMod 2 bit assignments.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BooleanAnalysis.PolynomialCorrelation.polynomialEval {k m : ℕ} (p : MvPolynomial (Fin k × Fin (2 * m + 1)) (ZMod 2)) (x : BlockCube k m) : ZMod 2

Evaluate a multivariate polynomial on the bits of a block input.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.polynomialEval p x = (MvPolynomial.eval (Complexity.BooleanAnalysis.PolynomialCorrelation.blockBits x)) p

def Complexity.BooleanAnalysis.PolynomialCorrelation.middleBandCount (m d : ℕ) : ℕ

The number of low monomials in the top d levels of an odd block. The additive inequality also handles d > m without truncated subtraction.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.middleBandCount m d = {a : Finset (Fin (2 * m + 1)) | a.card ≤ m ∧ m < a.card + d}.card

noncomputable def Complexity.BooleanAnalysis.PolynomialCorrelation.correlation {α : Type u_1} [Fintype α] (f g : α → ZMod 2) : ℝ

Absolute uniform correlation of two binary-valued functions.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.correlation f g = |(∑ x : α, if f x = g x then 1 else -1) / ↑(Fintype.card α)|

@[reducible, inline]

abbrev Complexity.BooleanAnalysis.PolynomialCorrelation.Atom (m : ℕ) : Type

An index for the single-block interpolation family.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.Atom m = (Complexity.BooleanAnalysis.PolynomialCorrelation.Low (Fin (2 * m + 1)) m × Bool)

def Complexity.BooleanAnalysis.PolynomialCorrelation.atomEval {m : ℕ} (a : Atom m) (x : Finset (Fin (2 * m + 1))) : ZMod 2

A low monomial, optionally multiplied by majority.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BooleanAnalysis.PolynomialCorrelation.atomWeight {m : ℕ} (a : Atom m) : ℕ

The modified degree used in the paper's multiplication argument.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.atomWeight a = if a.2 = true then m + 1 else (↑a.1).card

@[reducible, inline]

abbrev Complexity.BooleanAnalysis.PolynomialCorrelation.Term (k m : ℕ) : Type

A product of one interpolation generator from each block.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.Term k m = (Fin k → Complexity.BooleanAnalysis.PolynomialCorrelation.Atom m)

def Complexity.BooleanAnalysis.PolynomialCorrelation.termEval {k m : ℕ} (a : Term k m) (x : BlockCube k m) : ZMod 2

Evaluation of a product generator.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.termEval a x = ∏ i : Fin k, Complexity.BooleanAnalysis.PolynomialCorrelation.atomEval (a i) (x i)

def Complexity.BooleanAnalysis.PolynomialCorrelation.weight {k m : ℕ} (a : Term k m) : ℕ

The sum of modified degrees over the blocks.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.weight a = ∑ i : Fin k, Complexity.BooleanAnalysis.PolynomialCorrelation.atomWeight (a i)

def Complexity.BooleanAnalysis.PolynomialCorrelation.filtration (k m r : ℕ) : Submodule (ZMod 2) (BlockCube k m → ZMod 2)

Functions spanned by generators of weight at most r.

Equations

• One or more equations did not get rendered due to their size.