Algebraic ANF models for zero-place slices

The quartic exclusion compares restrictions to the six variables outside a₀,b₀. These models keep the six complementary variables in their original eight-coordinate positions and set the two anchor coefficients to zero. This lets the homogeneous projections already used by the exterior argument apply without introducing a second ANF type or enumerating Boolean functions.

noncomputable def UnrestrictedBooleanMul.N4.sliceComplementLinear (ell : LinearForm) : LinearForm

Remove the two anchor coordinates from a linear form.

Equations

• UnrestrictedBooleanMul.N4.sliceComplementLinear ell = ell + ell 0 • UnrestrictedBooleanMul.N4.sliceX + ell 4 • UnrestrictedBooleanMul.N4.sliceY

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

Evaluate the anchor-supported part of a linear form at fixed anchor values.

Equations

• UnrestrictedBooleanMul.N4.sliceAnchorValue ell x y = ell 0 * x + ell 4 * y

noncomputable def UnrestrictedBooleanMul.N4.sliceQuadraticAANF : ANF 8

The ANF product of the two complementary evaluation-at-one directions.

Equations

• UnrestrictedBooleanMul.N4.sliceQuadraticAANF = UnrestrictedBooleanMul.N4.linearANF UnrestrictedBooleanMul.N4.sliceABar * UnrestrictedBooleanMul.N4.linearANF UnrestrictedBooleanMul.N4.sliceBBar

noncomputable def UnrestrictedBooleanMul.N4.sliceInfinityQuadraticANF : ANF 8

The product of the two leading input coefficients.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.sliceQuadraticBANF : ANF 8

The sum of the complementary evaluation-at-one and infinity products.

Equations

• UnrestrictedBooleanMul.N4.sliceQuadraticBANF = UnrestrictedBooleanMul.N4.sliceQuadraticAANF + UnrestrictedBooleanMul.N4.sliceInfinityQuadraticANF

noncomputable def UnrestrictedBooleanMul.N4.sliceZeroFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) : ANF 8

Restrict an affine factor plus the zero-place product to an anchor slice.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.sliceOneFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) : ANF 8

Restrict an affine factor plus the evaluation-at-one product to an anchor slice.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.sliceInfinityFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) : ANF 8

Restrict an affine factor plus the infinity-place product to an anchor slice.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.sliceTypeBFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) : ANF 8

Restrict an affine factor with type-B quadratic part to an anchor slice.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.sliceCorrectionModel (a : F₂) (ell : LinearForm) (alpha : Fin 3 → F₂) (x y : F₂) : ANF 8

Restrict an affine-plus-rational-target correction to an anchor slice.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.sliceTangentModel (a : F₂) (ell : LinearForm) (eps x y : F₂) : ANF 8

Restrict an affine perturbation of a first-jet tangent target to an anchor slice.

Equations

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

def UnrestrictedBooleanMul.N4.sliceComplementOf (w : Fin 8 → F₂) : Fin 6 → F₂

Extract the six non-anchor input coordinates.

Equations

• UnrestrictedBooleanMul.N4.sliceComplementOf w = ![w 1, w 2, w 3, w 5, w 6, w 7]

theorem UnrestrictedBooleanMul.N4.sliceAssignment_complementOf (x y : F₂) (w : Fin 8 → F₂) : sliceAssignment x y (sliceComplementOf w) = ![x, w 1, w 2, w 3, y, w 5, w 6, w 7]

@[simp]

theorem UnrestrictedBooleanMul.N4.sliceComplementLinear_anchor_zero (ell : LinearForm) : sliceComplementLinear ell 0 = 0 ∧ sliceComplementLinear ell 4 = 0

theorem UnrestrictedBooleanMul.N4.sliceComplementLinear_other (ell : LinearForm) (i : Fin 8) (hi0 : i ≠ 0) (hi4 : i ≠ 4) : sliceComplementLinear ell i = ell i

@[simp]

theorem UnrestrictedBooleanMul.N4.eval_linearANF_formula (ell : LinearForm) (w : Fin 8 → F₂) : eval (linearANF ell) w = ∑ i : Fin 8, ell i * w i

@[simp]

theorem UnrestrictedBooleanMul.N4.eval_affineANF_formula (a : F₂) (ell : LinearForm) (w : Fin 8 → F₂) : eval (affineANF a ell) w = a + ∑ i : Fin 8, ell i * w i

theorem UnrestrictedBooleanMul.N4.eval_linearANF_slice (ell : LinearForm) (x y : F₂) (z : Fin 6 → F₂) : eval (linearANF ell) (sliceAssignment x y z) = sliceAnchorValue ell x y + eval (linearANF (sliceComplementLinear ell)) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.eval_affineANF_slice (a : F₂) (ell : LinearForm) (x y : F₂) (z : Fin 6 → F₂) : eval (affineANF a ell) (sliceAssignment x y z) = eval (affineANF (a + sliceAnchorValue ell x y) (sliceComplementLinear ell)) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.eval_rationalANF_slice (alpha : Fin 3 → F₂) (x y : F₂) (z : Fin 6 → F₂) : eval (rationalANF alpha) (sliceAssignment x y z) = alpha 0 * x * y + alpha 1 * (x + eval (linearANF sliceABar) (sliceAssignment x y z)) * (y + eval (linearANF sliceBBar) (sliceAssignment x y z)) + alpha 2 * eval (linearANF (placeA 2)) (sliceAssignment x y z) * eval (linearANF (placeB 2)) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.eval_affineANF_linear_add (a : F₂) (ell m : LinearForm) (w : Fin 8 → F₂) : eval (affineANF a (ell + m)) w = eval (affineANF a ell) w + eval (linearANF m) w

theorem UnrestrictedBooleanMul.N4.eval_affineANF_const_add (a b : F₂) (ell : LinearForm) (w : Fin 8 → F₂) : eval (affineANF (a + b) ell) w = b + eval (affineANF a ell) w

theorem UnrestrictedBooleanMul.N4.eval_linearANF_sliceVarying (x y : F₂) (w : Fin 8 → F₂) : eval (linearANF (sliceVaryingLinear x y)) w = x * eval (linearANF sliceBBar) w + y * eval (linearANF sliceABar) w

@[simp]

theorem UnrestrictedBooleanMul.N4.eval_sliceQuadraticAANF (w : Fin 8 → F₂) : eval sliceQuadraticAANF w = eval (linearANF sliceABar) w * eval (linearANF sliceBBar) w

@[simp]

theorem UnrestrictedBooleanMul.N4.eval_sliceInfinityQuadraticANF (w : Fin 8 → F₂) : eval sliceInfinityQuadraticANF w = eval (linearANF (placeA 2)) w * eval (linearANF (placeB 2)) w

@[simp]

theorem UnrestrictedBooleanMul.N4.eval_sliceQuadraticBANF (w : Fin 8 → F₂) : eval sliceQuadraticBANF w = eval sliceQuadraticAANF w + eval sliceInfinityQuadraticANF w

theorem UnrestrictedBooleanMul.N4.eval_representedLowFactor_slice (a : F₂) (ell : LinearForm) (alpha : Fin 3 → F₂) (x y : F₂) (z : Fin 6 → F₂) : eval (representedLowFactor a ell alpha) (sliceAssignment x y z) = eval (affineANF (a + sliceAnchorValue ell x y) (sliceComplementLinear ell)) (sliceAssignment x y z) + eval (rationalANF alpha) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.eval_sliceZeroFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) (z : Fin 6 → F₂) : eval (sliceZeroFactorModel a ell x y) (sliceAssignment x y z) = eval (representedLowFactor a ell (rationalSingleton 0)) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.eval_sliceOneFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) (z : Fin 6 → F₂) : eval (sliceOneFactorModel a ell x y) (sliceAssignment x y z) = eval (representedLowFactor a ell (rationalSingleton 1)) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.eval_sliceInfinityFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) (z : Fin 6 → F₂) : eval (sliceInfinityFactorModel a ell x y) (sliceAssignment x y z) = eval (representedLowFactor a ell (rationalSingleton 2)) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.eval_sliceTypeBFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) (z : Fin 6 → F₂) : eval (sliceTypeBFactorModel a ell x y) (sliceAssignment x y z) = eval (representedLowFactor a ell (rationalSingleton 1 + rationalSingleton 2)) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.eval_sliceCorrectionModel (a : F₂) (ell : LinearForm) (alpha : Fin 3 → F₂) (x y : F₂) (z : Fin 6 → F₂) : eval (sliceCorrectionModel a ell alpha x y) (sliceAssignment x y z) = eval (representedLowFactor a ell alpha) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.eval_sliceTangentModel (a : F₂) (ell : LinearForm) (eps x y : F₂) (z : Fin 6 → F₂) : eval (sliceTangentModel a ell eps x y) (sliceAssignment x y z) = eval (affineANF a ell + targetANF (rationalTangentAt 0 eps)) (sliceAssignment x y z)

def UnrestrictedBooleanMul.N4.AnchorsIndependent (p : ANF 8) : Prop

The Boolean function is unchanged when either anchor input is reassigned.

Equations

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

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_linearANF {ell : LinearForm} (h0 : ell 0 = 0) (h4 : ell 4 = 0) : AnchorsIndependent (linearANF ell)

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_affineANF (a : F₂) {ell : LinearForm} (h0 : ell 0 = 0) (h4 : ell 4 = 0) : AnchorsIndependent (affineANF a ell)

theorem UnrestrictedBooleanMul.N4.AnchorsIndependent.add {p q : ANF 8} (hp : AnchorsIndependent p) (hq : AnchorsIndependent q) : AnchorsIndependent (p + q)

theorem UnrestrictedBooleanMul.N4.AnchorsIndependent.mul {p q : ANF 8} (hp : AnchorsIndependent p) (hq : AnchorsIndependent q) : AnchorsIndependent (p * q)

theorem UnrestrictedBooleanMul.N4.AnchorsIndependent.smul (a : F₂) {p : ANF 8} (hp : AnchorsIndependent p) : AnchorsIndependent (a • p)

theorem UnrestrictedBooleanMul.N4.sliceABar_anchor_zero : sliceABar 0 = 0 ∧ sliceABar 4 = 0

theorem UnrestrictedBooleanMul.N4.sliceBBar_anchor_zero : sliceBBar 0 = 0 ∧ sliceBBar 4 = 0

theorem UnrestrictedBooleanMul.N4.sliceInfinityA_anchor_zero : placeA 2 0 = 0 ∧ placeA 2 4 = 0

theorem UnrestrictedBooleanMul.N4.sliceInfinityB_anchor_zero : placeB 2 0 = 0 ∧ placeB 2 4 = 0

theorem UnrestrictedBooleanMul.N4.sliceU_anchor_zero : sliceU 0 = 0 ∧ sliceU 4 = 0

theorem UnrestrictedBooleanMul.N4.sliceV_anchor_zero : sliceV 0 = 0 ∧ sliceV 4 = 0

theorem UnrestrictedBooleanMul.N4.sliceVaryingLinear_anchor_zero (x y : F₂) : sliceVaryingLinear x y 0 = 0 ∧ sliceVaryingLinear x y 4 = 0

theorem UnrestrictedBooleanMul.N4.sliceComplementLinear_anchor_zero_separate (ell : LinearForm) : sliceComplementLinear ell 0 = 0 ∧ sliceComplementLinear ell 4 = 0

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceZeroFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) : AnchorsIndependent (sliceZeroFactorModel a ell x y)

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceOneFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) : AnchorsIndependent (sliceOneFactorModel a ell x y)

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceInfinityFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) : AnchorsIndependent (sliceInfinityFactorModel a ell x y)

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceTypeBFactorModel (a : F₂) (ell : LinearForm) (x y : F₂) : AnchorsIndependent (sliceTypeBFactorModel a ell x y)

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceCorrectionModel (a : F₂) (ell : LinearForm) (alpha : Fin 3 → F₂) (x y : F₂) : AnchorsIndependent (sliceCorrectionModel a ell alpha x y)

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceTangentModel (a : F₂) (ell : LinearForm) (eps x y : F₂) : AnchorsIndependent (sliceTangentModel a ell eps x y)

theorem UnrestrictedBooleanMul.N4.eval_eq_of_slice_eq {p q : ANF 8} {x y : F₂} (hp : AnchorsIndependent p) (hq : AnchorsIndependent q) (h : ∀ (z : Fin 6 → F₂), eval p (sliceAssignment x y z) = eval q (sliceAssignment x y z)) (w : Fin 8 → F₂) : eval p w = eval q w