Place normalization on the complete target state

The first-jet argument chooses one of three rational places. This file extends the existing change of variables from rational generators and tangents to every Hankel target. The change is an involution on the Boolean ANF algebra, so target-ambient and rational-low membership can be transported in both directions. The only coordinate certificate is the displayed 7 × 7 change of Hankel coefficients.

def UnrestrictedBooleanMul.N4.normalizeTargetCoeff : Fin 3 → TargetCoeff → TargetCoeff

The induced changes on the seven Hankel coefficients: identity, translation, and reversal.

Equations

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

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_targetANF (theta : Fin 3) (c : TargetCoeff) : (anfPlaceNormalize theta) (targetANF c) = targetANF (normalizeTargetCoeff theta c)

theorem UnrestrictedBooleanMul.N4.normalizePlaceLinear_coordinate (theta : Fin 3) (i : Fin 8) : normalizePlaceLinear theta (coordinateLinear i) = inputPlaceChange theta i

theorem UnrestrictedBooleanMul.N4.prod_X_eq_monomial (s : Finset (Fin 8)) : ∏ i ∈ s, X i = monomial s

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_involutive (theta : Fin 3) (p : ANF 8) : (anfPlaceNormalize theta) ((anfPlaceNormalize theta) p) = p

Each of the three place changes is an involution on all Boolean ANFs.

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_injective (theta : Fin 3) : Function.Injective ⇑(anfPlaceNormalize theta)

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_mem_targetAmbient (theta : Fin 3) {p : ANF 8} (hp : p ∈ targetAmbient 8 (mulTarget 4)) : (anfPlaceNormalize theta) p ∈ targetAmbient 8 (mulTarget 4)

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_mem_targetAmbient_iff (theta : Fin 3) (p : ANF 8) : (anfPlaceNormalize theta) p ∈ targetAmbient 8 (mulTarget 4) ↔ p ∈ targetAmbient 8 (mulTarget 4)

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_mem_rationalLow_iff (theta : Fin 3) (p : ANF 8) : (anfPlaceNormalize theta) p ∈ rationalLowSpace ↔ p ∈ rationalLowSpace

def UnrestrictedBooleanMul.N4.ZeroNormalizedFirstJetState (C : Circuit 8 8) : Prop

The correlated first-jet state after moving its selected place to zero. The seed representative uses the very same linear form whose nonzero first-jet component was obtained in FirstJetSupport.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.zeroNormalizedFirstJetState {C : Circuit 8 8} (h : NormalizedEight C) : ZeroNormalizedFirstJetState C

noncomputable def UnrestrictedBooleanMul.N4.zeroFeedbackLowSpace : Submodule F₂ (ANF 8)

The degree-at-most-two state after the first feedback, in zero-place coordinates. The choice of tangent representative is immaterial modulo the rational place E₀.

Equations

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

theorem UnrestrictedBooleanMul.N4.zero_tangent_mem_feedbackLow (eps : F₂) : targetANF (rationalTangentAt 0 eps) ∈ zeroFeedbackLowSpace

theorem UnrestrictedBooleanMul.N4.exists_normalized_feedback_add_seed_of_mem_five {C : Circuit 8 8} (h : NormalizedEight C) {theta : Fin 3} {eps : F₂} (hflag : circuitFlag C 5 = circuitFlag C 4 ⊔ F₂ ∙ targetANF (rationalTangentAt theta eps)) {w : ANF 8} (hw : w ∈ circuitFlag C 5) : ∃ (low : ANF 8) (e : F₂), low ∈ zeroFeedbackLowSpace ∧ (anfPlaceNormalize theta) w = low + e • (anfPlaceNormalize theta) (C.gate 3)

Every wire in the fifth flag becomes a feedback-low wire plus at most one copy of the normalized seed.

theorem UnrestrictedBooleanMul.N4.feedbackCoeffRep_injective : Function.Injective feedbackCoeffRep

theorem UnrestrictedBooleanMul.N4.exists_feedbackLow_rep {p : ANF 8} (hp : p ∈ zeroFeedbackLowSpace) : ∃ (a : F₂) (ell : LinearForm) (q : FeedbackCoord), p = affineANF a ell + targetANF (feedbackCoeffRep q)

Concrete affine-plus-S representation of the feedback-low state.