Fixed homogeneous bridges for the feedback state

Only six quartic rows are consumed by the zero-wedge and second-jet minors. This file connects those rows to actual Boolean ANF products. The proof is bilinear and checks the fixed 7 × 7 × 6 basis matrix; it never enumerates circuits or Boolean functions.

def UnrestrictedBooleanMul.N4.feedbackQuarticCoord : Fin 6 → Fin 8 × Fin 8 × Fin 8 × Fin 8

The six quartic coordinates used by the feedback minors.

Equations

• UnrestrictedBooleanMul.N4.feedbackQuarticCoord = ![(0, 1, 4, 5), (0, 1, 4, 6), (0, 3, 4, 7), (0, 3, 5, 7), (0, 3, 6, 7), (0, 1, 6, 7)]

def UnrestrictedBooleanMul.N4.feedbackQuarticProbeANF : ANF 8 →ₗ[F₂] Fin 6 → F₂

Extract the six quartic ANF coefficients used in feedback arguments.

Equations

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

@[simp]

theorem UnrestrictedBooleanMul.N4.feedbackQuarticProbeANF_apply (p : ANF 8) (u : Fin 6) : feedbackQuarticProbeANF p u = anfFourProjection p (feedbackQuarticCoord u).1 (feedbackQuarticCoord u).2.1 (feedbackQuarticCoord u).2.2.1 (feedbackQuarticCoord u).2.2.2

def UnrestrictedBooleanMul.N4.feedbackQuarticWedgeProbe (q c : TwoForm) : Fin 6 → F₂

Extract the six feedback coordinates of a wedge of two two-forms.

Equations

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

theorem UnrestrictedBooleanMul.N4.anfFourProjection_eq_zero_of_degreeLE_three {p : ANF 8} (hp : DegreeLE 3 p) : anfFourProjection p = 0

theorem UnrestrictedBooleanMul.N4.feedbackQuarticProbeANF_eq_zero_of_degreeLE_three {p : ANF 8} (hp : DegreeLE 3 p) : feedbackQuarticProbeANF p = 0

def UnrestrictedBooleanMul.N4.feedbackQuarticWedgeProbeBilinear : TwoForm →ₗ[F₂] TwoForm →ₗ[F₂] Fin 6 → F₂

The six feedback wedge probes as a bilinear map.

Equations

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

theorem UnrestrictedBooleanMul.N4.feedbackQuarticProbe_target_mul_target (c d : TargetCoeff) : feedbackQuarticProbeANF (targetANF c * targetANF d) = feedbackQuarticWedgeProbe (targetTwo c) (targetTwo d)

theorem UnrestrictedBooleanMul.N4.feedbackProduct_quarticProbe (a b : F₂) (ell m : LinearForm) (q c : FeedbackCoord) : feedbackQuarticProbeANF ((affineANF a ell + targetANF (feedbackCoeffRep q)) * (affineANF b m + targetANF (feedbackCoeffRep c))) = feedbackQuarticWedgeProbe (targetTwo (feedbackCoeffRep q)) (targetTwo (feedbackCoeffRep c))

theorem UnrestrictedBooleanMul.N4.feedbackProduct_zeroWedgeStructure (a b : F₂) (ell m : LinearForm) (q c : FeedbackCoord) (hzero : feedbackQuarticProbeANF ((affineANF a ell + targetANF (feedbackCoeffRep q)) * (affineANF b m + targetANF (feedbackCoeffRep c))) = 0) : q = 0 ∨ c = 0 ∨ q = c ∨ InFirstJetPlane q ∧ InFirstJetPlane c

Quartic vanishing for a product of two feedback-low wires has exactly the zero-wedge alternatives of Feedback.lean.