Reduction on the agreement set

For each product of low monomials, choose a block with enough unused degree, if one exists. On the agreement set, the majority in this block can be eliminated using the polynomial and strictly smaller modified degree.

noncomputable def Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.pivot {k m : ℕ} (d : ℕ) (a : Term k m) : Option (Fin k)

A block in which the low monomial has at least d degrees to spare.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.pivot d a = if h : ∃ (i : Fin k), (↑(a i).1).card + d ≤ m then some h.choose else none

def Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.Allowed {k m : ℕ} (d : ℕ) (a : Term k m) : Prop

The retained generators omit the majority in the chosen block.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.Allowed d a = ∀ (i : Fin k), Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.pivot d a = some i → (a i).2 = false

def Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.setFlag {k m : ℕ} (a : Term k m) (i : Fin k) (b : Bool) : Term k m

Change only the majority flag in a block.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.setFlag a i b = Function.update a i ((a i).1, b)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.pivot_congr {k m d : ℕ} {a b : Term k m} (h : ∀ (i : Fin k), (a i).1 = (b i).1) : pivot d a = pivot d b

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.setFlag_first {k m : ℕ} (a : Term k m) (i j : Fin k) (b : Bool) : (setFlag a i b j).1 = (a j).1

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.pivot_setFlag {k m d : ℕ} (a : Term k m) (i : Fin k) (b : Bool) : pivot d (setFlag a i b) = pivot d a

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.pivot_good {k m d : ℕ} {a : Term k m} {i : Fin k} (h : pivot d a = some i) : (↑(a i).1).card + d ≤ m

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.term_setFlag {k m : ℕ} (a : Term k m) (i : Fin k) (x : BlockCube k m) : termEval (setFlag a i true) x = termEval a x * majority (x i)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.setFlag_true_eq {k m : ℕ} {a : Term k m} {i : Fin k} (h : (a i).2 = true) : setFlag a i true = a

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.setFlag_twice {k m : ℕ} (a : Term k m) (i : Fin k) (b c : Bool) : setFlag (setFlag a i b) i c = setFlag a i c

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.allowed_setFlag_false {k m d : ℕ} {a : Term k m} {i : Fin k} (h : pivot d a = some i) : Allowed d (setFlag a i false)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.allowed_setFlag_other {k m d : ℕ} {a : Term k m} {i j : Fin k} (h : pivot d a = some i) (hne : j ≠ i) : Allowed d (setFlag (setFlag a i false) j true)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.weight_setFlag_drop {k m d : ℕ} {a : Term k m} {i : Fin k} (hi : pivot d a = some i) (hb : (a i).2 = true) : weight (setFlag a i false) + d < weight a

def Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.restrictTo {α : Type u_1} (E : Set α) : (α → ZMod 2) →ₗ[ZMod 2] ↑E → ZMod 2

Restriction of a function to a subset of its inputs.

Equations

• Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.restrictTo E = { toFun := fun (f : α → ZMod 2) (x : ↑E) => f ↑x, map_add' := ⋯, map_smul' := ⋯ }

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.agreement_span {k m d : ℕ} (p : MvPolynomial (Fin k × Fin (2 * m + 1)) (ZMod 2)) (hp : p.totalDegree ≤ d) (E : Set (BlockCube k m)) (hE : ∀ x ∈ E, polynomialEval p x = xorMajority x) : Submodule.span (ZMod 2) (Set.range fun (a : { a : Term k m // Allowed d a }) => (restrictTo E) (termEval ↑a)) = ⊤

The retained generators span all functions on any agreement set.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.agreement_card_le {k m d : ℕ} (p : MvPolynomial (Fin k × Fin (2 * m + 1)) (ZMod 2)) (hp : p.totalDegree ≤ d) (E : Set (BlockCube k m)) (hE : ∀ x ∈ E, polynomialEval p x = xorMajority x) : Nat.card ↑E ≤ Nat.card { a : Term k m // Allowed d a }

The agreement set has at most as many points as retained generators.