Cubic projection against an arbitrary Hankel target

This extends the rational-place cubic bridge to every coefficient in the seven-dimensional Hankel target. It is used only for the D = 0 branch of quartic exclusion.

def UnrestrictedBooleanMul.N4.cubicTargetModel (r : Fin 8) (c : TargetCoeff) : ThreeForm

Cubic part of an input variable times an arbitrary product target.

Equations

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

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_linear_mul_target (ell : LinearForm) (c : TargetCoeff) : anfThreeProjection (linearANF ell * targetANF c) = vectorWedgeTwo ell (targetTwo c)

Multiplying a linear ANF by a target quadratic has cubic part given by the vector--two-form exterior product.

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_target_mul_affine (c : TargetCoeff) (a : F₂) (ell : LinearForm) : anfThreeProjection (targetANF c * affineANF a ell) = vectorWedgeTwo ell (targetTwo c)

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_targetRep_mul_affine (A b : F₂) (ell m : LinearForm) (c : TargetCoeff) : anfThreeProjection ((affineANF A ell + targetANF c) * affineANF b m) = vectorWedgeTwo m (targetTwo c)

theorem UnrestrictedBooleanMul.N4.nonrational_target_vectorWedge_injective {c : TargetCoeff} (hc : ¬IsRationalCoeff c) {ell : LinearForm} (h : vectorWedgeTwo ell (targetTwo c) = 0) : ell = 0

A nonrational Hankel target has no nonzero vector annihilator. Otherwise the target two-form would be decomposable and hence one of the three rational rank-one places.

theorem UnrestrictedBooleanMul.N4.seedUsing_factorCoeff_ne_zero_of_not_mem_targetAmbient {g correction factor target : ANF 8} {targetConst factorConst : F₂} {targetLinear factorLinear : LinearForm} {targetCoeff : TargetCoeff} {factorCoeff : Fin 3 → F₂} (hseed : g ∉ targetAmbient 8 (mulTarget 4)) (hcorrection : correction ∈ rationalLowSpace) (htargetEq : target = (g + correction) * factor) (htargetMem : target ∈ targetAmbient 8 (mulTarget 4)) (htargetNotLow : target ∉ rationalLowSpace) (htargetRep : target = affineANF targetConst targetLinear + targetANF targetCoeff) (hfactorRep : factor = affineANF factorConst factorLinear + rationalANF factorCoeff) (htargetNonrational : ¬IsRationalCoeff targetCoeff) (hright : target * factor = target) : factorCoeff ≠ 0

A seed outside the target ambient forces every seed-using factor to have a nonzero rational quadratic coefficient.

theorem UnrestrictedBooleanMul.N4.seedUsing_factorCoeff_ne_zero {g correction factor target : ANF 8} {targetConst factorConst : F₂} {targetLinear factorLinear : LinearForm} {targetCoeff : TargetCoeff} {factorCoeff : Fin 3 → F₂} (hquartic : quarticProbeANF g ≠ 0) (hcorrection : correction ∈ rationalLowSpace) (htargetEq : target = (g + correction) * factor) (htargetMem : target ∈ targetAmbient 8 (mulTarget 4)) (htargetNotLow : target ∉ rationalLowSpace) (htargetRep : target = affineANF targetConst targetLinear + targetANF targetCoeff) (hfactorRep : factor = affineANF factorConst factorLinear + rationalANF factorCoeff) (htargetNonrational : ¬IsRationalCoeff targetCoeff) (hright : target * factor = target) : factorCoeff ≠ 0

Quartic specialization of the ambient-space obstruction.

theorem UnrestrictedBooleanMul.N4.seedUsing_factorCoeff_ne_zero_of_cubic {g correction factor target : ANF 8} {targetConst factorConst : F₂} {targetLinear factorLinear : LinearForm} {targetCoeff : TargetCoeff} {factorCoeff : Fin 3 → F₂} (hcubicSeed : anfThreeProjection g ≠ 0) (hcorrection : correction ∈ rationalLowSpace) (htargetEq : target = (g + correction) * factor) (htargetMem : target ∈ targetAmbient 8 (mulTarget 4)) (htargetNotLow : target ∉ rationalLowSpace) (htargetRep : target = affineANF targetConst targetLinear + targetANF targetCoeff) (hfactorRep : factor = affineANF factorConst factorLinear + rationalANF factorCoeff) (htargetNonrational : ¬IsRationalCoeff targetCoeff) (hright : target * factor = target) : factorCoeff ≠ 0

Cubic specialization of the ambient-space obstruction.