Algebraic exclusion of the two quartic slice types

This file is the coordinate-free bookkeeping core of the manuscript's type-A/type-B slice argument. Its inputs are the cubic, quadratic, and linear coefficient equations on two distinct active slices. The proof uses only exterior products and the two support planes established in SliceGeometry; it does not enumerate circuits or Boolean functions.

def UnrestrictedBooleanMul.N4.sliceVaryingLinear (x y : F₂) : LinearForm

The linear slice variation induced by the two anchor values.

Equations

• UnrestrictedBooleanMul.N4.sliceVaryingLinear x y = x • UnrestrictedBooleanMul.N4.sliceBBar + y • UnrestrictedBooleanMul.N4.sliceABar

def UnrestrictedBooleanMul.N4.pointwiseLinearProduct (ell m : LinearForm) : LinearForm

Coordinatewise product of two linear coefficient vectors.

Equations

• UnrestrictedBooleanMul.N4.pointwiseLinearProduct ell m i = ell i * m i

def UnrestrictedBooleanMul.N4.sliceProductLinear (mu nu : F₂) (ell n base : LinearForm) (lambdaOne x y : F₂) : LinearForm

Linear part of (mu + ell) * (nu + n + Q), followed by the fixed correction and the r₁ slice variation.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.sliceTargetDifference (x y x' y' : F₂) : LinearForm

The difference in the target linear parts at two anchor assignments.

Equations

• UnrestrictedBooleanMul.N4.sliceTargetDifference x y x' y' = (y + y') • UnrestrictedBooleanMul.N4.sliceU + (x + x') • UnrestrictedBooleanMul.N4.sliceV

def UnrestrictedBooleanMul.N4.SliceQuadraticEquationA (mu : F₂) (ell n : LinearForm) (lambdaOne lambdaInfinity : F₂) : Prop

Vanishing of the type-A slice quadratic after its rational correction.

Equations

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

def UnrestrictedBooleanMul.N4.SliceQuadraticEquationB (mu : F₂) (ell n : LinearForm) (lambdaOne lambdaInfinity : F₂) : Prop

Vanishing of the type-B slice quadratic after its rational correction.

Equations

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

theorem UnrestrictedBooleanMul.N4.inSliceComplementPlane_zero : InSliceComplementPlane 0

theorem UnrestrictedBooleanMul.N4.InSliceComplementPlane.add {ell m : LinearForm} (hell : InSliceComplementPlane ell) (hm : InSliceComplementPlane m) : InSliceComplementPlane (ell + m)

theorem UnrestrictedBooleanMul.N4.InSliceComplementPlane.smul (a : F₂) {ell : LinearForm} (hell : InSliceComplementPlane ell) : InSliceComplementPlane (a • ell)

theorem UnrestrictedBooleanMul.N4.sliceABar_mem_complement_plane : InSliceComplementPlane sliceABar

theorem UnrestrictedBooleanMul.N4.sliceBBar_mem_complement_plane : InSliceComplementPlane sliceBBar

theorem UnrestrictedBooleanMul.N4.sliceVaryingLinear_mem (x y : F₂) : InSliceComplementPlane (sliceVaryingLinear x y)

theorem UnrestrictedBooleanMul.N4.pointwiseLinearProduct_mem {ell m : LinearForm} (hell : InSliceComplementPlane ell) (hm : InSliceComplementPlane m) : InSliceComplementPlane (pointwiseLinearProduct ell m)

Coordinatewise Boolean contraction preserves the complementary plane: the two generators have disjoint support and are idempotent.

theorem UnrestrictedBooleanMul.N4.sliceQuadratics_independent {a b : F₂} (h : a • sliceQuadraticA + b • sliceInfinityQuadratic = 0) : a = 0 ∧ b = 0

def UnrestrictedBooleanMul.N4.InSliceInfinityPlane (ell : LinearForm) : Prop

Membership in the two-input support of the infinity place.

Equations

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

theorem UnrestrictedBooleanMul.N4.sliceInfinityQuadratic_ne_zero : sliceInfinityQuadratic ≠ 0

theorem UnrestrictedBooleanMul.N4.sliceInfinityQuadratic_annihilator {ell : LinearForm} (h : vectorWedgeTwo ell sliceInfinityQuadratic = 0) : InSliceInfinityPlane ell

theorem UnrestrictedBooleanMul.N4.complement_infinity_plane_intersection {ell : LinearForm} (hc : InSliceComplementPlane ell) (hi : InSliceInfinityPlane ell) : ell = 0

theorem UnrestrictedBooleanMul.N4.vectorWedge_eq_typeA_plus_infinity_impossible {ell n : LinearForm} {a : F₂} (hell : InSliceComplementPlane ell) (hellNe : ell ≠ 0) (h : vectorWedge ell n = a • sliceQuadraticA + sliceInfinityQuadratic) : False

theorem UnrestrictedBooleanMul.N4.second_factor_mem_of_typeA_wedge {ell n : LinearForm} {a : F₂} (hell : InSliceComplementPlane ell) (hellNe : ell ≠ 0) (h : vectorWedge ell n = a • sliceQuadraticA) : InSliceComplementPlane n

theorem UnrestrictedBooleanMul.N4.add_ne_zero_of_ne_f2 {a b : F₂} (h : a ≠ b) : a + b ≠ 0

theorem UnrestrictedBooleanMul.N4.distinct_corner_target_difference_not_in_plane {x y x' y' : F₂} (h : x ≠ x' ∨ y ≠ y') : ¬InSliceComplementPlane (sliceTargetDifference x y x' y')

theorem UnrestrictedBooleanMul.N4.solve_typeB_quadratic {mu lambdaOne lambdaInfinity : F₂} (h : mu • sliceQuadraticB + lambdaOne • sliceQuadraticA + lambdaInfinity • sliceInfinityQuadratic = 0) : mu = lambdaOne ∧ mu = lambdaInfinity

theorem UnrestrictedBooleanMul.N4.solve_typeA_quadratic_zero_first {mu lambdaOne lambdaInfinity : F₂} (h : mu • sliceQuadraticA + lambdaOne • sliceQuadraticA + lambdaInfinity • sliceInfinityQuadratic = 0) : mu = lambdaOne ∧ lambdaInfinity = 0

theorem UnrestrictedBooleanMul.N4.sliceProductLinear_zero_first_cancel (mu nu lambdaOne x y : F₂) (n base m : LinearForm) (hmu : mu = lambdaOne) (hn : n = m + sliceVaryingLinear x y) : sliceProductLinear mu nu 0 n base lambdaOne x y = lambdaOne • m + base

theorem UnrestrictedBooleanMul.N4.sliceProductLinear_add_base_mem (mu nu lambdaOne x y : F₂) (ell n base : LinearForm) (hell : InSliceComplementPlane ell) (hn : InSliceComplementPlane n) : InSliceComplementPlane (sliceProductLinear mu nu ell n base lambdaOne x y + base)

theorem UnrestrictedBooleanMul.N4.no_typeB_active_slice_pair {x y x' y' mu mu' nu nu' lambdaOne lambdaInfinity : F₂} {ell m n n' base : LinearForm} (hdistinct : x ≠ x' ∨ y ≠ y') (hn : n = m + sliceVaryingLinear x y) (hn' : n' = m + sliceVaryingLinear x' y') (hcubic : vectorWedgeTwo ell sliceQuadraticB = 0) (hquad : SliceQuadraticEquationB mu ell n lambdaOne lambdaInfinity) (hquad' : SliceQuadraticEquationB mu' ell n' lambdaOne lambdaInfinity) (hlinear : sliceProductLinear mu nu ell n base lambdaOne x y + sliceProductLinear mu' nu' ell n' base lambdaOne x' y' = sliceTargetDifference x y x' y') : False

Type B: rank four kills the first complementary linear form, after which quadratic matching cancels every slice-varying linear term.

theorem UnrestrictedBooleanMul.N4.no_typeA_active_slice_pair {x y x' y' mu mu' quadMu quadMu' nu nu' lambdaOne lambdaInfinity : F₂} {ell m n n' base : LinearForm} (hdistinct : x ≠ x' ∨ y ≠ y') (hn : n = m + sliceVaryingLinear x y) (hn' : n' = m + sliceVaryingLinear x' y') (hcubic : vectorWedgeTwo ell sliceQuadraticA = 0) (hquad : SliceQuadraticEquationA quadMu ell n lambdaOne lambdaInfinity) (hquad' : SliceQuadraticEquationA quadMu' ell n' lambdaOne lambdaInfinity) (hquadMu : ell = 0 → quadMu = mu) (hquadMu' : ell = 0 → quadMu' = mu') (hlinear : sliceProductLinear mu nu ell n base lambdaOne x y + sliceProductLinear mu' nu' ell n' base lambdaOne x' y' = sliceTargetDifference x y x' y') : False

Type A: either the first complementary form is zero (constant-slice case), or quadratic matching puts both factor forms in the type-A support plane, so every slice difference stays in that plane.

def UnrestrictedBooleanMul.N4.SliceQuadraticEquationInfinity (mu : F₂) (ell n : LinearForm) (lambdaOne lambdaInfinity : F₂) : Prop

Vanishing of the infinity-type slice quadratic after its rational correction.

Equations

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

theorem UnrestrictedBooleanMul.N4.InSliceInfinityPlane.zero : InSliceInfinityPlane 0

theorem UnrestrictedBooleanMul.N4.InSliceInfinityPlane.add {ell m : LinearForm} (hell : InSliceInfinityPlane ell) (hm : InSliceInfinityPlane m) : InSliceInfinityPlane (ell + m)

theorem UnrestrictedBooleanMul.N4.InSliceInfinityPlane.smul (a : F₂) {ell : LinearForm} (hell : InSliceInfinityPlane ell) : InSliceInfinityPlane (a • ell)

theorem UnrestrictedBooleanMul.N4.pointwiseLinearProduct_infinity_mem {ell m : LinearForm} (hell : InSliceInfinityPlane ell) (hm : InSliceInfinityPlane m) : InSliceInfinityPlane (pointwiseLinearProduct ell m)

theorem UnrestrictedBooleanMul.N4.sliceUV_combination_not_in_infinity_plane (a b : F₂) (hne : a ≠ 0 ∨ b ≠ 0) : ¬InSliceInfinityPlane (a • sliceU + b • sliceV)

theorem UnrestrictedBooleanMul.N4.distinct_corner_target_difference_not_in_infinity_plane {x y x' y' : F₂} (h : x ≠ x' ∨ y ≠ y') : ¬InSliceInfinityPlane (sliceTargetDifference x y x' y')

theorem UnrestrictedBooleanMul.N4.solve_infinity_quadratic_zero_first {mu lambdaOne lambdaInfinity : F₂} (h : mu • sliceInfinityQuadratic + lambdaOne • sliceQuadraticA + lambdaInfinity • sliceInfinityQuadratic = 0) : lambdaOne = 0 ∧ mu = lambdaInfinity

theorem UnrestrictedBooleanMul.N4.vectorWedge_eq_infinity_plus_typeA_impossible {ell n : LinearForm} {a : F₂} (hell : InSliceInfinityPlane ell) (hellNe : ell ≠ 0) (h : vectorWedge ell n = sliceQuadraticA + a • sliceInfinityQuadratic) : False

theorem UnrestrictedBooleanMul.N4.second_factor_mem_of_infinity_wedge {ell n : LinearForm} {a : F₂} (hell : InSliceInfinityPlane ell) (hellNe : ell ≠ 0) (h : vectorWedge ell n = a • sliceInfinityQuadratic) : InSliceInfinityPlane n

theorem UnrestrictedBooleanMul.N4.sliceProductLinear_add_base_infinity_mem (mu nu x y : F₂) (ell n base : LinearForm) (hell : InSliceInfinityPlane ell) (hn : InSliceInfinityPlane n) : InSliceInfinityPlane (sliceProductLinear mu nu ell n base 0 x y + base)

theorem UnrestrictedBooleanMul.N4.no_typeInfinity_active_slice_pair {x y x' y' mu mu' quadMu quadMu' nu nu' lambdaOne lambdaInfinity : F₂} {ell n base : LinearForm} (hdistinct : x ≠ x' ∨ y ≠ y') (hcubic : vectorWedgeTwo ell sliceInfinityQuadratic = 0) (hquad : SliceQuadraticEquationInfinity quadMu ell n lambdaOne lambdaInfinity) (hquad' : SliceQuadraticEquationInfinity quadMu' ell n lambdaOne lambdaInfinity) (hquadMu : ell = 0 → quadMu = mu) (hquadMu' : ell = 0 → quadMu' = mu') (hlinear : sliceProductLinear mu nu ell n base lambdaOne x y + sliceProductLinear mu' nu' ell n base lambdaOne x' y' = sliceTargetDifference x y x' y') : False

The remaining singleton-at-infinity seed type is excluded directly, without appealing to a coordinate symmetry.