Quintic anchor certificate

After place normalization the first feedback target is a tangent at the zero rational place. Sixteen degree-five monomials separate a rational cubic from every cubic not anchored there. The ANF bridge is checked only on the 8 * 3 * 2 input/place/tangent basis rows and extended by linearity. This is a fixed algebraic matrix certificate, not circuit enumeration.

def UnrestrictedBooleanMul.N4.quinticAnchorCoord : Fin 16 → Fin 8 × Fin 8 × Fin 8 × Fin 8 × Fin 8

Sixteen quintic coordinates used to detect the cubic anchor.

Equations

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

def UnrestrictedBooleanMul.N4.quinticAnchorSet (k : Fin 16) : Finset (Fin 8)

The squarefree monomial corresponding to a quintic anchor coordinate.

Equations

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

def UnrestrictedBooleanMul.N4.anfQuinticAnchorProbe : ANF 8 →ₗ[F₂] Fin 16 → F₂

Extract the sixteen quintic anchor coefficients from an ANF.

Equations

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

def UnrestrictedBooleanMul.N4.cubicAnchorWedgeProbe (h : ThreeForm) (q : TwoForm) : Fin 16 → F₂

The sixteen anchor coordinates of a three-form wedged with a two-form.

Equations

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

def UnrestrictedBooleanMul.N4.cubicAnchorWedgeProbeBilinear : ThreeForm →ₗ[F₂] TwoForm →ₗ[F₂] Fin 16 → F₂

The quintic anchor wedge probes as a bilinear map.

Equations

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

theorem UnrestrictedBooleanMul.N4.anfQuinticAnchorProbe_eq_zero_of_degreeLE_four {p : ANF 8} (hp : DegreeLE 4 p) : anfQuinticAnchorProbe p = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfQuinticAnchorProbe_monomial (u : Finset (Fin 8)) (k : Fin 16) : anfQuinticAnchorProbe (monomial u) k = if u = quinticAnchorSet k then 1 else 0

theorem UnrestrictedBooleanMul.N4.DegreeLE.smul {m d : ℕ} {p : ANF m} (hp : DegreeLE d p) (a : F₂) : DegreeLE d (a • p)

theorem UnrestrictedBooleanMul.N4.degreeLE_monomial_of_card_le {m d : ℕ} (u : Finset (Fin m)) (hu : u.card ≤ d) : DegreeLE d (monomial u)

def UnrestrictedBooleanMul.N4.anfMonomialList : List (Finset (Fin 8)) → ANF 8

The ANF sum of a list of squarefree monomials.

Equations

• UnrestrictedBooleanMul.N4.anfMonomialList [] = 0
• UnrestrictedBooleanMul.N4.anfMonomialList (u :: rest) = UnrestrictedBooleanMul.monomial u + UnrestrictedBooleanMul.N4.anfMonomialList rest

def UnrestrictedBooleanMul.N4.monomialListProbeModel (sets : List (Finset (Fin 8))) (r : Fin 8) : Fin 16 → F₂

The anchor coefficients after multiplying a monomial list by one input variable.

Equations

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

theorem UnrestrictedBooleanMul.N4.anfQuinticAnchorProbe_X_mul_monomialList (sets : List (Finset (Fin 8))) (r : Fin 8) : anfQuinticAnchorProbe (X r * anfMonomialList sets) = monomialListProbeModel sets r

theorem UnrestrictedBooleanMul.N4.degreeLE_anfMonomialList {d : ℕ} (sets : List (Finset (Fin 8))) (hsets : ∀ u ∈ sets, u.card ≤ d) : DegreeLE d (anfMonomialList sets)

def UnrestrictedBooleanMul.N4.oneTangentLowList (eps : F₂) : List (Finset (Fin 8))

The lower-degree monomials in the evaluation-at-one tangent product.

Equations

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

def UnrestrictedBooleanMul.N4.oneTangentQuarticList (eps : F₂) : List (Finset (Fin 8))

The quartic monomials in the evaluation-at-one tangent product.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.oneTangentProductANF (eps : F₂) : ANF 8

The ANF of the evaluation-at-one target times its chosen tangent target.

Equations

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

def UnrestrictedBooleanMul.N4.infinityTangentBasisModel (r : Fin 8) (eps : F₂) (k : Fin 16) : F₂

The quintic anchor coefficients of a variable times the infinity tangent product.

Equations

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

theorem UnrestrictedBooleanMul.N4.anfQuinticAnchorProbe_linear_rational_zero_tangent (ell : LinearForm) (alpha : Fin 3 → F₂) (eps : F₂) : anfQuinticAnchorProbe (linearANF ell * rationalANF alpha * targetANF (rationalTangentAt 0 eps)) = cubicAnchorWedgeProbe (vectorWedgeTwo ell (rationalTwo alpha)) (targetTwo (rationalTangentAt 0 eps))

The selected degree-five coefficients of a rational cubic times a zero-place tangent are its exterior anchor probes.

theorem UnrestrictedBooleanMul.N4.cubicAnchorProbe_zero_tangent_classification (ell : LinearForm) (alpha : Fin 3 → F₂) (eps : F₂) (hann : cubicAnchorWedgeProbe (vectorWedgeTwo ell (rationalTwo alpha)) (targetTwo (rationalTangentAt 0 eps)) = 0) : vectorWedgeTwo ell (rationalTwo alpha) = vectorWedgeTwo (alpha 0 • ell) (rationalPlaceTwo 0)

The 16-row certificate: a rational cubic annihilating a zero-place tangent is anchored at the zero rational place.

theorem UnrestrictedBooleanMul.N4.anfQuinticAnchorProbe_low_mul_target_zero {p : ANF 8} (hp : DegreeLE 2 p) (c : TargetCoeff) : anfQuinticAnchorProbe (p * targetANF c) = 0

A degree-at-most-two ANF times a quadratic target contributes no degree-five anchor probe.