Rational-prefix rigidity

This file proves the algebraic core of the manuscript's prefix proposition. If two wires have quadratic parts in the three rational-place space and their product has no cubic or quartic part, then any target quadratic shadow of that product is again in the rational-place space. No circuit enumeration is used.

theorem UnrestrictedBooleanMul.N4.targetTwo_rationalPlaceCoeff (θ : Fin 3) : targetTwo (rationalPlaceCoeff θ) = rationalPlaceTwo θ

theorem UnrestrictedBooleanMul.N4.rationalPlaceTwo_ne_zero (θ : Fin 3) : rationalPlaceTwo θ ≠ 0

theorem UnrestrictedBooleanMul.N4.rationalPlaceTwo_mem (θ : Fin 3) : rationalPlaceTwo θ ∈ rationalPlaceTwoSpace

theorem UnrestrictedBooleanMul.N4.rationalTwo_mem (γ : Fin 3 → F₂) : rationalTwo γ ∈ rationalPlaceTwoSpace

theorem UnrestrictedBooleanMul.N4.rationalPlaceTwoSpace_le_targetTwoSpace : rationalPlaceTwoSpace ≤ targetTwoSpace

theorem UnrestrictedBooleanMul.N4.rational_contraction_mem_of_cubic_zero (γ : Fin 3 → F₂) (N : LinearForm) (h : vectorWedgeTwo N (rationalTwo γ) = 0) : booleanContraction N (rationalTwo γ) ∈ rationalPlaceTwoSpace

A vanishing rational cubic contraction has only a rational quadratic degree-lowering shadow.

theorem UnrestrictedBooleanMul.N4.coeff_mem_rational_of_targetTwo_mem {c : TargetCoeff} (hc : targetTwo c ∈ rationalPlaceTwoSpace) : c ∈ rationalCoeffSpace

Recover rational Hankel coefficients from membership of the exterior two-form in the rational-place span.

theorem UnrestrictedBooleanMul.N4.exterior_prefix_rigidity (a b : F₂) (ell m : LinearForm) (α β : Fin 3 → F₂) (c : TargetCoeff) (hquartic : wedgeTwo (rationalTwo α) (rationalTwo β) = 0) (hcubic : rationalProductCubic ell m α β = 0) (hquadratic : targetTwo c = rationalProductQuadratic a b ell m α β) : c ∈ rationalCoeffSpace

Exterior prefix rigidity. The hypotheses are precisely the quartic, cubic, and quadratic homogeneous equations for a low product landing in the target space.