Cubic seed and first-feedback interfaces

After quartic exclusion the normalized seed is the product of two rational-low factors with dependent quadratic parts. This file packages the resulting exterior normal form at circuit level. The package records both homogeneous parts needed later: the nonzero anchored cubic N ∧ G and its Boolean quadratic companion ρ G + z ∧ N + κ_G(N).

No circuit configurations are enumerated here; the proof is obtained from the three algebraic dependency cases in low_product_quadratic_normal_form.

def UnrestrictedBooleanMul.N4.CubicSeedNormalForm (g : ANF 8) : Prop

Complete homogeneous normal form of a cubic seed arising from the normalized rational prefix.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.cubicSeedNormalForm {C : Circuit 8 8} (h : NormalizedEight C) : CubicSeedNormalForm (C.gate 3)

The normalized seed has the manuscript's anchored cubic normal form and the matching quadratic shadow.

theorem UnrestrictedBooleanMul.N4.degreeLE_two_of_degreeLE_three_of_cubic_zero {p : ANF 8} (hp : DegreeLE 3 p) (hcubic : anfThreeProjection p = 0) : DegreeLE 2 p

A degree-three ANF with zero cubic homogeneous part is in fact of degree at most two.

theorem UnrestrictedBooleanMul.N4.mem_affine_of_degreeLE_two_of_twoProjection_zero {p : ANF 8} (hp : DegreeLE 2 p) (htwo : anfTwoProjection p = 0) : p ∈ affine 8

Coefficient reconstruction in degrees zero and one.

theorem UnrestrictedBooleanMul.N4.mem_rationalLow_of_degreeLE_two_of_twoProjection_mem {p : ANF 8} (hp : DegreeLE 2 p) (htwo : anfTwoProjection p ∈ rationalPlaceTwoSpace) : p ∈ rationalLowSpace

A degree-at-most-two ANF whose quadratic shadow is in the rational-place span belongs to the rational-low state Aff + R.

def UnrestrictedBooleanMul.N4.CubicSeedAnchoredForm (g : ANF 8) : Prop

The manuscript's seed-coset representative M (z + G), with all lower terms absorbed into Aff + R.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.cubicSeedAnchoredForm {C : Circuit 8 8} (h : NormalizedEight C) : CubicSeedAnchoredForm (C.gate 3)

Upgrade the homogeneous seed normal form to an equality modulo the rational-low state.

theorem UnrestrictedBooleanMul.N4.anfQuinticAnchorProbe_mul_target_congr_of_cubic {p q : ANF 8} (hp : DegreeLE 3 p) (hq : DegreeLE 3 q) (hcubic : anfThreeProjection p = anfThreeProjection q) (c : TargetCoeff) : anfQuinticAnchorProbe (p * targetANF c) = anfQuinticAnchorProbe (q * targetANF c)

Multiplication by a quadratic target sees only the cubic homogeneous part in degree five.

def UnrestrictedBooleanMul.N4.SeedUsingCubicClassifiedFormAt (g : ANF 8) (theta : Fin 3) : Prop

Classified algebraic output of a seed-using useful child at a specified rational place. Indexing by the place keeps every later normalization tied to the very same feedback witness.

Equations

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

def UnrestrictedBooleanMul.N4.SeedUsingCubicClassifiedForm (g : ANF 8) : Prop

Classified algebraic output of a seed-using useful child after quartic exclusion. Right idempotence makes the low factor a rational singleton and the new target its first tangent.

Equations

• UnrestrictedBooleanMul.N4.SeedUsingCubicClassifiedForm g = ∃ (theta : Fin 3), UnrestrictedBooleanMul.N4.SeedUsingCubicClassifiedFormAt g theta

theorem UnrestrictedBooleanMul.N4.NormalizedEight.seedUsingCubicClassifiedForm_of_child {C : Circuit 8 8} (h : NormalizedEight C) {target representative shift : ANF 8} (htarget : target ∈ targetAmbient 8 (mulTarget 4)) (htargetOld : target ∉ circuitFlag C 4) (hshift : shift ∈ circuitFlag C 4) (htargetEq : target = shift + representative) (hseedUsing : IsSeedUsingProduct (C.gate 3) representative) : SeedUsingCubicClassifiedForm (C.gate 3)

A seed-using branch of the first useful child has the classified cubic feedback form.

theorem UnrestrictedBooleanMul.N4.cubic_anchor_zero_of_left_idempotence {g correction target : ANF 8} {targetConst eps : F₂} {targetLinear anchorLinear : LinearForm} {anchorCoeff : Fin 3 → F₂} (hg : DegreeLE 3 g) (hcubic : anfThreeProjection g = vectorWedgeTwo anchorLinear (rationalTwo anchorCoeff)) (hcorrection : correction ∈ rationalLowSpace) (htarget : target = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps)) (hleft : (g + correction) * target = target) : vectorWedgeTwo anchorLinear (rationalTwo anchorCoeff) = vectorWedgeTwo (anchorCoeff 0 • anchorLinear) (rationalPlaceTwo 0)

Degree five in the left idempotence identity forces a rational cubic to share the zero-place anchor of a tangent target.

theorem UnrestrictedBooleanMul.N4.normalizePlaceLinear_involutive (theta : Fin 3) (ell : LinearForm) : normalizePlaceLinear theta (normalizePlaceLinear theta ell) = ell

The three place-normalizing changes of variables are involutions on linear forms.

theorem UnrestrictedBooleanMul.N4.normalizeRationalCoeff_involutive (theta : Fin 3) (alpha : Fin 3 → F₂) : normalizeRationalCoeff theta (normalizeRationalCoeff theta alpha) = alpha

The corresponding permutation of rational-place coefficients is also an involution.

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_mem_rationalLow (theta : Fin 3) {p : ANF 8} (hp : p ∈ rationalLowSpace) : (anfPlaceNormalize theta) p ∈ rationalLowSpace

Place normalization preserves the rational-low state.

theorem UnrestrictedBooleanMul.N4.normalized_anchored_cubic_ne_zero (theta : Fin 3) (ell : LinearForm) (alpha : Fin 3 → F₂) (hnonzero : vectorWedgeTwo ell (rationalTwo alpha) ≠ 0) : vectorWedgeTwo (normalizePlaceLinear theta ell) (rationalTwo (normalizeRationalCoeff theta alpha)) ≠ 0

Nonzero anchored rational cubics remain nonzero under place normalization. The proof uses involutivity and rational-low reconstruction, not a rank computation.

def UnrestrictedBooleanMul.N4.NormalizedCubicAnchorFormAt (theta : Fin 3) (g : ANF 8) : Prop

Seed data after normalizing the specified classified feedback place to zero.

Equations

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

def UnrestrictedBooleanMul.N4.NormalizedCubicAnchorForm (g : ANF 8) : Prop

The normalized cubic anchor form holds at some rational place.

Equations

• UnrestrictedBooleanMul.N4.NormalizedCubicAnchorForm g = ∃ (theta : Fin 3), UnrestrictedBooleanMul.N4.NormalizedCubicAnchorFormAt theta g

theorem UnrestrictedBooleanMul.N4.seedUsingCubicClassified_normalized_anchor_at {g : ANF 8} {theta : Fin 3} (hseed : CubicSeedAnchoredForm g) (hfeedback : SeedUsingCubicClassifiedFormAt g theta) : NormalizedCubicAnchorFormAt theta g

A classified seed-using feedback forces the normalized seed cubic to be anchored at the feedback place.

theorem UnrestrictedBooleanMul.N4.seedUsingCubicClassified_normalized_anchor {g : ANF 8} (hseed : CubicSeedAnchoredForm g) (hfeedback : SeedUsingCubicClassifiedForm g) : NormalizedCubicAnchorForm g

def UnrestrictedBooleanMul.N4.ZeroAnchoredCubicSeedForm (g : ANF 8) : Prop

Canonical zero-place representative of the seed coset.

Equations

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

theorem UnrestrictedBooleanMul.N4.normalizedCubicAnchorForm_zeroRepresentative_at {g : ANF 8} {theta : Fin 3} (h : NormalizedCubicAnchorFormAt theta g) : ZeroAnchoredCubicSeedForm ((anfPlaceNormalize theta) g)

Extra rational-place components in an anchored cubic contribute only a rational-low correction, so the seed coset has the canonical M(z+E₀) representative.

theorem UnrestrictedBooleanMul.N4.normalizedCubicAnchorForm_zeroRepresentative {g : ANF 8} (h : NormalizedCubicAnchorForm g) : ∃ (theta : Fin 3), ZeroAnchoredCubicSeedForm ((anfPlaceNormalize theta) g)

theorem UnrestrictedBooleanMul.N4.NormalizedEight.seedUsingFirstFeedback_zeroAnchor {C : Circuit 8 8} (h : NormalizedEight C) {target representative shift : ANF 8} (htarget : target ∈ targetAmbient 8 (mulTarget 4)) (htargetOld : target ∉ circuitFlag C 4) (hshift : shift ∈ circuitFlag C 4) (htargetEq : target = shift + representative) (hseedUsing : IsSeedUsingProduct (C.gate 3) representative) : ∃ (theta : Fin 3), ZeroAnchoredCubicSeedForm ((anfPlaceNormalize theta) (C.gate 3))

Circuit-level endpoint of the cubic annihilator/degree-five argument for a seed-using first child.