Homogeneous ANF/exterior bridge

The exterior calculations are connected to Boolean ANFs through the degree three and degree four coefficient projections below. Only fixed products of an input variable with one of the three rational places (and pairs of those places) require coordinate normalization.

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

Cubic coefficients as a three-form array, with repeated-index coordinates zero.

Equations

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

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

Quartic coefficients as a four-form array, with repeated-index coordinates zero.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.linearANF (ell : LinearForm) : ANF 8

The Boolean ANF of the given linear form.

Equations

• UnrestrictedBooleanMul.N4.linearANF ell = ∑ i : Fin 8, ell i • UnrestrictedBooleanMul.X i

noncomputable def UnrestrictedBooleanMul.N4.affineANF (a : F₂) (ell : LinearForm) : ANF 8

The Boolean ANF with the given constant and linear parts.

Equations

• UnrestrictedBooleanMul.N4.affineANF a ell = a • 1 + UnrestrictedBooleanMul.N4.linearANF ell

noncomputable def UnrestrictedBooleanMul.N4.rationalANF (α : Fin 3 → F₂) : ANF 8

The target ANF of a linear combination of rational-place evaluations.

Equations

• UnrestrictedBooleanMul.N4.rationalANF α = UnrestrictedBooleanMul.N4.targetANF (UnrestrictedBooleanMul.N4.rationalCoeffRep α)

theorem UnrestrictedBooleanMul.N4.rationalANF_eq_sum (α : Fin 3 → F₂) : rationalANF α = ∑ θ : Fin 3, α θ • targetANF (rationalPlaceCoeff θ)

def UnrestrictedBooleanMul.N4.hankelIndex (i j : Fin 4) : Fin 7

The product coefficient index corresponding to two input coefficient indices.

Equations

• UnrestrictedBooleanMul.N4.hankelIndex i j = ⟨↑i + ↑j, ⋯⟩

def UnrestrictedBooleanMul.N4.targetPair (i j : Fin 4) : Finset (Fin 8)

The squarefree mixed monomial for one coefficient from each input polynomial.

Equations

• UnrestrictedBooleanMul.N4.targetPair i j = {UnrestrictedBooleanMul.N4.aCoord i, UnrestrictedBooleanMul.N4.bCoord j}

theorem UnrestrictedBooleanMul.N4.targetANF_eq_double_sum (c : TargetCoeff) : targetANF c = ∑ i : Fin 4, ∑ j : Fin 4, c (hankelIndex i j) • monomial (targetPair i j)

The target Hankel form as its sixteen cross monomials.

theorem UnrestrictedBooleanMul.N4.coeff_targetANF_mul_targetANF (c d : TargetCoeff) (s : Finset (Fin 8)) : (targetANF c * targetANF d).coeff { vars := s } = ∑ u : Fin 4, ∑ v : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4, c (hankelIndex i j) * d (hankelIndex u v) * if targetPair i j ∪ targetPair u v = s then 1 else 0

A target-product coefficient is a finite convolution of its mixed monomials.

def UnrestrictedBooleanMul.N4.monomialThree (s : Finset (Fin 8)) : ThreeForm

The cubic coordinate array of a squarefree monomial.

Equations

• UnrestrictedBooleanMul.N4.monomialThree s i j k = if {i, j, k}.card = 3 then if s = {i, j, k} then 1 else 0 else 0

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_monomial (s : Finset (Fin 8)) : anfThreeProjection (monomial s) = monomialThree s

def UnrestrictedBooleanMul.N4.cubicPlaceModel (r : Fin 8) (θ : Fin 3) : ThreeForm

Cubic part of an input variable times a rational-place product.

Equations

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

def UnrestrictedBooleanMul.N4.coordinateLinear (r : Fin 8) : LinearForm

The linear form selecting one input coordinate.

Equations

• UnrestrictedBooleanMul.N4.coordinateLinear r i = if i = r then 1 else 0

theorem UnrestrictedBooleanMul.N4.vectorWedgeTwo_add_right_h (u : LinearForm) (q r : TwoForm) : vectorWedgeTwo u (q + r) = vectorWedgeTwo u q + vectorWedgeTwo u r

theorem UnrestrictedBooleanMul.N4.vectorWedgeTwo_smul_right_h (u : LinearForm) (a : F₂) (q : TwoForm) : vectorWedgeTwo u (a • q) = a • vectorWedgeTwo u q

def UnrestrictedBooleanMul.N4.vectorWedgeTwoBilinear : LinearForm →ₗ[F₂] TwoForm →ₗ[F₂] ThreeForm

The vector and two-form exterior product as a bilinear map.

Equations

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

theorem UnrestrictedBooleanMul.N4.monomialThree_union_targetPair (r : Fin 8) (i j : Fin 4) : monomialThree ({r} ∪ targetPair i j) = vectorWedgeTwo (coordinateLinear r) (vectorWedge (coordinateLinear (aCoord i)) (coordinateLinear (bCoord j)))

theorem UnrestrictedBooleanMul.N4.targetTwo_eq_double_wedge (c : TargetCoeff) : targetTwo c = ∑ i : Fin 4, ∑ j : Fin 4, c (hankelIndex i j) • vectorWedge (coordinateLinear (aCoord i)) (coordinateLinear (bCoord j))

theorem UnrestrictedBooleanMul.N4.linear_eq_sum_coordinate (ell : LinearForm) : ell = ∑ i : Fin 8, ell i • coordinateLinear i

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_linear_mul_rational (ell : LinearForm) (β : Fin 3 → F₂) : anfThreeProjection (linearANF ell * rationalANF β) = vectorWedgeTwo ell (rationalTwo β)

def UnrestrictedBooleanMul.N4.quarticProbeSet : Fin 3 → Finset (Fin 8)

Three quartic monomials detecting the rational-place wedge coordinates.

Equations

• UnrestrictedBooleanMul.N4.quarticProbeSet = ![{0, 1, 4, 6}, {1, 3, 5, 7}, {0, 3, 4, 7}]

def UnrestrictedBooleanMul.N4.quarticProbeANF : ANF 8 →ₗ[F₂] Fin 3 → F₂

Extract the three designated quartic coefficients of an ANF.

Equations

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

@[simp]

theorem UnrestrictedBooleanMul.N4.quarticProbeANF_monomial (s : Finset (Fin 8)) (t : Fin 3) : quarticProbeANF (monomial s) t = if s = quarticProbeSet t then 1 else 0

def UnrestrictedBooleanMul.N4.quarticWedgeProbe (q r : TwoForm) : Fin 3 → F₂

The three designated coordinates of a wedge of two two-forms.

Equations

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

def UnrestrictedBooleanMul.N4.wedgeTwoBilinear : TwoForm →ₗ[F₂] TwoForm →ₗ[F₂] FourForm

The exterior product of two two-forms as a bilinear map.

Equations

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

def UnrestrictedBooleanMul.N4.quarticWedgeProbeBilinear : TwoForm →ₗ[F₂] TwoForm →ₗ[F₂] Fin 3 → F₂

The three quartic wedge probes as a bilinear map.

Equations

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

theorem UnrestrictedBooleanMul.N4.quarticProbe_targetANF_mul_targetANF (c d : TargetCoeff) : quarticProbeANF (targetANF c * targetANF d) = quarticWedgeProbe (targetTwo c) (targetTwo d)

theorem UnrestrictedBooleanMul.N4.quarticProbe_rational_mul_rational (α β : Fin 3 → F₂) : quarticProbeANF (rationalANF α * rationalANF β) = quarticWedgeProbe (rationalTwo α) (rationalTwo β)

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_eq_zero_of_mem_targetAmbient {p : ANF 8} (hp : p ∈ targetAmbient 8 (mulTarget 4)) : anfThreeProjection p = 0

theorem UnrestrictedBooleanMul.N4.quarticProbeANF_eq_zero_of_mem_targetAmbient {p : ANF 8} (hp : p ∈ targetAmbient 8 (mulTarget 4)) : quarticProbeANF p = 0

theorem UnrestrictedBooleanMul.N4.rational_probe_zero_dependent (α β : Fin 3 → F₂) (h : quarticWedgeProbe (rationalTwo α) (rationalTwo β) = 0) : α = 0 ∨ β = 0 ∨ α = β

The three recorded quartic coordinates are already enough to detect dependence inside the rational-place three-space.

theorem UnrestrictedBooleanMul.N4.rational_wedge_zero_of_probe_zero (α β : Fin 3 → F₂) (h : quarticWedgeProbe (rationalTwo α) (rationalTwo β) = 0) : wedgeTwo (rationalTwo α) (rationalTwo β) = 0