Normalizing a quartic seed plane at the zero place

Once the feedback coefficient is the singleton at zero, the independent seed quadratics can be changed to a basis whose first member is that singleton. The second member has one of the three concrete coefficient words below. Changing factor basis modifies the seed product only by rational-low wires, which are absorbed into the existing correction.

def UnrestrictedBooleanMul.N4.QuarticPlaneTypeAtZero (zeta : Fin 3 → F₂) : Prop

One of the three nonzero coefficient vectors supported away from the zero place.

Equations

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

@[instance_reducible]

instance UnrestrictedBooleanMul.N4.instDecidableQuarticPlaneTypeAtZero (zeta : Fin 3 → F₂) : Decidable (QuarticPlaneTypeAtZero zeta)

Equations

• UnrestrictedBooleanMul.N4.instDecidableQuarticPlaneTypeAtZero zeta = id inferInstance

theorem UnrestrictedBooleanMul.N4.quarticPlaneTypeAtZero_of_coord_zero (zeta : Fin 3 → F₂) (hzero : zeta 0 = 0) (hne : zeta ≠ 0) : QuarticPlaneTypeAtZero zeta

A nonzero coefficient word with zero coordinate at the anchor is one of the three possible complementary plane directions.

theorem UnrestrictedBooleanMul.N4.rational_plane_basis_at_zero (alpha beta : Fin 3 → F₂) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hab : alpha ≠ beta) (hzero : InRationalCoeffPlane alpha beta (rationalSingleton 0)) : ∃ (p : F₂) (q : F₂) (r : F₂) (s : F₂), p * s + q * r = 1 ∧ s • alpha + q • beta = rationalSingleton 0 ∧ (r • alpha + p • beta) 0 = 0 ∧ r • alpha + p • beta ≠ 0

Explicit GL₂(F₂) basis selection for a coefficient plane containing the zero singleton.

theorem UnrestrictedBooleanMul.N4.representedLowFactor_linear_combination (s q a b : F₂) (ell m : LinearForm) (alpha beta gamma : Fin 3 → F₂) (hgamma : s • alpha + q • beta = gamma) : s • representedLowFactor a ell alpha + q • representedLowFactor b m beta = representedLowFactor (s * a + q * b) (s • ell + q • m) gamma

def UnrestrictedBooleanMul.N4.ZeroAnchoredQuarticSeedForm (g correction : ANF 8) : Prop

A quartic seed and correction expressed in the normalized zero-anchored plane form.

Equations

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

theorem UnrestrictedBooleanMul.N4.zeroAnchoredQuarticSeedForm_of_plane {g correction : ANF 8} {leftConst rightConst : F₂} {leftLinear rightLinear : LinearForm} {alpha beta : Fin 3 → F₂} (hg : g = representedLowFactor leftConst leftLinear alpha * representedLowFactor rightConst rightLinear beta) (hcorrection : correction ∈ rationalLowSpace) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hab : alpha ≠ beta) (hzero : InRationalCoeffPlane alpha beta (rationalSingleton 0)) : ZeroAnchoredQuarticSeedForm g correction

Absorb a GL₂(F₂) change of the two seed factors into the rational-low correction.