The first low--low collision

After the seed-using branch is excluded, the first useful suffix gate is a low--low product. This file first removes the remaining circuit bookkeeping: the useful target cannot arise from that product alone, so the old-state shift contains the cubic seed with coefficient one. Consequently the seed and the new low--low product have a genuinely non-rational quadratic collision in Aff + T.

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

A low-low child collides with a cubic seed modulo low terms to produce a new target.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.cubicLowLowCollision_of_firstUsefulChild {C : Circuit 8 8} (h : NormalizedEight C) {target child shift : ANF 8} (htarget : target ∈ targetAmbient 8 (mulTarget 4)) (htargetOld : target ∉ circuitFlag C 4) (hshift : shift ∈ circuitFlag C 4) (htargetEq : target = shift + child) (hchild : IsLowLowProduct child) : ∃ low ∈ rationalLowSpace, target ∉ rationalLowSpace ∧ target = low + C.gate 3 + child

Preserve the particular child and target when extracting the cubic-seed collision.

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

The first useful low-low child must cancel the seed high part.

def UnrestrictedBooleanMul.N4.CubicLowLowNormalCollisionAt (g target targetAffine : ANF 8) (targetCoeff : TargetCoeff) : Prop

Coordinate-ready form of the collision. The child has zero quartic probe, its cubic projection equals the nonzero seed cubic, and the surviving quadratic target coefficient is outside the rational-place span.

Equations

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

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

Existence of a target and affine correction in the normalized cubic low-low collision form.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.cubicLowLowNormalCollisionAt {C : Circuit 8 8} (h : NormalizedEight C) {child low target : ANF 8} (hchild : IsLowLowProduct child) (hlow : low ∈ rationalLowSpace) (htarget : target ∈ targetAmbient 8 (mulTarget 4)) (htargetNotLow : target ∉ rationalLowSpace) (htargetEq : target = low + C.gate 3 + child) : ∃ (targetAffine : ANF 8) (targetCoeff : TargetCoeff), CubicLowLowNormalCollisionAt (C.gate 3) target targetAffine targetCoeff

Normalize a fixed low-low collision without changing its target witness.

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

def UnrestrictedBooleanMul.N4.ExteriorFirstJetCollision : Prop

Exterior-coordinate data describing a cubic low-low collision at a first jet.

Equations

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

def UnrestrictedBooleanMul.N4.ExteriorFirstJetCollisionAt (g target targetAffine : ANF 8) (targetCoeff : TargetCoeff) : Prop

Exterior collision data retaining the seed projections and the particular target.

Equations

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

theorem UnrestrictedBooleanMul.N4.cubicLowLowNormalCollisionAt_exterior {g target targetAffine : ANF 8} {targetCoeff : TargetCoeff} (h : CubicLowLowNormalCollisionAt g target targetAffine targetCoeff) : ExteriorFirstJetCollisionAt g target targetAffine targetCoeff

Project a fixed collision to exterior coordinates, retaining its correlated witnesses.

theorem UnrestrictedBooleanMul.N4.NormalizedEight.exteriorFirstJetCollision {C : Circuit 8 8} (h : NormalizedEight C) : ExteriorFirstJetCollision

Existential exterior collision obtained from the correlated projection theorem.

theorem UnrestrictedBooleanMul.N4.rationalCubicDirectSum_eq_zero_of_cubic_equal (alpha beta : Fin 3 → F₂) (N N' : LinearForm) (hcubic : vectorWedgeTwo N (rationalTwo alpha) = vectorWedgeTwo N' (rationalTwo beta)) : (rationalCubicDirectSum fun (theta : Fin 3) => alpha theta • N + beta theta • N') = 0

Two equal cubic presentations yield a zero direct sum after addition in characteristic two.

theorem UnrestrictedBooleanMul.N4.contraction_sum_mem_rational_of_cubic_equal (alpha beta : Fin 3 → F₂) (N N' : LinearForm) (hcubic : vectorWedgeTwo N (rationalTwo alpha) = vectorWedgeTwo N' (rationalTwo beta)) : booleanContraction N (rationalTwo alpha) + booleanContraction N' (rationalTwo beta) ∈ rationalPlaceTwoSpace

The Boolean degree-lowering contractions attached to two equal rational cubic presentations differ only by a rational quadratic form. This is the coordinate-free role of the direct-sum kernel I₀ ⊕ I₁ ⊕ I∞.

def UnrestrictedBooleanMul.N4.ExteriorFirstJetReducedCollision : Prop

The reduced exterior-coordinate form of a first-jet collision.

Equations

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

theorem UnrestrictedBooleanMul.N4.exteriorFirstJetCollision_reduce_quadratic {seedCoeff childCoeff lowCoeff : Fin 3 → F₂} {seedLinear seedCompanion childLinear childCompanion : LinearForm} {seedRho childRho : F₂} {targetCoeff : TargetCoeff} (hcubic : vectorWedgeTwo seedLinear (rationalTwo seedCoeff) = vectorWedgeTwo childLinear (rationalTwo childCoeff)) (hquadratic : targetTwo targetCoeff = rationalTwo lowCoeff + (seedRho • rationalTwo seedCoeff + vectorWedge seedCompanion seedLinear + booleanContraction seedLinear (rationalTwo seedCoeff)) + (childRho • rationalTwo childCoeff + vectorWedge childCompanion childLinear + booleanContraction childLinear (rationalTwo childCoeff))) : ∃ (rationalCoeff : Fin 3 → F₂), targetTwo targetCoeff = rationalTwo rationalCoeff + vectorWedge seedCompanion seedLinear + vectorWedge childCompanion childLinear

Equal cubic parts make the Boolean contractions rational, preserving all linear witnesses.

theorem UnrestrictedBooleanMul.N4.exteriorFirstJetCollision_reduced (h : ExteriorFirstJetCollision) : ExteriorFirstJetReducedCollision

def UnrestrictedBooleanMul.N4.InPlaceSupport (theta : Fin 3) (u : LinearForm) : Prop

A linear form lies in the two-input support of a rational place.

Equations

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

theorem UnrestrictedBooleanMul.N4.cubic_equal_support_relation (alpha beta : Fin 3 → F₂) (N N' : LinearForm) (hcubic : vectorWedgeTwo N (rationalTwo alpha) = vectorWedgeTwo N' (rationalTwo beta)) (theta : Fin 3) : InPlaceSupport theta (alpha theta • N + beta theta • N')

theorem UnrestrictedBooleanMul.N4.place_supports_disjoint {theta phi : Fin 3} (hne : theta ≠ phi) {u : LinearForm} (htheta : InPlaceSupport theta u) (hphi : InPlaceSupport phi u) : u = 0

theorem UnrestrictedBooleanMul.N4.target_rational_of_distinct_place_wedges {theta phi : Fin 3} (hne : theta ≠ phi) {N N' z w : LinearForm} {gamma : Fin 3 → F₂} {c : TargetCoeff} (hN : InPlaceSupport theta N) (hN' : InPlaceSupport phi N') (htarget : targetTwo c = rationalTwo gamma + vectorWedge z N + vectorWedge w N') : IsRationalCoeff c

theorem UnrestrictedBooleanMul.N4.target_rational_of_same_second_wedge {N z w : LinearForm} {gamma : Fin 3 → F₂} {c : TargetCoeff} (htarget : targetTwo c = rationalTwo gamma + vectorWedge z N + vectorWedge w N) : IsRationalCoeff c

theorem UnrestrictedBooleanMul.N4.target_rational_of_support_and_sum_support {theta phi : Fin 3} (hne : theta ≠ phi) {N N' z w : LinearForm} {gamma : Fin 3 → F₂} {c : TargetCoeff} (hN : InPlaceSupport theta N) (hsum : InPlaceSupport phi (N + N')) (htarget : targetTwo c = rationalTwo gamma + vectorWedge z N + vectorWedge w N') : IsRationalCoeff c

theorem UnrestrictedBooleanMul.N4.target_rational_of_support_and_sum_support_right {theta phi : Fin 3} (hne : theta ≠ phi) {N N' z w : LinearForm} {gamma : Fin 3 → F₂} {c : TargetCoeff} (hN' : InPlaceSupport theta N') (hsum : InPlaceSupport phi (N + N')) (htarget : targetTwo c = rationalTwo gamma + vectorWedge z N + vectorWedge w N') : IsRationalCoeff c

@[simp]

theorem UnrestrictedBooleanMul.N4.rationalSingleton_apply_self (theta : Fin 3) : rationalSingleton theta theta = 1

theorem UnrestrictedBooleanMul.N4.rationalSingleton_apply_ne {theta phi : Fin 3} (hne : phi ≠ theta) : rationalSingleton theta phi = 0

theorem UnrestrictedBooleanMul.N4.cubic_collision_forces_common_singleton (alpha beta : Fin 3 → F₂) (N N' z w : LinearForm) (gamma : Fin 3 → F₂) (c : TargetCoeff) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hcubic : vectorWedgeTwo N (rationalTwo alpha) = vectorWedgeTwo N' (rationalTwo beta)) (htargetNonrational : ¬IsRationalCoeff c) (htarget : targetTwo c = rationalTwo gamma + vectorWedge z N + vectorWedge w N') : ∃ (theta : Fin 3), alpha = rationalSingleton theta ∧ beta = rationalSingleton theta

Non-rationality leaves only a common singleton rational place in the two equal cubic presentations. The proof uses the three direct-sum support relations and the support-pair separators; it does not enumerate coefficient words.