The cancelled-high low--low branch

The second low--low gate can cancel the cubic seed only through a common first-jet target direction. Its quadratic shadow is then a sum of a term supported on K₀ and at most two exterior directions. Jet separation sends the resulting target back to the feedback state.

theorem UnrestrictedBooleanMul.N4.normalizedFirstJetVector_not_mem_anchorPlane (pa pb ja jb : F₂) (hjet : ja ≠ 0 ∨ jb ≠ 0) : normalizedFirstJetVector pa pb ja jb ∉ anchorPlane

theorem UnrestrictedBooleanMul.N4.normalizedFirstJet_span_two_ne_anchorPlane (pa pb ja jb : F₂) (N : LinearForm) (hjet : ja ≠ 0 ∨ jb ≠ 0) : Submodule.span F₂ (Set.range ![normalizedFirstJetVector pa pb ja jb, N]) ≠ anchorPlane

theorem UnrestrictedBooleanMul.N4.rationalCoeffRep_mem_feedbackCoeffSpace (alpha : Fin 3 → F₂) : rationalCoeffRep alpha ∈ feedbackCoeffSpace

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.booleanContraction (ell : LinearForm) {k : TwoForm} (hk : SupportedK0Two k) : SupportedK0Two (N4.booleanContraction ell k)

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.rationalPlaceTwo_zero : SupportedK0Two (rationalPlaceTwo 0)

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.booleanContraction_zeroPlace (M : LinearForm) : SupportedK0Two (N4.booleanContraction M (rationalPlaceTwo 0))

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.targetTwo_feedback_firstPlane (q : FeedbackCoord) (hq : InFirstJetPlane q) : SupportedK0Two (targetTwo (feedbackCoeffRep q))

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.affine_mul_coordinateQuadratic (a : F₂) (ell u v : LinearForm) (hu : InK0Linear u) (hv : InK0Linear v) (hdisjoint : pointwiseLinearProduct u v = 0) : SupportedK0Two (anfTwoProjection (affineANF a ell * (linearANF u * linearANF v)))

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.affine_mul_feedback_firstPlane (a : F₂) (ell : LinearForm) (q : FeedbackCoord) (hq : InFirstJetPlane q) : SupportedK0Two (anfTwoProjection (affineANF a ell * targetANF (feedbackCoeffRep q)))

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.feedback_firstPlane_mul_affine (q : FeedbackCoord) (a : F₂) (ell : LinearForm) (hq : InFirstJetPlane q) : SupportedK0Two (anfTwoProjection (targetANF (feedbackCoeffRep q) * affineANF a ell))

theorem UnrestrictedBooleanMul.N4.SupportedK0Two.feedback_firstPlane_mul_feedback_firstPlane (q c : FeedbackCoord) (hq : InFirstJetPlane q) (hc : InFirstJetPlane c) : SupportedK0Two (anfTwoProjection (targetANF (feedbackCoeffRep q) * targetANF (feedbackCoeffRep c)))

theorem UnrestrictedBooleanMul.N4.feedbackProduct_twoShadow_supported (a b : F₂) (ell m : LinearForm) (q c : FeedbackCoord) (hq : InFirstJetPlane q) (hc : InFirstJetPlane c) : SupportedK0Two (anfTwoProjection ((affineANF a ell + targetANF (feedbackCoeffRep q)) * (affineANF b m + targetANF (feedbackCoeffRep c))) + vectorWedge ell m)

After removing the affine--affine wedge, a product whose two target parts lie in the first-jet plane is wholly supported on K₀.

theorem UnrestrictedBooleanMul.N4.feedbackCoeffRep_zero : feedbackCoeffRep 0 = 0

theorem UnrestrictedBooleanMul.N4.targetANF_feedbackCoeffRep_zero : targetANF (feedbackCoeffRep 0) = 0

def UnrestrictedBooleanMul.N4.feedbackCoeffPure (q : FeedbackCoord) : TargetCoeff

A computational presentation of the feedback coefficient word. It is kept separate from the basis-vector presentation so the small fixed cubic certificate below contains no classical Pi.basisFun.

Equations

• UnrestrictedBooleanMul.N4.feedbackCoeffPure q s = ((q 3 + if s = 0 then q 0 else 0) + if s = 1 then q 1 else 0) + if s = 6 then q 2 else 0

theorem UnrestrictedBooleanMul.N4.feedbackCoeffRep_eq_pure (q : FeedbackCoord) : feedbackCoeffRep q = feedbackCoeffPure q

theorem UnrestrictedBooleanMul.N4.commonFeedback_seedCubic_classification (pa pb ja jb : F₂) (q : FeedbackCoord) (N : LinearForm) (hjet : ja ≠ 0 ∨ jb ≠ 0) (hq0 : q ≠ 0) (hcubic : vectorWedgeTwo N (targetTwo (feedbackCoeffRep q)) = vectorWedgeTwo (normalizedFirstJetVector pa pb ja jb) (rationalPlaceTwo 0)) : InFirstJetPlane q ∧ InK0Linear N

theorem UnrestrictedBooleanMul.N4.feedbackProduct_cubic_zero_left (a b : F₂) (ell m : LinearForm) (c : FeedbackCoord) : anfThreeProjection ((affineANF a ell + targetANF (feedbackCoeffRep 0)) * (affineANF b m + targetANF (feedbackCoeffRep c))) = vectorWedgeTwo ell (targetTwo (feedbackCoeffRep c))

theorem UnrestrictedBooleanMul.N4.feedbackProduct_cubic_zero_right (a b : F₂) (ell m : LinearForm) (q : FeedbackCoord) : anfThreeProjection ((affineANF a ell + targetANF (feedbackCoeffRep q)) * (affineANF b m + targetANF (feedbackCoeffRep 0))) = vectorWedgeTwo m (targetTwo (feedbackCoeffRep q))

theorem UnrestrictedBooleanMul.N4.feedbackProduct_cubic_equal (a b : F₂) (ell m : LinearForm) (q : FeedbackCoord) : anfThreeProjection ((affineANF a ell + targetANF (feedbackCoeffRep q)) * (affineANF b m + targetANF (feedbackCoeffRep q))) = vectorWedgeTwo (ell + m) (targetTwo (feedbackCoeffRep q))

theorem UnrestrictedBooleanMul.N4.target_mem_feedback_of_seed_product_shadow {g correction shift product F : ANF 8} {M companion N R : LinearForm} {pa pb ja jb : F₂} (hcorrection : correction ∈ rationalLowSpace) (hseed : g + correction = linearANF M * (linearANF companion + rationalANF (rationalSingleton 0))) (hM : M = normalizedFirstJetVector pa pb ja jb) (hjet : ja ≠ 0 ∨ jb ≠ 0) (hshift : shift ∈ zeroFeedbackLowSpace) (hFmem : F ∈ targetAmbient 8 (mulTarget 4)) (hF : F = shift + g + product) (hN : InK0Linear N) (hproductShadow : SupportedK0Two (anfTwoProjection product + vectorWedge N R)) : F ∈ zeroFeedbackLowSpace

Assemble the seed quadratic identity and a one-direction product shadow, then invoke jet separation.

theorem UnrestrictedBooleanMul.N4.no_normalizedLowLow_feedbackTarget {g correction shift p r F : ANF 8} {M companion : LinearForm} {pa pb ja jb : F₂} (hg : DegreeLE 3 g) (hcorrection : correction ∈ rationalLowSpace) (hseed : g + correction = linearANF M * (linearANF companion + rationalANF (rationalSingleton 0))) (hM : M = normalizedFirstJetVector pa pb ja jb) (hjet : ja ≠ 0 ∨ jb ≠ 0) (hseedCubic : vectorWedgeTwo M (rationalPlaceTwo 0) ≠ 0) (hshift : shift ∈ zeroFeedbackLowSpace) (hp : p ∈ zeroFeedbackLowSpace) (hr : r ∈ zeroFeedbackLowSpace) (hFmem : F ∈ targetAmbient 8 (mulTarget 4)) (hFoutside : F ∉ zeroFeedbackLowSpace) (hF : F = shift + g + p * r) : False

Algebraic exclusion of the low--low second feedback whose cubic part cancels the normalized seed.