The degree-two Reed--Muller minimum word

This file supplies the algebraic flattening ingredient for quadratic Boolean circuits. Quadratic functions are stored recursively as

q(x₀,x') = q₀(x') + x₀ a(x'),

where a is affine. The minimum-weight proof is therefore an induction on variables, not an enumeration of eight-variable truth tables.

inductive UnrestrictedBooleanMul.N4.AffineCode : ℕ → Type

Recursive squarefree encoding of an affine polynomial over the two-element field.

• nil (c : F₂) : AffineCode 0
• cons {n : ℕ} (tail : AffineCode n) (head : F₂) : AffineCode (n + 1)

@[instance_reducible]

instance UnrestrictedBooleanMul.N4.instDecidableEqAffineCode {a✝ : ℕ} : DecidableEq (AffineCode a✝)

Equations

• UnrestrictedBooleanMul.N4.instDecidableEqAffineCode = UnrestrictedBooleanMul.N4.instDecidableEqAffineCode.decEq

def UnrestrictedBooleanMul.N4.instDecidableEqAffineCode.decEq {a✝ : ℕ} (x✝ x✝¹ : AffineCode a✝) : Decidable (x✝ = x✝¹)

Equations

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

inductive UnrestrictedBooleanMul.N4.QuadraticCode : ℕ → Type

Recursive squarefree encoding of a polynomial of degree at most two.

• nil (c : F₂) : QuadraticCode 0
• cons {n : ℕ} (tail : QuadraticCode n) (cross : AffineCode n) : QuadraticCode (n + 1)

def UnrestrictedBooleanMul.N4.instDecidableEqQuadraticCode.decEq {a✝ : ℕ} (x✝ x✝¹ : QuadraticCode a✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance UnrestrictedBooleanMul.N4.instDecidableEqQuadraticCode {a✝ : ℕ} : DecidableEq (QuadraticCode a✝)

Equations

• UnrestrictedBooleanMul.N4.instDecidableEqQuadraticCode = UnrestrictedBooleanMul.N4.instDecidableEqQuadraticCode.decEq

def UnrestrictedBooleanMul.N4.assignmentTail {n : ℕ} (x : Fin (n + 1) → F₂) : Fin n → F₂

Remove the first coordinate of a Boolean assignment.

Equations

• UnrestrictedBooleanMul.N4.assignmentTail x i = x i.succ

def UnrestrictedBooleanMul.N4.assignmentCons {n : ℕ} (b : F₂) (x : Fin n → F₂) : Fin (n + 1) → F₂

Prepend one field element to a Boolean assignment.

Equations

• UnrestrictedBooleanMul.N4.assignmentCons b x i = Fin.cases b x i

@[simp]

theorem UnrestrictedBooleanMul.N4.assignmentCons_zero {n : ℕ} (b : F₂) (x : Fin n → F₂) : assignmentCons b x 0 = b

@[simp]

theorem UnrestrictedBooleanMul.N4.assignmentCons_succ {n : ℕ} (b : F₂) (x : Fin n → F₂) (i : Fin n) : assignmentCons b x i.succ = x i

@[simp]

theorem UnrestrictedBooleanMul.N4.assignmentTail_cons {n : ℕ} (b : F₂) (x : Fin n → F₂) : assignmentTail (assignmentCons b x) = x

def UnrestrictedBooleanMul.N4.assignmentEquiv (n : ℕ) : (Fin (n + 1) → F₂) ≃ F₂ × (Fin n → F₂)

Split a Boolean assignment into its first coordinate and its tail.

Equations

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

def UnrestrictedBooleanMul.N4.AffineCode.eval {n : ℕ} : AffineCode n → (Fin n → F₂) → F₂

Evaluate a recursively encoded affine polynomial on a Boolean assignment.

Equations

• (UnrestrictedBooleanMul.N4.AffineCode.nil c).eval x_3 = c
• (tail.cons head).eval x_3 = tail.eval (UnrestrictedBooleanMul.N4.assignmentTail x_3) + x_3 0 * head

def UnrestrictedBooleanMul.N4.QuadraticCode.eval {n : ℕ} : QuadraticCode n → (Fin n → F₂) → F₂

Evaluate a recursively encoded quadratic polynomial on a Boolean assignment.

Equations

• (UnrestrictedBooleanMul.N4.QuadraticCode.nil c).eval x_3 = c
• (tail.cons cross).eval x_3 = tail.eval (UnrestrictedBooleanMul.N4.assignmentTail x_3) + x_3 0 * cross.eval (UnrestrictedBooleanMul.N4.assignmentTail x_3)

@[simp]

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_nil (c : F₂) (x : Fin 0 → F₂) : (nil c).eval x = c

@[simp]

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_cons {n : ℕ} (a : AffineCode n) (d b : F₂) (x : Fin n → F₂) : (a.cons d).eval (assignmentCons b x) = a.eval x + b * d

@[simp]

theorem UnrestrictedBooleanMul.N4.QuadraticCode.eval_nil (c : F₂) (x : Fin 0 → F₂) : (nil c).eval x = c

@[simp]

theorem UnrestrictedBooleanMul.N4.QuadraticCode.eval_cons {n : ℕ} (q : QuadraticCode n) (a : AffineCode n) (b : F₂) (x : Fin n → F₂) : (q.cons a).eval (assignmentCons b x) = q.eval x + b * a.eval x

def UnrestrictedBooleanMul.N4.truthBit (a : F₂) : ℕ

The natural-number indicator of a nonzero field element.

Equations

• UnrestrictedBooleanMul.N4.truthBit a = if a = 0 then 0 else 1

def UnrestrictedBooleanMul.N4.truthWeight {X : Type u_1} [Fintype X] (f : X → F₂) : ℕ

The number of inputs on which a field-valued function is nonzero.

Equations

• UnrestrictedBooleanMul.N4.truthWeight f = ∑ x : X, UnrestrictedBooleanMul.N4.truthBit (f x)

theorem UnrestrictedBooleanMul.N4.truthBit_zero : truthBit 0 = 0

theorem UnrestrictedBooleanMul.N4.truthBit_one : truthBit 1 = 1

theorem UnrestrictedBooleanMul.N4.truthWeight_assignment_split {n : ℕ} (f : (Fin (n + 1) → F₂) → F₂) : truthWeight f = (truthWeight fun (x : Fin n → F₂) => f (assignmentCons 0 x)) + truthWeight fun (x : Fin n → F₂) => f (assignmentCons 1 x)

def UnrestrictedBooleanMul.N4.AffineCode.zero (n : ℕ) : AffineCode n

The recursively encoded zero affine polynomial.

Equations

• UnrestrictedBooleanMul.N4.AffineCode.zero 0 = UnrestrictedBooleanMul.N4.AffineCode.nil 0
• UnrestrictedBooleanMul.N4.AffineCode.zero n.succ = (UnrestrictedBooleanMul.N4.AffineCode.zero n).cons 0

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

The recursively encoded constant affine polynomial.

Equations

• UnrestrictedBooleanMul.N4.AffineCode.const 0 x✝ = UnrestrictedBooleanMul.N4.AffineCode.nil x✝
• UnrestrictedBooleanMul.N4.AffineCode.const n.succ x✝ = (UnrestrictedBooleanMul.N4.AffineCode.const n x✝).cons 0

def UnrestrictedBooleanMul.N4.AffineCode.add {n : ℕ} : AffineCode n → AffineCode n → AffineCode n

Coefficientwise addition of recursively encoded affine polynomials.

Equations

• (UnrestrictedBooleanMul.N4.AffineCode.nil a).add (UnrestrictedBooleanMul.N4.AffineCode.nil b) = UnrestrictedBooleanMul.N4.AffineCode.nil (a + b)
• (a.cons x_3).add (b.cons y) = (a.add b).cons (x_3 + y)

def UnrestrictedBooleanMul.N4.QuadraticCode.zero (n : ℕ) : QuadraticCode n

The recursively encoded zero quadratic polynomial.

Equations

• UnrestrictedBooleanMul.N4.QuadraticCode.zero 0 = UnrestrictedBooleanMul.N4.QuadraticCode.nil 0
• UnrestrictedBooleanMul.N4.QuadraticCode.zero n.succ = (UnrestrictedBooleanMul.N4.QuadraticCode.zero n).cons (UnrestrictedBooleanMul.N4.AffineCode.zero n)

def UnrestrictedBooleanMul.N4.QuadraticCode.add {n : ℕ} : QuadraticCode n → QuadraticCode n → QuadraticCode n

Coefficientwise addition of recursively encoded quadratic polynomials.

Equations

• (UnrestrictedBooleanMul.N4.QuadraticCode.nil a).add (UnrestrictedBooleanMul.N4.QuadraticCode.nil b) = UnrestrictedBooleanMul.N4.QuadraticCode.nil (a + b)
• (q.cons a).add (r.cons b) = (q.add r).cons (a.add b)

def UnrestrictedBooleanMul.N4.AffineCode.toQuadratic {n : ℕ} : AffineCode n → QuadraticCode n

View an affine polynomial as a quadratic polynomial.

Equations

• (UnrestrictedBooleanMul.N4.AffineCode.nil a).toQuadratic = UnrestrictedBooleanMul.N4.QuadraticCode.nil a
• (a.cons d).toQuadratic = a.toQuadratic.cons (UnrestrictedBooleanMul.N4.AffineCode.const n d)

@[simp]

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_zero {n : ℕ} (x : Fin n → F₂) : (zero n).eval x = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_const {n : ℕ} (c : F₂) (x : Fin n → F₂) : (const n c).eval x = c

@[simp]

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_add {n : ℕ} (a b : AffineCode n) (x : Fin n → F₂) : (a.add b).eval x = a.eval x + b.eval x

@[simp]

theorem UnrestrictedBooleanMul.N4.QuadraticCode.eval_zero {n : ℕ} (x : Fin n → F₂) : (zero n).eval x = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.QuadraticCode.eval_add {n : ℕ} (q r : QuadraticCode n) (x : Fin n → F₂) : (q.add r).eval x = q.eval x + r.eval x

@[simp]

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_toQuadratic {n : ℕ} (a : AffineCode n) (x : Fin n → F₂) : a.toQuadratic.eval x = a.eval x

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_injective {n : ℕ} : Function.Injective fun (a : AffineCode n) => a.eval

def UnrestrictedBooleanMul.N4.AffineCode.Nonconstant {n : ℕ} : AffineCode n → Prop

At least one linear coefficient of the affine code is nonzero.

Equations

• x_2.Nonconstant = False
• (a.cons d).Nonconstant = (a.Nonconstant ∨ d ≠ 0)

theorem UnrestrictedBooleanMul.N4.AffineCode.exists_eval_zero_of_nonconstant {n : ℕ} {a : AffineCode n} (ha : a.Nonconstant) : ∃ (x : Fin n → F₂), a.eval x = 0

theorem UnrestrictedBooleanMul.N4.AffineCode.weight_nonconstant {n : ℕ} {a : AffineCode n} (ha : a.Nonconstant) : truthWeight a.eval = 2 ^ (n - 1)

theorem UnrestrictedBooleanMul.N4.truthWeight_pos_of_exists {X : Type u_1} [Fintype X] {f : X → F₂} (h : ∃ (x : X), f x ≠ 0) : 0 < truthWeight f

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_eq_of_not_nonconstant {n : ℕ} {a : AffineCode n} (ha : ¬a.Nonconstant) (x y : Fin n → F₂) : a.eval x = a.eval y

theorem UnrestrictedBooleanMul.N4.AffineCode.weight_nonzero_lower {n : ℕ} {a : AffineCode n} (ha : ∃ (x : Fin n → F₂), a.eval x ≠ 0) : 2 ^ (n - 1) ≤ truthWeight a.eval

theorem UnrestrictedBooleanMul.N4.f2_eq_iff_add_eq_zero (u v : F₂) : u = v ↔ u + v = 0

theorem UnrestrictedBooleanMul.N4.AffineCode.eq_zero_or_eq_of_vanishes {n : ℕ} {a c : AffineCode n} (ha : a.Nonconstant) (h : ∀ (x : Fin n → F₂), a.eval x = 0 → c.eval x = 0) : c = zero n ∨ c = a

theorem UnrestrictedBooleanMul.N4.QuadraticCode.factor_of_vanishes {n : ℕ} {a : AffineCode n} (ha : a.Nonconstant) {q : QuadraticCode n} (h : ∀ (x : Fin n → F₂), a.eval x = 0 → q.eval x = 0) : ∃ (b : AffineCode n), ∀ (x : Fin n → F₂), q.eval x = a.eval x * b.eval x

theorem UnrestrictedBooleanMul.N4.truthBit_pair_identity (u v : F₂) : truthBit u + truthBit (u + v) = truthBit v + 2 * if v = 0 then truthBit u else 0

theorem UnrestrictedBooleanMul.N4.truthWeight_pair_identity {X : Type u_1} [Fintype X] (f g : X → F₂) : (truthWeight f + truthWeight fun (x : X) => f x + g x) = truthWeight g + 2 * ∑ x : X, if g x = 0 then truthBit (f x) else 0

theorem UnrestrictedBooleanMul.N4.truthWeight_pair_ge {X : Type u_1} [Fintype X] (f g : X → F₂) : truthWeight g ≤ truthWeight f + truthWeight fun (x : X) => f x + g x

theorem UnrestrictedBooleanMul.N4.vanishes_of_truthWeight_pair_eq {X : Type u_1} [Fintype X] {f g : X → F₂} (h : (truthWeight f + truthWeight fun (x : X) => f x + g x) = truthWeight g) (x : X) : g x = 0 → f x = 0

theorem UnrestrictedBooleanMul.N4.QuadraticCode.minimum_weight {n : ℕ} (hn : 2 ≤ n) {q : QuadraticCode n} (hq : ∃ (x : Fin n → F₂), q.eval x ≠ 0) : 2 ^ (n - 2) ≤ truthWeight q.eval

theorem UnrestrictedBooleanMul.N4.AffineCode.weight_eq_full_of_not_nonconstant {n : ℕ} {a : AffineCode n} (hnc : ¬a.Nonconstant) (ha : ∃ (x : Fin n → F₂), a.eval x ≠ 0) : truthWeight a.eval = 2 ^ n

theorem UnrestrictedBooleanMul.N4.QuadraticCode.minimum_word_factor {n : ℕ} (hn : 2 ≤ n) {q : QuadraticCode n} (hq : ∃ (x : Fin n → F₂), q.eval x ≠ 0) (hweight : truthWeight q.eval = 2 ^ (n - 2)) : ∃ (a : AffineCode n) (b : AffineCode n), ∀ (x : Fin n → F₂), q.eval x = a.eval x * b.eval x

theorem UnrestrictedBooleanMul.N4.QuadraticCode.eval_injective {n : ℕ} : Function.Injective fun (q : QuadraticCode n) => q.eval

def UnrestrictedBooleanMul.N4.AffineCode.smul (k : F₂) {n : ℕ} : AffineCode n → AffineCode n

Multiply every affine coefficient by a field scalar.

Equations

• UnrestrictedBooleanMul.N4.AffineCode.smul k (UnrestrictedBooleanMul.N4.AffineCode.nil a) = UnrestrictedBooleanMul.N4.AffineCode.nil (k * a)
• UnrestrictedBooleanMul.N4.AffineCode.smul k (a.cons d) = (UnrestrictedBooleanMul.N4.AffineCode.smul k a).cons (k * d)

def UnrestrictedBooleanMul.N4.QuadraticCode.smul (k : F₂) {n : ℕ} : QuadraticCode n → QuadraticCode n

Multiply every quadratic coefficient by a field scalar.

Equations

• UnrestrictedBooleanMul.N4.QuadraticCode.smul k (UnrestrictedBooleanMul.N4.QuadraticCode.nil c) = UnrestrictedBooleanMul.N4.QuadraticCode.nil (k * c)
• UnrestrictedBooleanMul.N4.QuadraticCode.smul k (q.cons a) = (UnrestrictedBooleanMul.N4.QuadraticCode.smul k q).cons (UnrestrictedBooleanMul.N4.AffineCode.smul k a)

@[simp]

theorem UnrestrictedBooleanMul.N4.AffineCode.eval_smul {n : ℕ} (k : F₂) (a : AffineCode n) (x : Fin n → F₂) : (smul k a).eval x = k * a.eval x

@[simp]

theorem UnrestrictedBooleanMul.N4.QuadraticCode.eval_smul {n : ℕ} (k : F₂) (q : QuadraticCode n) (x : Fin n → F₂) : (smul k q).eval x = k * q.eval x

theorem UnrestrictedBooleanMul.N4.f2_mul_self (u : F₂) : u * u = u

def UnrestrictedBooleanMul.N4.QuadraticCode.mulAffine {n : ℕ} : AffineCode n → AffineCode n → QuadraticCode n

Encode the Boolean product of two affine polynomials as a quadratic polynomial.

Equations

• One or more equations did not get rendered due to their size.
• UnrestrictedBooleanMul.N4.QuadraticCode.mulAffine (UnrestrictedBooleanMul.N4.AffineCode.nil a) (UnrestrictedBooleanMul.N4.AffineCode.nil b) = UnrestrictedBooleanMul.N4.QuadraticCode.nil (a * b)

@[simp]

theorem UnrestrictedBooleanMul.N4.QuadraticCode.eval_mulAffine {n : ℕ} (a b : AffineCode n) (x : Fin n → F₂) : (mulAffine a b).eval x = a.eval x * b.eval x