Low--low products after the first feedback

The zero-high branch is reduced along the zero-wedge alternatives in the feedback coefficient space. The independent alternative is confined to the four-dimensional first-jet support K₀ by cubic rows.

def UnrestrictedBooleanMul.N4.InK0Linear (ell : LinearForm) : Prop

A linear form is supported on the first two coefficients of each input polynomial.

Equations

• UnrestrictedBooleanMul.N4.InK0Linear ell = (ell 2 = 0 ∧ ell 3 = 0 ∧ ell 6 = 0 ∧ ell 7 = 0)

theorem UnrestrictedBooleanMul.N4.normalizedFirstJetVector_inK0 (pa pb ja jb : F₂) : InK0Linear (normalizedFirstJetVector pa pb ja jb)

theorem UnrestrictedBooleanMul.N4.feedbackCoeffRep_firstPlane (q : FeedbackCoord) (hq : InFirstJetPlane q) : feedbackCoeffRep q = q 0 • targetBasis 0 + q 1 • targetBasis 1

theorem UnrestrictedBooleanMul.N4.targetANF_feedback_firstPlane (q : FeedbackCoord) (hq : InFirstJetPlane q) : targetANF (feedbackCoeffRep q) = q 0 • Mul 4 0 + q 1 • Mul 4 1

theorem UnrestrictedBooleanMul.N4.feedbackTarget_rationalLow_of_rational (q : FeedbackCoord) (hq : IsRationalCoeff (feedbackCoeffRep q)) : targetANF (feedbackCoeffRep q) ∈ rationalLowSpace

theorem UnrestrictedBooleanMul.N4.feedbackLowRep_rationalLow_of_rational (a : F₂) (ell : LinearForm) (q : FeedbackCoord) (hq : IsRationalCoeff (feedbackCoeffRep q)) : affineANF a ell + targetANF (feedbackCoeffRep q) ∈ rationalLowSpace

def UnrestrictedBooleanMul.N4.OutsideK0Index (i : Fin 8) : Prop

An input coordinate outside the normalized first-jet support.

Equations

• UnrestrictedBooleanMul.N4.OutsideK0Index i = (i = 2 ∨ i = 3 ∨ i = 6 ∨ i = 7)

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

theorem UnrestrictedBooleanMul.N4.monomialThree_eq_zero_of_not_mem (s : Finset (Fin 8)) (i j k : Fin 8) (hi : i ∉ s) : monomialThree s i j k = 0

theorem UnrestrictedBooleanMul.N4.independentFirstPlane_linears_inK0 (a b : F₂) (ell m : LinearForm) (q c : FeedbackCoord) (hq : InFirstJetPlane q) (hc : InFirstJetPlane c) (hq0 : q ≠ 0) (hc0 : c ≠ 0) (hqc : q ≠ c) (hprod : (affineANF a ell + targetANF (feedbackCoeffRep q)) * (affineANF b m + targetANF (feedbackCoeffRep c)) ∈ targetAmbient 8 (mulTarget 4)) : InK0Linear ell ∧ InK0Linear m

theorem UnrestrictedBooleanMul.N4.independentFirstPlane_linears_inK0_of_seedCubic (a b : F₂) (ell m M : LinearForm) (q c : FeedbackCoord) (hq : InFirstJetPlane q) (hc : InFirstJetPlane c) (hq0 : q ≠ 0) (hc0 : c ≠ 0) (hqc : q ≠ c) (hM : InK0Linear M) (hthree : anfThreeProjection ((affineANF a ell + targetANF (feedbackCoeffRep q)) * (affineANF b m + targetANF (feedbackCoeffRep c))) = vectorWedgeTwo M (rationalPlaceTwo 0)) : InK0Linear ell ∧ InK0Linear m

The same outside-row solve when the cubic part is the normalized seed rather than zero. The seed has no row leaving K₀, so the two scalar equations used above are unchanged.

theorem UnrestrictedBooleanMul.N4.linearANF_eq_k0 (ell : LinearForm) (h : InK0Linear ell) : linearANF ell = ell 0 • X 0 + ell 1 • X 1 + ell 4 • X 4 + ell 5 • X 5

theorem UnrestrictedBooleanMul.N4.monomialTwo_eq_zero_of_not_mem (s : Finset (Fin 8)) (i j : Fin 8) (hi : i ∉ s) : monomialTwo s i j = 0

theorem UnrestrictedBooleanMul.N4.firstPlane_product_two_outside (a b : F₂) (ell m : LinearForm) (q c : FeedbackCoord) (hell : InK0Linear ell) (hm : InK0Linear m) (hq : InFirstJetPlane q) (hc : InFirstJetPlane c) (z : Fin 8) (hz : OutsideK0Index z) (j : Fin 8) : anfTwoProjection ((affineANF a ell + targetANF (feedbackCoeffRep q)) * (affineANF b m + targetANF (feedbackCoeffRep c))) z j = 0

theorem UnrestrictedBooleanMul.N4.feedbackLow_mul_mem_of_mem_targetAmbient {p r : ANF 8} (hp : p ∈ zeroFeedbackLowSpace) (hr : r ∈ zeroFeedbackLowSpace) (hprod : p * r ∈ targetAmbient 8 (mulTarget 4)) : p * r ∈ zeroFeedbackLowSpace

A product of two feedback-low wires whose high part vanishes cannot leave the feedback-low state.