Algebraic quadratic lower-bound core

The classical quadratic lower bound is developed here without importing it as an assumption. The key certificate is a two-bit linear coloring of the rank-at-most-two Hankel graph. Every nonzero word in the explicit rank-two table has nonzero color, so a family with pairwise rank-two differences has at most four members. This replaces a search over quadratic circuits by a small linear-algebra certificate.

def UnrestrictedBooleanMul.N4.rankTwoColor : TargetCoeff →ₗ[F₂] Fin 2 → F₂

The two-bit certificate (c₀+c₂+c₅, c₁+c₃+c₆).

Equations

• UnrestrictedBooleanMul.N4.rankTwoColor = { toFun := fun (c : UnrestrictedBooleanMul.N4.TargetCoeff) => ![c 0 + c 2 + c 5, c 1 + c 3 + c 6], map_add' := ⋯, map_smul' := ⋯ }

theorem UnrestrictedBooleanMul.N4.rankTwoColor_eq_zero_iff {c : TargetCoeff} (hc : HankelRankLETwo c) : rankTwoColor c = 0 ↔ c = 0

The color kernel contains no nonzero rank-at-most-two Hankel word.

theorem UnrestrictedBooleanMul.N4.rankTwo_clique_card_le_four {ι : Type u_1} [Fintype ι] (c : ι → TargetCoeff) (hinj : Function.Injective c) (hpair : ∀ (i j : ι), HankelRankLETwo (c i + c j)) : Fintype.card ι ≤ 4

A family of distinct target words whose pairwise differences have Hankel rank at most two has cardinality at most four.

def UnrestrictedBooleanMul.N4.IsOuterTarget (c : TargetCoeff) : Prop

A target Hankel matrix is an outer product.

Equations

• UnrestrictedBooleanMul.N4.IsOuterTarget c = ∃ (a : Fin 4 → UnrestrictedBooleanMul.F₂) (b : Fin 4 → UnrestrictedBooleanMul.F₂), ∀ (i j : Fin 4), c ⟨↑i + ↑j, ⋯⟩ = a i * b j

theorem UnrestrictedBooleanMul.N4.decomposableTarget_outer {c : TargetCoeff} (hc : IsDecomposableTarget c) : IsOuterTarget c

theorem UnrestrictedBooleanMul.N4.outer_sum_rankTwo {c d : TargetCoeff} (hc : IsOuterTarget c) (hd : IsOuterTarget d) : HankelRankLETwo (c + d)

A sum of two outer-product target matrices has Hankel rank at most two.

theorem UnrestrictedBooleanMul.N4.sum_decomposable_rankTwo {c d : TargetCoeff} (hc : IsDecomposableTarget c) (hd : IsDecomposableTarget d) : HankelRankLETwo (c + d)

Sums of two arbitrary decomposable forms

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.Vec4 : Type

Four-dimensional vectors over the two-element field.

Equations

• UnrestrictedBooleanMul.N4.Vec4 = (Fin 4 → UnrestrictedBooleanMul.F₂)

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.Two4 : Type

Two-index coordinate arrays in four dimensions.

Equations

• UnrestrictedBooleanMul.N4.Two4 = (Fin 4 → Fin 4 → UnrestrictedBooleanMul.F₂)

def UnrestrictedBooleanMul.N4.vecWedge4 (u v : Vec4) : Two4

The exterior product of two four-dimensional vectors.

Equations

• UnrestrictedBooleanMul.N4.vecWedge4 u v i j = u i * v j + u j * v i

def UnrestrictedBooleanMul.N4.tripleWedge (u v x : Vec4) : Fin 4 → Fin 4 → Fin 4 → F₂

The exterior product of three four-dimensional vectors.

Equations

• UnrestrictedBooleanMul.N4.tripleWedge u v x i j k = x i * (u j * v k + u k * v j) + x j * (u i * v k + u k * v i) + x k * (u i * v j + u j * v i)

def UnrestrictedBooleanMul.N4.TripleWedgeZero (u v x : Vec4) : Prop

The exterior product of the three vectors vanishes.

Equations

• UnrestrictedBooleanMul.N4.TripleWedgeZero u v x = (UnrestrictedBooleanMul.N4.tripleWedge u v x = 0)

@[instance_reducible]

instance UnrestrictedBooleanMul.N4.instDecidableTripleWedgeZero (u v x : Vec4) : Decidable (TripleWedgeZero u v x)

Equations

• UnrestrictedBooleanMul.N4.instDecidableTripleWedgeZero u v x = { decide := decide (∀ a ∈ Finset.univ, UnrestrictedBooleanMul.N4.tripleWedge u v x a = 0 a), reflects_decide := ⋯ }

theorem UnrestrictedBooleanMul.N4.tripleWedgeZero_mem_span (u v x : Vec4) (huv : vecWedge4 u v ≠ 0) (hx : TripleWedgeZero u v x) : ∃ (a : F₂) (b : F₂), x = a • u + b • v

If u ∧ v is nonzero and x ∧ u ∧ v = 0, then x lies in the plane spanned by u,v. The proof chooses a nonzero 2 × 2 minor and solves the resulting two equations, so it works symbolically rather than by enumeration.

theorem UnrestrictedBooleanMul.N4.vecWedgeTwo_repeat (x y : Vec4) : (fun (i j k : Fin 4) => x i * vecWedge4 x y j k + x j * vecWedge4 x y i k + x k * vecWedge4 x y i j) = 0

def UnrestrictedBooleanMul.N4.IsOuterCross (u v : LinearForm) : Prop

The mixed input matrix is a single outer product.

Equations

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

theorem UnrestrictedBooleanMul.N4.outerCross_of_A_dependent {u v : LinearForm} (h : vecWedge4 (aPart u) (aPart v) = 0) : IsOuterCross u v

def UnrestrictedBooleanMul.N4.IsTwoOuterTarget (c : TargetCoeff) : Prop

The target Hankel matrix is a sum of two outer products.

Equations

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

theorem UnrestrictedBooleanMul.N4.twoOuter_rankTwo {c : TargetCoeff} (hc : IsTwoOuterTarget c) : HankelRankLETwo c

theorem UnrestrictedBooleanMul.N4.target_sum_two_decomposable_rankTwo {c : TargetCoeff} {u v x y : LinearForm} (h : targetTwo c = vectorWedge u v + vectorWedge x y) : HankelRankLETwo c

If a target two-form is the sum of two arbitrary decomposable two-forms, then its Hankel rank is at most two.

Eight decomposable forms cannot cover the target space

def UnrestrictedBooleanMul.N4.rationalPlaceCoeff : Fin 3 → TargetCoeff

The coefficient vectors for evaluations at zero, one, and infinity.

Equations

• UnrestrictedBooleanMul.N4.rationalPlaceCoeff = ![UnrestrictedBooleanMul.N4.rZeroCoeff, UnrestrictedBooleanMul.N4.rOneCoeff, UnrestrictedBooleanMul.N4.rInfinityCoeff]

theorem UnrestrictedBooleanMul.N4.rationalPlaceCoeff_injective : Function.Injective rationalPlaceCoeff

theorem UnrestrictedBooleanMul.N4.targetTwo_decomposableTarget {c : TargetCoeff} (h : IsDecomposableTwo (targetTwo c)) : IsDecomposableTarget c

theorem UnrestrictedBooleanMul.N4.target_decomposable_family_card_le_three {ι : Type u_1} [Fintype ι] (c : ι → TargetCoeff) (hinj : Function.Injective c) (hne : ∀ (i : ι), c i ≠ 0) (hdec : ∀ (i : ι), IsDecomposableTwo (targetTwo (c i))) : Fintype.card ι ≤ 3

theorem UnrestrictedBooleanMul.N4.add_mem_of_codim_one {V : Type u_1} [AddCommGroup V] [Module F₂ V] [FiniteDimensional F₂ V] {T Q : Submodule F₂ V} (hTQ : T ≤ Q) (hT : Module.finrank F₂ ↥T = 7) (hQ : Module.finrank F₂ ↥Q = 8) {x y : V} (hxQ : x ∈ Q) (hyQ : y ∈ Q) (hxT : x ∉ T) (hyT : y ∉ T) : x + y ∈ T

def UnrestrictedBooleanMul.N4.rationalPlaceTwoSpace : Submodule F₂ TwoForm

The span of the three rational-place target two-forms.

Equations

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

theorem UnrestrictedBooleanMul.N4.rationalPlaceTwoSpace_finrank_le_three : Module.finrank F₂ ↥rationalPlaceTwoSpace ≤ 3

theorem UnrestrictedBooleanMul.N4.decomposable_mem_rationalPlaceTwoSpace {q : TwoForm} (hq : q ∈ targetTwoSpace) (hdec : IsDecomposableTwo q) : q ∈ rationalPlaceTwoSpace

def UnrestrictedBooleanMul.N4.decomposableTwoSpan (q : Fin 8 → TwoForm) : Submodule F₂ TwoForm

The span of eight candidate two-form generators.

Equations

• UnrestrictedBooleanMul.N4.decomposableTwoSpan q = Submodule.span UnrestrictedBooleanMul.F₂ (Set.range q)

theorem UnrestrictedBooleanMul.N4.no_eight_decomposable_span (q : Fin 8 → TwoForm) (hdec : ∀ (i : Fin 8), IsDecomposableTwo (q i)) : ¬targetTwoSpace ≤ decomposableTwoSpan q

Eight decomposable alternating forms cannot span the seven-dimensional Hankel target. The proof splits by whether their span has dimension seven or eight. In codimension one, at most three forms lie in the target and at most four lie outside it; the latter bound is the two-bit Hankel coloring.