Semantic bridge for quadratic ANFs

The Reed--Muller argument is phrased recursively as a code. This file connects that code to canonical Boolean ANFs without enumerating functions. Only sparse evaluations and finite sums of monomials are used.

def UnrestrictedBooleanMul.N4.AffineCode.constantCoeff {n : ℕ} : AffineCode n → F₂

The constant coefficient of a recursively encoded affine polynomial.

Equations

• (UnrestrictedBooleanMul.N4.AffineCode.nil c).constantCoeff = c
• (a.cons head).constantCoeff = a.constantCoeff

def UnrestrictedBooleanMul.N4.AffineCode.linearCoeff {n : ℕ} : AffineCode n → Fin n → F₂

The linear coefficients of a recursively encoded affine polynomial.

Equations

• (UnrestrictedBooleanMul.N4.AffineCode.nil c).linearCoeff = fun (i : Fin 0) => i.elim0
• (a.cons head).linearCoeff = fun (i : Fin (n + 1)) => Fin.cases head a.linearCoeff i

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_eq_coeff_formula {n : ℕ} (a : AffineCode n) (x : Fin n → F₂) : a.eval x = a.constantCoeff + ∑ i : Fin n, a.linearCoeff i * x i

def UnrestrictedBooleanMul.N4.AffineCode.ofCoeffs (n : ℕ) : F₂ → (Fin n → F₂) → AffineCode n

Encode an affine polynomial from its constant and linear coefficients.

Equations

• UnrestrictedBooleanMul.N4.AffineCode.ofCoeffs 0 x✝ x_3 = UnrestrictedBooleanMul.N4.AffineCode.nil x✝
• UnrestrictedBooleanMul.N4.AffineCode.ofCoeffs n.succ x✝ l = (UnrestrictedBooleanMul.N4.AffineCode.ofCoeffs n x✝ fun (i : Fin n) => l i.succ).cons (l 0)

@[simp]

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_ofCoeffs (n : ℕ) (c : F₂) (l x : Fin n → F₂) : (ofCoeffs n c l).eval x = c + ∑ i : Fin n, l i * x i

noncomputable def UnrestrictedBooleanMul.N4.AffineCode.anf (a : AffineCode 8) : ANF 8

Convert an eight-variable affine code to its squarefree Boolean ANF.

Equations

• a.anf = a.constantCoeff • 1 + ∑ i : Fin 8, a.linearCoeff i • UnrestrictedBooleanMul.X i

theorem UnrestrictedBooleanMul.N4.AffineCode.anf_mem_affine (a : AffineCode 8) : a.anf ∈ affine 8

@[simp]

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_anf (a : AffineCode 8) (x : Fin 8 → F₂) : UnrestrictedBooleanMul.eval a.anf x = a.eval x

def UnrestrictedBooleanMul.N4.QuadraticSemantic (p : ANF 8) : Prop

The ANF agrees on every Boolean input with a quadratic code.

Equations

• UnrestrictedBooleanMul.N4.QuadraticSemantic p = ∃ (q : UnrestrictedBooleanMul.N4.QuadraticCode 8), ∀ (x : Fin 8 → UnrestrictedBooleanMul.F₂), q.eval x = UnrestrictedBooleanMul.eval p x

def UnrestrictedBooleanMul.N4.quadraticSemanticSpace : Submodule F₂ (ANF 8)

The subspace of ANFs representing quadratic Boolean functions.

Equations

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

theorem UnrestrictedBooleanMul.N4.affine_monomial_semantic (i : Fin 8) : X i ∈ quadraticSemanticSpace

theorem UnrestrictedBooleanMul.N4.one_semantic : 1 ∈ quadraticSemanticSpace

theorem UnrestrictedBooleanMul.N4.quadratic_monomial_semantic (i j : Fin 8) : X i * X j ∈ quadraticSemanticSpace

noncomputable def UnrestrictedBooleanMul.N4.lowReconstruct (p : ANF 8) : ANF 8

Retain only the coefficients of squarefree monomials of degree at most two.

Equations

• UnrestrictedBooleanMul.N4.lowReconstruct p = ∑ s : UnrestrictedBooleanMul.Monomial 8, if s.vars.card ≤ 2 then p.coeff s • UnrestrictedBooleanMul.monomial s.vars else 0

theorem UnrestrictedBooleanMul.N4.lowReconstruct_eq {p : ANF 8} (hp : DegreeLE 2 p) : lowReconstruct p = p

theorem UnrestrictedBooleanMul.N4.monomial_semantic_of_card_le_two (s : Monomial 8) (hs : s.vars.card ≤ 2) : monomial s.vars ∈ quadraticSemanticSpace

theorem UnrestrictedBooleanMul.N4.quadratic_semantic_of_degreeLE {p : ANF 8} (hp : DegreeLE 2 p) : p ∈ quadraticSemanticSpace

def UnrestrictedBooleanMul.N4.supportAssignment (t : Finset (Fin 8)) : Fin 8 → F₂

The Boolean assignment whose nonzero coordinates form the given finite set.

Equations

• UnrestrictedBooleanMul.N4.supportAssignment t i = if i ∈ t then 1 else 0

theorem UnrestrictedBooleanMul.N4.prod_supportAssignment (s t : Finset (Fin 8)) : ∏ i ∈ s, supportAssignment t i = if s ⊆ t then 1 else 0

theorem UnrestrictedBooleanMul.N4.eval_monomial_supportAssignment (s t : Finset (Fin 8)) : eval (monomial s) (supportAssignment t) = if s ⊆ t then 1 else 0

noncomputable def UnrestrictedBooleanMul.N4.sparseEvalMap (t : Finset (Fin 8)) : ANF 8 →ₗ[F₂] F₂

Evaluate an ANF on the indicator assignment of a finite set.

Equations

• UnrestrictedBooleanMul.N4.sparseEvalMap t = (UnrestrictedBooleanMul.evalHom (UnrestrictedBooleanMul.N4.supportAssignment t)).toLinearMap

noncomputable def UnrestrictedBooleanMul.N4.pairPolarMap (i j : Fin 8) : ANF 8 →ₗ[F₂] F₂

The second finite difference at zero in two coordinate directions.

Equations

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

def UnrestrictedBooleanMul.N4.pairCoeffMap (i j : Fin 8) : ANF 8 →ₗ[F₂] F₂

Extract the coefficient supported on the specified pair of variables.

Equations

• UnrestrictedBooleanMul.N4.pairCoeffMap i j = { toFun := fun (p : UnrestrictedBooleanMul.ANF 8) => p.coeff { vars := {i, j} }, map_add' := ⋯, map_smul' := ⋯ }

theorem UnrestrictedBooleanMul.N4.subset_pair_polar_identity (s : Finset (Fin 8)) (i j : Fin 8) (hij : i ≠ j) : ((((if s ⊆ ∅ then 1 else 0) + if s ⊆ {i} then 1 else 0) + if s ⊆ {j} then 1 else 0) + if s ⊆ {i, j} then 1 else 0) = if s = {i, j} then 1 else 0

theorem UnrestrictedBooleanMul.N4.sparseEvalMap_single (t : Finset (Fin 8)) (s : Monomial 8) (c : F₂) : (sparseEvalMap t) (MonoidAlgebra.single s c) = c * if s.vars ⊆ t then 1 else 0

theorem UnrestrictedBooleanMul.N4.pairPolarMap_eq_pairCoeffMap (i j : Fin 8) (hij : i ≠ j) : pairPolarMap i j = pairCoeffMap i j

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_congr_of_eval_eq {p q : ANF 8} (h : ∀ (x : Fin 8 → F₂), eval p x = eval q x) : anfTwoProjection p = anfTwoProjection q

def UnrestrictedBooleanMul.N4.quadraticOneCode : QuadraticCode 8

The constant-one quadratic code in eight variables.

Equations

• UnrestrictedBooleanMul.N4.quadraticOneCode = (UnrestrictedBooleanMul.N4.AffineCode.ofCoeffs 8 1 fun (x : Fin 8) => 0).toQuadratic

def UnrestrictedBooleanMul.N4.fiber00 (p q g : QuadraticCode 8) : QuadraticCode 8

The quadratic expression 1 + p + q + g used for the zero-zero fiber.

Equations

• UnrestrictedBooleanMul.N4.fiber00 p q g = ((UnrestrictedBooleanMul.N4.quadraticOneCode.add p).add q).add g

def UnrestrictedBooleanMul.N4.fiber01 (q g : QuadraticCode 8) : QuadraticCode 8

The quadratic expression q + g used for the zero-one fiber.

Equations

• UnrestrictedBooleanMul.N4.fiber01 q g = q.add g

def UnrestrictedBooleanMul.N4.fiber10 (p g : QuadraticCode 8) : QuadraticCode 8

The quadratic expression p + g used for the one-zero fiber.

Equations

• UnrestrictedBooleanMul.N4.fiber10 p g = p.add g

theorem UnrestrictedBooleanMul.N4.fiber_truth_identity (u v : F₂) : truthBit (1 + u + v + u * v) + truthBit (v + u * v) + truthBit (u + u * v) + truthBit (u * v) = 1

theorem UnrestrictedBooleanMul.N4.fiber_weights_sum (p q g : QuadraticCode 8) (hg : ∀ (x : Fin 8 → F₂), g.eval x = p.eval x * q.eval x) : truthWeight (fiber00 p q g).eval + truthWeight (fiber01 q g).eval + truthWeight (fiber10 p g).eval + truthWeight g.eval = 256

theorem UnrestrictedBooleanMul.N4.QuadraticCode.exists_eval_ne_zero_of_weight_pos {q : QuadraticCode 8} (h : 0 < truthWeight q.eval) : ∃ (x : Fin 8 → F₂), q.eval x ≠ 0

theorem UnrestrictedBooleanMul.N4.QuadraticCode.eval_eq_zero_of_weight_zero {q : QuadraticCode 8} (h : truthWeight q.eval = 0) (x : Fin 8 → F₂) : q.eval x = 0

theorem UnrestrictedBooleanMul.N4.quadratic_product_projection_alternative {p q g : ANF 8} (hgate : g = p * q) (hp : DegreeLE 2 p) (hq : DegreeLE 2 q) (hg : DegreeLE 2 g) : anfTwoProjection g ∈ Submodule.span F₂ {anfTwoProjection p, anfTwoProjection q} ∨ IsDecomposableTwo (anfTwoProjection g)