Excluding a seed-using second feedback

This file composes the manuscript's degree-five, degree-four, and degree-three rows. A target outside the feedback state is first forced to be a second jet. Its right absorption identity then kills the feedback quadratic and linear parts of the other factor. The remaining constant would put the nonzero seed cubic in the quadratic target ambient.

theorem UnrestrictedBooleanMul.N4.mem_feedbackCoeffSpace_iff_exists_rep (c : TargetCoeff) : c ∈ feedbackCoeffSpace ↔ ∃ (q : FeedbackCoord), c = feedbackCoeffRep q

theorem UnrestrictedBooleanMul.N4.feedbackTarget_mem_zeroFeedbackLow (q : FeedbackCoord) : targetANF (feedbackCoeffRep q) ∈ zeroFeedbackLowSpace

theorem UnrestrictedBooleanMul.N4.targetRep_mem_zeroFeedbackLow_iff (a : F₂) (ell : LinearForm) (c : TargetCoeff) : affineANF a ell + targetANF c ∈ zeroFeedbackLowSpace ↔ c ∈ feedbackCoeffSpace

theorem UnrestrictedBooleanMul.N4.target_feedback_absorption_wedge_zero (A b : F₂) (ell m : LinearForm) (c : TargetCoeff) (q : FeedbackCoord) (habsorb : (affineANF A ell + targetANF c) * (affineANF b m + targetANF (feedbackCoeffRep q)) = affineANF A ell + targetANF c) : feedbackQuarticWedgeProbe (targetTwo c) (targetTwo (feedbackCoeffRep q)) = 0

Quartic degree in a right absorption identity is exactly the wedge of the target coefficient with the feedback coefficient of the factor.

theorem UnrestrictedBooleanMul.N4.no_normalizedSeedUsing_feedbackTarget {g correction addend factor F : ANF 8} {M N : LinearForm} {pa pb ja jb : F₂} (hg : DegreeLE 3 g) (hcorrection : correction ∈ rationalLowSpace) (hseed : g + correction = linearANF M * (linearANF N + rationalANF (rationalSingleton 0))) (hM : M = normalizedFirstJetVector pa pb ja jb) (hjet : ja ≠ 0 ∨ jb ≠ 0) (hseedCubic : vectorWedgeTwo M (rationalPlaceTwo 0) ≠ 0) (haddend : addend ∈ zeroFeedbackLowSpace) (hfactor : factor ∈ zeroFeedbackLowSpace) (hFmem : F ∈ targetAmbient 8 (mulTarget 4)) (hFoutside : F ∉ zeroFeedbackLowSpace) (hF : F = (g + addend) * factor) : False

Algebraic exclusion of the G-using type of second feedback.