The degree-six seed-plane equation

The manuscript's degree-six identity is recorded through one squarefree coefficient. On the three rational-place quadratic directions this coefficient is their alternating determinant. Degree subadditivity removes every term containing an affine factor, so no large exterior-power coordinate space or circuit enumeration is needed.

def UnrestrictedBooleanMul.N4.sexticProbeSet : Finset (Fin 8)

A six-variable probe on which the three rational places have coefficient one in their exterior product: a₀ a₁ a₃ b₀ b₁ b₃.

Equations

• UnrestrictedBooleanMul.N4.sexticProbeSet = {0, 1, 3, 4, 5, 7}

def UnrestrictedBooleanMul.N4.anfSexticProbe : ANF 8 →ₗ[F₂] F₂

Extract the designated degree-six coefficient of an ANF.

Equations

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

@[simp]

theorem UnrestrictedBooleanMul.N4.anfSexticProbe_monomial (s : Finset (Fin 8)) : anfSexticProbe (monomial s) = if s = sexticProbeSet then 1 else 0

@[simp]

theorem UnrestrictedBooleanMul.N4.sexticProbeSet_card : sexticProbeSet.card = 6

theorem UnrestrictedBooleanMul.N4.anfSexticProbe_eq_zero_of_degreeLE_five {p : ANF 8} (hp : DegreeLE 5 p) : anfSexticProbe p = 0

theorem UnrestrictedBooleanMul.N4.degreeLE_one_affineANF (a : F₂) (ell : LinearForm) : DegreeLE 1 (affineANF a ell)

theorem UnrestrictedBooleanMul.N4.degreeLE_two_rationalANF (alpha : Fin 3 → F₂) : DegreeLE 2 (rationalANF alpha)

theorem UnrestrictedBooleanMul.N4.degreeLE_two_targetANF (c : TargetCoeff) : DegreeLE 2 (targetANF c)

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

def UnrestrictedBooleanMul.N4.rationalTripleDet (alpha beta delta : Fin 3 → F₂) : F₂

The characteristic-two determinant of three rational-place coefficient vectors.

Equations

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

theorem UnrestrictedBooleanMul.N4.anfSexticProbe_rational_triple (alpha beta delta : Fin 3 → F₂) : anfSexticProbe (rationalANF alpha * rationalANF beta * rationalANF delta) = rationalTripleDet alpha beta delta

The selected sextic coefficient of three rational quadratics is exactly the determinant of their three coefficient vectors.

theorem UnrestrictedBooleanMul.N4.anfSexticProbe_lowProduct_mul_lowFactor (a b c : F₂) (ell m n : LinearForm) (alpha beta delta : Fin 3 → F₂) : anfSexticProbe ((affineANF a ell + rationalANF alpha) * (affineANF b m + rationalANF beta) * (affineANF c n + rationalANF delta)) = rationalTripleDet alpha beta delta

In a product of three rational-low factors, the sextic probe sees only the three rational quadratic parts.

theorem UnrestrictedBooleanMul.N4.rationalTripleDet_eq_zero_of_seedUsing_target {g correction factor target : ANF 8} {a b c : F₂} {ell m n : LinearForm} {alpha beta delta : Fin 3 → F₂} (hg : g = (affineANF a ell + rationalANF alpha) * (affineANF b m + rationalANF beta)) (hcorrection : correction ∈ rationalLowSpace) (hfactor : factor = affineANF c n + rationalANF delta) (htarget : target = (g + correction) * factor) (htargetAmbient : target ∈ targetAmbient 8 (mulTarget 4)) : rationalTripleDet alpha beta delta = 0

The degree-six part of a seed-using target equation forces the rational quadratic part of the feedback factor into the seed coefficient plane. This lemma records the determinant equation; the finite three-dimensional plane criterion below turns it into explicit span membership.

def UnrestrictedBooleanMul.N4.InRationalCoeffPlane (alpha beta delta : Fin 3 → F₂) : Prop

The third rational coefficient vector belongs to the span of the first two.

Equations

• UnrestrictedBooleanMul.N4.InRationalCoeffPlane alpha beta delta = ∃ (p : UnrestrictedBooleanMul.F₂) (q : UnrestrictedBooleanMul.F₂), delta = p • alpha + q • beta

@[instance_reducible]

instance UnrestrictedBooleanMul.N4.instDecidableInRationalCoeffPlane (alpha beta delta : Fin 3 → F₂) : Decidable (InRationalCoeffPlane alpha beta delta)

Equations

• UnrestrictedBooleanMul.N4.instDecidableInRationalCoeffPlane alpha beta delta = id inferInstance

theorem UnrestrictedBooleanMul.N4.rationalTripleDet_zero_mem_plane (alpha beta delta : Fin 3 → F₂) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hab : alpha ≠ beta) (hdet : rationalTripleDet alpha beta delta = 0) : InRationalCoeffPlane alpha beta delta

In F₂³, a zero determinant against two independent vectors is equivalent to membership in their plane.