Algebraic feedback-state lemmas

The feedback state has quadratic target space S = ⟨E₀,E₁,E₆,r₁⟩. The only relation among its six pair wedges is E₀ ∧ E₁ = 0. We prove this from the five coordinate rows displayed in the manuscript and derive the zero-wedge structure needed by the low--low second-feedback exclusion.

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.FeedbackCoord : Type

Coordinates in the basis consisting of the first, second, last, and evaluation-at-one targets.

Equations

• UnrestrictedBooleanMul.N4.FeedbackCoord = (Fin 4 → UnrestrictedBooleanMul.F₂)

noncomputable def UnrestrictedBooleanMul.N4.feedbackCoeffRep (q : FeedbackCoord) : TargetCoeff

Represent feedback coordinates in the target coefficient space.

Equations

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

def UnrestrictedBooleanMul.N4.feedbackMinor (q c : FeedbackCoord) (i j : Fin 4) : F₂

A two-by-two minor of the two feedback coordinate vectors.

Equations

• UnrestrictedBooleanMul.N4.feedbackMinor q c i j = q i * c j + q j * c i

theorem UnrestrictedBooleanMul.N4.feedback_wedge_relations {q c : FeedbackCoord} (h : wedgeTwo (targetTwo (feedbackCoeffRep q)) (targetTwo (feedbackCoeffRep c)) = 0) : feedbackMinor q c 0 2 = 0 ∧ feedbackMinor q c 0 3 = 0 ∧ feedbackMinor q c 1 2 = 0 ∧ feedbackMinor q c 1 3 = 0 ∧ feedbackMinor q c 2 3 = 0

def UnrestrictedBooleanMul.N4.InFirstJetPlane (q : FeedbackCoord) : Prop

The feedback vector lies in the plane of the first two target coefficients.

Equations

• UnrestrictedBooleanMul.N4.InFirstJetPlane q = (q 2 = 0 ∧ q 3 = 0)

theorem UnrestrictedBooleanMul.N4.feedback_dependent_or_firstJetPlane {q c : FeedbackCoord} (h02 : feedbackMinor q c 0 2 = 0) (h03 : feedbackMinor q c 0 3 = 0) (h12 : feedbackMinor q c 1 2 = 0) (h13 : feedbackMinor q c 1 3 = 0) (h23 : feedbackMinor q c 2 3 = 0) : q = 0 ∨ c = 0 ∨ q = c ∨ InFirstJetPlane q ∧ InFirstJetPlane c

theorem UnrestrictedBooleanMul.N4.feedback_zero_wedge_structure {q c : FeedbackCoord} (h : wedgeTwo (targetTwo (feedbackCoeffRep q)) (targetTwo (feedbackCoeffRep c)) = 0) : q = 0 ∨ c = 0 ∨ q = c ∨ InFirstJetPlane q ∧ InFirstJetPlane c

Zero-wedge structure in S: either the two directions are dependent, or both lie in ⟨E₀,E₁⟩.

theorem UnrestrictedBooleanMul.N4.feedback_zero_wedge_structure_of_rows {q c : FeedbackCoord} (h0 : wedgeTwo (targetTwo (feedbackCoeffRep q)) (targetTwo (feedbackCoeffRep c)) 0 1 4 5 = 0) (h1 : wedgeTwo (targetTwo (feedbackCoeffRep q)) (targetTwo (feedbackCoeffRep c)) 0 1 4 6 = 0) (h2 : wedgeTwo (targetTwo (feedbackCoeffRep q)) (targetTwo (feedbackCoeffRep c)) 0 3 4 7 = 0) (h3 : wedgeTwo (targetTwo (feedbackCoeffRep q)) (targetTwo (feedbackCoeffRep c)) 0 3 5 7 = 0) (h4 : wedgeTwo (targetTwo (feedbackCoeffRep q)) (targetTwo (feedbackCoeffRep c)) 0 3 6 7 = 0) : q = 0 ∨ c = 0 ∨ q = c ∨ InFirstJetPlane q ∧ InFirstJetPlane c

Row-wise form used by the ANF quartic bridge. These are precisely the five displayed rows of the manuscript's zero-wedge matrix.

noncomputable def UnrestrictedBooleanMul.N4.secondJetFeedbackCoeff (α β : F₂) : TargetCoeff

The second-jet coefficient vector with its two lower-order parameters.

Equations

• UnrestrictedBooleanMul.N4.secondJetFeedbackCoeff α β = UnrestrictedBooleanMul.N4.targetBasis 2 + α • UnrestrictedBooleanMul.N4.targetBasis 1 + β • UnrestrictedBooleanMul.N4.targetBasis 0

theorem UnrestrictedBooleanMul.N4.secondJet_wedge_feedback_injective (α β : F₂) (q : FeedbackCoord) (h : wedgeTwo (targetTwo (secondJetFeedbackCoeff α β)) (targetTwo (feedbackCoeffRep q)) = 0) : q = 0

Wedge by any second-jet representative is injective on the feedback state S.

theorem UnrestrictedBooleanMul.N4.secondJet_wedge_feedback_injective_of_rows (α β : F₂) (q : FeedbackCoord) (h0 : wedgeTwo (targetTwo (secondJetFeedbackCoeff α β)) (targetTwo (feedbackCoeffRep q)) 0 1 4 5 = 0) (h1 : wedgeTwo (targetTwo (secondJetFeedbackCoeff α β)) (targetTwo (feedbackCoeffRep q)) 0 1 4 6 = 0) (h2 : wedgeTwo (targetTwo (secondJetFeedbackCoeff α β)) (targetTwo (feedbackCoeffRep q)) 0 1 6 7 = 0) (h3 : wedgeTwo (targetTwo (secondJetFeedbackCoeff α β)) (targetTwo (feedbackCoeffRep q)) 0 3 6 7 = 0) : q = 0

Four-row version of second-jet injectivity, matching the explicit minor in the manuscript.

theorem UnrestrictedBooleanMul.N4.secondJetFeedback_not_rankOne (α β : F₂) : ¬HankelRankLEOne (secondJetFeedbackCoeff α β)

theorem UnrestrictedBooleanMul.N4.secondJet_vector_wedge_injective (α β : F₂) (u : LinearForm) (h : vectorWedgeTwo u (targetTwo (secondJetFeedbackCoeff α β)) = 0) : u = 0

The alternating rank of a second-jet representative is at least four; equivalently, wedging it with a vector is injective.