Saturation after the first feedback

This file returns from the homogeneous algebra to the normalized circuit. Every input of gate six is a feedback-low wire plus one Boolean multiple of the normalized seed. Boolean idempotence reduces their product, modulo that state, to exactly the two algebraic types excluded in SecondFeedbackUsing and SecondFeedbackHigh.

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

The zero-place feedback space enlarged by one seed ANF.

Equations

• UnrestrictedBooleanMul.N4.normalizedFeedbackState g = UnrestrictedBooleanMul.N4.zeroFeedbackLowSpace ⊔ UnrestrictedBooleanMul.F₂ ∙ g

def UnrestrictedBooleanMul.N4.IsFeedbackLowLowProduct (f : ANF 8) : Prop

A product of two ANFs in the zero-place feedback space.

Equations

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

def UnrestrictedBooleanMul.N4.IsNormalizedSeedUsingProduct (g f : ANF 8) : Prop

A product of a seed plus a feedback-low term with another feedback-low term.

Equations

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

theorem UnrestrictedBooleanMul.N4.exists_feedback_add_seed_of_mem_normalizedFeedbackState {g w : ANF 8} (hw : w ∈ normalizedFeedbackState g) : ∃ (low : ANF 8) (e : F₂), low ∈ zeroFeedbackLowSpace ∧ w = low + e • g

theorem UnrestrictedBooleanMul.N4.normalize_feedback_state_product {g l r : ANF 8} (hl : l ∈ normalizedFeedbackState g) (hr : r ∈ normalizedFeedbackState g) : ∃ (f : ANF 8), ∃ s ∈ normalizedFeedbackState g, l * r = s + f ∧ (IsFeedbackLowLowProduct f ∨ IsNormalizedSeedUsingProduct g f)

Product normalization inside the post-jet state. This is the same four-case Boolean identity as the seed-state normalization, now over the larger feedback-low subspace.

theorem UnrestrictedBooleanMul.N4.normalizedFeedbackLow_pullback_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)) {p : ANF 8} (hp : p ∈ zeroFeedbackLowSpace) : (anfPlaceNormalize theta) p ∈ circuitFlag C 5

A zero-place feedback-low vector pulled back by the involutive place change is already present before gate six.

theorem UnrestrictedBooleanMul.N4.normalized_targetWitness_not_feedbackLow {C : Circuit 8 8} (h : NormalizedEight C) {theta : Fin 3} {eps : F₂} (hflag : circuitFlag C 5 = circuitFlag C 4 ⊔ F₂ ∙ targetANF (rationalTangentAt theta eps)) {t : ANF 8} (ht : t ∉ circuitFlag C 5) : (anfPlaceNormalize theta) t ∉ zeroFeedbackLowSpace

theorem UnrestrictedBooleanMul.N4.zeroFeedbackLow_mem_targetAmbient {p : ANF 8} (hp : p ∈ zeroFeedbackLowSpace) : p ∈ targetAmbient 8 (mulTarget 4)

theorem UnrestrictedBooleanMul.N4.NormalizedEight.gateSix_not_useful {C : Circuit 8 8} (h : NormalizedEight C) : ¬UsefulAt C (mulTarget 4) 5

Gate six cannot be useful after the normalized first feedback. The proof contains no circuit enumeration: it uses the flag decomposition once, then the two algebraic second-feedback exclusions.