Homogeneous degree and seed predicates

The Boolean ANF multiplication lowers degree when variables repeat, so the formal development records degree by coefficients rather than by a polynomial quotient API. This file supplies the high-part predicates used by the seed and defect arguments.

def UnrestrictedBooleanMul.N4.homogeneousPart {m : ℕ} (d : ℕ) (p : ANF m) : ANF m

Keep exactly the monomials of cardinality d.

Equations

• UnrestrictedBooleanMul.N4.homogeneousPart d p = MonoidAlgebra.ofCoeff (Finsupp.filter (fun (s : UnrestrictedBooleanMul.Monomial m) => s.vars.card = d) p.coeff)

@[simp]

theorem UnrestrictedBooleanMul.N4.homogeneousPart_coeff {m d : ℕ} (p : ANF m) (s : Monomial m) : (homogeneousPart d p).coeff s = if s.vars.card = d then p.coeff s else 0

def UnrestrictedBooleanMul.N4.homogeneousProjection {m : ℕ} (d : ℕ) : ANF m →ₗ[F₂] ANF m

Linear projection onto the squarefree monomials of exactly the specified degree.

Equations

• UnrestrictedBooleanMul.N4.homogeneousProjection d = { toFun := UnrestrictedBooleanMul.N4.homogeneousPart d, map_add' := ⋯, map_smul' := ⋯ }

def UnrestrictedBooleanMul.N4.DegreeLE {m : ℕ} (d : ℕ) (p : ANF m) : Prop

The ANF has no monomial above degree d.

Equations

• UnrestrictedBooleanMul.N4.DegreeLE d p = ∀ (s : UnrestrictedBooleanMul.Monomial m), d < s.vars.card → p.coeff s = 0

theorem UnrestrictedBooleanMul.N4.DegreeLE.mul {m d e : ℕ} {p q : ANF m} (hp : DegreeLE d p) (hq : DegreeLE e q) : DegreeLE (d + e) (p * q)

Boolean ANF degree is subadditive under multiplication. This uses only the support inclusion for monoid algebras and card (s ∪ t) ≤ card s + card t; repeated Boolean variables can lower, but never raise, the degree.

theorem UnrestrictedBooleanMul.N4.DegreeLE.mono {m d e : ℕ} {p : ANF m} (hp : DegreeLE d p) (hde : d ≤ e) : DegreeLE e p

def UnrestrictedBooleanMul.N4.HasNonzeroHigh {m : ℕ} (p : ANF m) : Prop

There is a genuinely high monomial (degree at least three).

Equations

• UnrestrictedBooleanMul.N4.HasNonzeroHigh p = ∃ (s : UnrestrictedBooleanMul.Monomial m), 3 ≤ s.vars.card ∧ p.coeff s ≠ 0

def UnrestrictedBooleanMul.N4.QuarticFree {m : ℕ} (p : ANF m) : Prop

The degree-four homogeneous component vanishes.

Equations

• UnrestrictedBooleanMul.N4.QuarticFree p = (UnrestrictedBooleanMul.N4.homogeneousPart 4 p = 0)

def UnrestrictedBooleanMul.N4.IsCubicSeed {m : ℕ} (p : ANF m) : Prop

A seed whose only possible nonzero high component is cubic.

Equations

• UnrestrictedBooleanMul.N4.IsCubicSeed p = (UnrestrictedBooleanMul.N4.HasNonzeroHigh p ∧ UnrestrictedBooleanMul.N4.DegreeLE 3 p)

def UnrestrictedBooleanMul.N4.SeedHighNonzero (C : Circuit 8 8) : Prop

The fourth gate has a nonzero component of degree greater than two.

Equations

• UnrestrictedBooleanMul.N4.SeedHighNonzero C = UnrestrictedBooleanMul.N4.HasNonzeroHigh (C.gate 3)

def UnrestrictedBooleanMul.N4.SeedQuarticFree (C : Circuit 8 8) : Prop

The fourth gate has no degree-four homogeneous component.

Equations

• UnrestrictedBooleanMul.N4.SeedQuarticFree C = UnrestrictedBooleanMul.N4.QuarticFree (C.gate 3)

def UnrestrictedBooleanMul.N4.CubicSeedState (C : Circuit 8 8) : Prop

The fourth gate is a cubic seed.

Equations

• UnrestrictedBooleanMul.N4.CubicSeedState C = UnrestrictedBooleanMul.N4.IsCubicSeed (C.gate 3)

def UnrestrictedBooleanMul.N4.quadraticANFSpace (m : ℕ) : Submodule F₂ (ANF m)

The linear subspace of Boolean ANFs of degree at most two.

Equations

• UnrestrictedBooleanMul.N4.quadraticANFSpace m = { carrier := {p : UnrestrictedBooleanMul.ANF m | UnrestrictedBooleanMul.N4.DegreeLE 2 p}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem UnrestrictedBooleanMul.N4.mem_quadraticANFSpace_iff {m : ℕ} (p : ANF m) : p ∈ quadraticANFSpace m ↔ ¬HasNonzeroHigh p

theorem UnrestrictedBooleanMul.N4.affine_coeff_zero_of_two_le {m : ℕ} {p : ANF m} (hp : p ∈ affine m) (s : Monomial m) (hs : 2 ≤ s.vars.card) : p.coeff s = 0

theorem UnrestrictedBooleanMul.N4.affine_coeff_zero_of_three_le {m : ℕ} {p : ANF m} (hp : p ∈ affine m) (s : Monomial m) (hs : 3 ≤ s.vars.card) : p.coeff s = 0

theorem UnrestrictedBooleanMul.N4.aVar_ne_bVar_index (i j : Fin 4) : ⟨↑i, ⋯⟩ ≠ ⟨4 + ↑j, ⋯⟩

theorem UnrestrictedBooleanMul.N4.coeff_aVar_mul_bVar_zero_of_three_le (i j : Fin 4) (s : Monomial 8) (hs : 3 ≤ s.vars.card) : (aVar 4 i * bVar 4 j).coeff s = 0

theorem UnrestrictedBooleanMul.N4.Mul_four_coeff_zero_of_three_le (i : Fin 7) (s : Monomial 8) (hs : 3 ≤ s.vars.card) : (Mul 4 i).coeff s = 0

theorem UnrestrictedBooleanMul.N4.mulTarget_coeff_zero_of_three_le {p : ANF 8} (hp : p ∈ mulTarget 4) (s : Monomial 8) (hs : 3 ≤ s.vars.card) : p.coeff s = 0

theorem UnrestrictedBooleanMul.N4.targetAmbient_coeff_zero_of_three_le {p : ANF 8} (hp : p ∈ targetAmbient 8 (mulTarget 4)) (s : Monomial 8) (hs : 3 ≤ s.vars.card) : p.coeff s = 0

theorem UnrestrictedBooleanMul.N4.targetAmbient_le_quadraticANFSpace : targetAmbient 8 (mulTarget 4) ≤ quadraticANFSpace 8

theorem UnrestrictedBooleanMul.N4.affine_le_quadraticANFSpace {m : ℕ} : affine m ≤ quadraticANFSpace m

theorem UnrestrictedBooleanMul.N4.wireSpace_le_quadratic_of_prefix {m r j : ℕ} (g : Fin r → ANF m) (hgate : ∀ (i : Fin r), ↑i < j → g i ∈ quadraticANFSpace m) : wireSpace g j ≤ quadraticANFSpace m

theorem UnrestrictedBooleanMul.N4.inf_unchanged_of_first_high (V A : Submodule F₂ (ANF 8)) (g : ANF 8) (hV : V ≤ quadraticANFSpace 8) (hA : A ≤ quadraticANFSpace 8) (hg : g ∉ quadraticANFSpace 8) : (V ⊔ F₂ ∙ g) ⊓ A = V ⊓ A

Adjoining a first high-degree vector to an entirely quadratic state cannot create a new direction in a quadratic ambient target.

theorem UnrestrictedBooleanMul.N4.first_high_gate_not_useful (C : Circuit 8 8) (j : Fin 8) (hprev : ∀ (i : Fin 8), ↑i < ↑j → C.gate i ∈ quadraticANFSpace 8) (hhigh : HasNonzeroHigh (C.gate j)) : ¬UsefulAt C (mulTarget 4) j

theorem UnrestrictedBooleanMul.N4.normalized_all_gates_quadratic_of_seed_not_high {C : Circuit 8 8} (hNorm : NormalizedEight C) (hseed : ¬SeedHighNonzero C) (i : Fin 8) : C.gate i ∈ quadraticANFSpace 8

If the normalized seed were quadratic, every later gate would remain quadratic: the first high suffix gate would be a forbidden second non-useful gate.

theorem UnrestrictedBooleanMul.N4.not_high_of_mem_targetAmbient {p : ANF 8} (hp : p ∈ targetAmbient 8 (mulTarget 4)) : ¬HasNonzeroHigh p

theorem UnrestrictedBooleanMul.N4.finalWire_le_targetAmbient_of_defect_zero (C : Circuit 8 8) (hdef : flagDefectRank C.finalWire (mulTarget 4) = 0) : C.finalWire ≤ targetAmbient 8 (mulTarget 4)

Zero defect means the entire final wire space lies in Aff + T; in particular every gate output has degree at most two.

theorem UnrestrictedBooleanMul.N4.gate_not_high_of_defect_zero (C : Circuit 8 8) (hdef : flagDefectRank C.finalWire (mulTarget 4) = 0) (i : Fin 8) : ¬HasNonzeroHigh (C.gate i)