Homogeneous projections of the slice models

These lemmas calculate only the degree-three, degree-two, and degree-one parts used by the manuscript. The fixed coordinate checks concern the two explicit complementary quadratics; there is no search over circuits or Boolean functions.

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_linearANF (ell : LinearForm) : anfLinearProjection (linearANF ell) = ell

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_affineANF (a : F₂) (ell : LinearForm) : anfLinearProjection (affineANF a ell) = ell

theorem UnrestrictedBooleanMul.N4.eval_linearANF_supportAssignment (ell : LinearForm) (t : Finset (Fin 8)) : eval (linearANF ell) (supportAssignment t) = ∑ i ∈ t, ell i

noncomputable def UnrestrictedBooleanMul.N4.singlePolarMap (i : Fin 8) : ANF 8 →ₗ[F₂] F₂

The first finite difference at zero in one coordinate direction.

Equations

• UnrestrictedBooleanMul.N4.singlePolarMap i = UnrestrictedBooleanMul.N4.sparseEvalMap ∅ + UnrestrictedBooleanMul.N4.sparseEvalMap {i}

def UnrestrictedBooleanMul.N4.singleCoeffMap (i : Fin 8) : ANF 8 →ₗ[F₂] F₂

Extract the coefficient of one linear monomial.

Equations

• UnrestrictedBooleanMul.N4.singleCoeffMap i = { toFun := fun (p : UnrestrictedBooleanMul.ANF 8) => p.coeff { vars := {i} }, map_add' := ⋯, map_smul' := ⋯ }

theorem UnrestrictedBooleanMul.N4.singlePolarMap_eq_singleCoeffMap (i : Fin 8) : singlePolarMap i = singleCoeffMap i

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_congr_of_eval_eq {p q : ANF 8} (h : ∀ (x : Fin 8 → F₂), eval p x = eval q x) : anfLinearProjection p = anfLinearProjection q

Equality of Boolean functions determines the homogeneous linear projection.

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_linear_mul_linear (ell m : LinearForm) : anfLinearProjection (linearANF ell * linearANF m) = pointwiseLinearProduct ell m

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_affine_mul_affine (a b : F₂) (ell m : LinearForm) : anfLinearProjection (affineANF a ell * affineANF b m) = a • m + b • ell + pointwiseLinearProduct ell m

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_linear_mul_quadratic (ell m n : LinearForm) : anfThreeProjection (linearANF ell * (linearANF m * linearANF n)) = vectorWedgeTwo ell (vectorWedge m n)

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_linear_mul_sliceQuadraticA (ell : LinearForm) : anfThreeProjection (linearANF ell * sliceQuadraticAANF) = vectorWedgeTwo ell sliceQuadraticA

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_linear_mul_sliceInfinityQuadratic (ell : LinearForm) : anfThreeProjection (linearANF ell * sliceInfinityQuadraticANF) = vectorWedgeTwo ell sliceInfinityQuadratic

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_linear_mul_quadratic (ell m n : LinearForm) (hdisjoint : pointwiseLinearProduct m n = 0) : anfTwoProjection (linearANF ell * (linearANF m * linearANF n)) = booleanContraction ell (vectorWedge m n)

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_linear_mul_quadratic (ell m n : LinearForm) (hdisjoint : pointwiseLinearProduct m n = 0) : anfLinearProjection (linearANF ell * (linearANF m * linearANF n)) = 0

theorem UnrestrictedBooleanMul.N4.sliceQuadraticA_disjoint : pointwiseLinearProduct sliceABar sliceBBar = 0

theorem UnrestrictedBooleanMul.N4.sliceInfinityQuadratic_disjoint : pointwiseLinearProduct (placeA 2) (placeB 2) = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_sliceQuadraticAANF : anfTwoProjection sliceQuadraticAANF = sliceQuadraticA

@[simp]

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_sliceInfinityQuadraticANF : anfTwoProjection sliceInfinityQuadraticANF = sliceInfinityQuadratic

@[simp]

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_sliceQuadraticBANF : anfTwoProjection sliceQuadraticBANF = sliceQuadraticB

@[simp]

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_sliceQuadraticAANF : anfThreeProjection sliceQuadraticAANF = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_sliceInfinityQuadraticANF : anfThreeProjection sliceInfinityQuadraticANF = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_sliceQuadraticBANF : anfThreeProjection sliceQuadraticBANF = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_sliceQuadraticAANF : anfLinearProjection sliceQuadraticAANF = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_sliceInfinityQuadraticANF : anfLinearProjection sliceInfinityQuadraticANF = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_sliceQuadraticBANF : anfLinearProjection sliceQuadraticBANF = 0

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_affine_mul_sliceQuadraticA (a : F₂) (ell : LinearForm) : anfTwoProjection (affineANF a ell * sliceQuadraticAANF) = a • sliceQuadraticA + booleanContraction ell sliceQuadraticA

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_affine_mul_sliceInfinityQuadratic (a : F₂) (ell : LinearForm) : anfTwoProjection (affineANF a ell * sliceInfinityQuadraticANF) = a • sliceInfinityQuadratic + booleanContraction ell sliceInfinityQuadratic

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_affine_mul_sliceQuadraticA (a : F₂) (ell : LinearForm) : anfLinearProjection (affineANF a ell * sliceQuadraticAANF) = 0

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_affine_mul_sliceInfinityQuadratic (a : F₂) (ell : LinearForm) : anfLinearProjection (affineANF a ell * sliceInfinityQuadraticANF) = 0

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_affine_mul_sliceQuadraticA (a : F₂) (ell : LinearForm) : anfThreeProjection (affineANF a ell * sliceQuadraticAANF) = vectorWedgeTwo ell sliceQuadraticA

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_affine_mul_sliceInfinityQuadratic (a : F₂) (ell : LinearForm) : anfThreeProjection (affineANF a ell * sliceInfinityQuadraticANF) = vectorWedgeTwo ell sliceInfinityQuadratic

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_affine_mul_sliceQuadraticB (a : F₂) (ell : LinearForm) : anfTwoProjection (affineANF a ell * sliceQuadraticBANF) = a • sliceQuadraticB + booleanContraction ell sliceQuadraticB

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_affine_mul_sliceQuadraticB (a : F₂) (ell : LinearForm) : anfLinearProjection (affineANF a ell * sliceQuadraticBANF) = 0

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_affine_mul_sliceQuadraticB (a : F₂) (ell : LinearForm) : anfThreeProjection (affineANF a ell * sliceQuadraticBANF) = vectorWedgeTwo ell sliceQuadraticB

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_affineANF (a : F₂) (ell : LinearForm) : anfThreeProjection (affineANF a ell) = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_sliceCorrectionModel (a : F₂) (ell : LinearForm) (alpha : Fin 3 → F₂) (x y : F₂) : anfThreeProjection (sliceCorrectionModel a ell alpha x y) = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_sliceCorrectionModel (a : F₂) (ell : LinearForm) (alpha : Fin 3 → F₂) (x y : F₂) : anfTwoProjection (sliceCorrectionModel a ell alpha x y) = alpha 1 • sliceQuadraticA + alpha 2 • sliceInfinityQuadratic

@[simp]

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_sliceCorrectionModel (a : F₂) (ell : LinearForm) (alpha : Fin 3 → F₂) (x y : F₂) : anfLinearProjection (sliceCorrectionModel a ell alpha x y) = sliceComplementLinear ell + alpha 1 • sliceVaryingLinear x y

@[simp]

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_sliceTangentModel (a : F₂) (ell : LinearForm) (eps x y : F₂) : anfThreeProjection (sliceTangentModel a ell eps x y) = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_sliceTangentModel (a : F₂) (ell : LinearForm) (eps x y : F₂) : anfTwoProjection (sliceTangentModel a ell eps x y) = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_sliceTangentModel (a : F₂) (ell : LinearForm) (eps x y : F₂) : anfLinearProjection (sliceTangentModel a ell eps x y) = sliceComplementLinear ell + y • sliceU + x • sliceV

theorem UnrestrictedBooleanMul.N4.booleanContraction_sliceComplement_sliceQuadraticA (p q : F₂) : booleanContraction (p • sliceABar + q • sliceBBar) sliceQuadraticA = (p + q) • sliceQuadraticA

The Boolean degree-lowering contraction on the type-A support plane.

theorem UnrestrictedBooleanMul.N4.booleanContraction_sliceInfinity_sliceInfinityQuadratic (p q : F₂) : booleanContraction (p • placeA 2 + q • placeB 2) sliceInfinityQuadratic = (p + q) • sliceInfinityQuadratic

theorem UnrestrictedBooleanMul.N4.booleanContraction_zero (q : TwoForm) : booleanContraction 0 q = 0

noncomputable def UnrestrictedBooleanMul.N4.sliceTypeAFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : ANF 8

The full sliced type-A product, including its affine and rational-target correction.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.sliceTypeBFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : ANF 8

The full sliced type-B product, including its affine and rational-target correction.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.sliceTypeInfinityFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : ANF 8

The full sliced infinity-type product, including its affine and rational-target correction.

Equations

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

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceTypeAFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : AnchorsIndependent (sliceTypeAFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y)

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceTypeBFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : AnchorsIndependent (sliceTypeBFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y)

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceTypeInfinityFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : AnchorsIndependent (sliceTypeInfinityFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y)

@[simp]

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_sliceTypeAFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfThreeProjection (sliceTypeAFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y) = vectorWedgeTwo (sliceComplementLinear leftLinear) sliceQuadraticA

@[simp]

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_sliceTypeBFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfThreeProjection (sliceTypeBFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y) = vectorWedgeTwo (sliceComplementLinear leftLinear) sliceQuadraticB

@[simp]

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_sliceTypeInfinityFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfThreeProjection (sliceTypeInfinityFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y) = vectorWedgeTwo (sliceComplementLinear leftLinear) sliceInfinityQuadratic

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_sliceTypeAFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfTwoProjection (sliceTypeAFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y) = (leftConst + sliceAnchorValue leftLinear x y + x * y) • sliceQuadraticA + vectorWedge (sliceComplementLinear leftLinear) (sliceComplementLinear rightLinear + sliceVaryingLinear x y) + booleanContraction (sliceComplementLinear leftLinear) sliceQuadraticA + correctionCoeff 1 • sliceQuadraticA + correctionCoeff 2 • sliceInfinityQuadratic

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_sliceTypeBFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfTwoProjection (sliceTypeBFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y) = (leftConst + sliceAnchorValue leftLinear x y + x * y) • sliceQuadraticB + vectorWedge (sliceComplementLinear leftLinear) (sliceComplementLinear rightLinear + sliceVaryingLinear x y) + booleanContraction (sliceComplementLinear leftLinear) sliceQuadraticB + correctionCoeff 1 • sliceQuadraticA + correctionCoeff 2 • sliceInfinityQuadratic

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_sliceTypeInfinityFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfTwoProjection (sliceTypeInfinityFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y) = (leftConst + sliceAnchorValue leftLinear x y + x * y) • sliceInfinityQuadratic + vectorWedge (sliceComplementLinear leftLinear) (sliceComplementLinear rightLinear) + booleanContraction (sliceComplementLinear leftLinear) sliceInfinityQuadratic + correctionCoeff 1 • sliceQuadraticA + correctionCoeff 2 • sliceInfinityQuadratic

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_sliceTypeAFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfLinearProjection (sliceTypeAFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y) = sliceProductLinear (leftConst + sliceAnchorValue leftLinear x y + x * y) (rightConst + sliceAnchorValue rightLinear x y + x * y) (sliceComplementLinear leftLinear) (sliceComplementLinear rightLinear + sliceVaryingLinear x y) (sliceComplementLinear correctionLinear) (correctionCoeff 1) x y

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_sliceTypeBFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfLinearProjection (sliceTypeBFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y) = sliceProductLinear (leftConst + sliceAnchorValue leftLinear x y + x * y) (rightConst + sliceAnchorValue rightLinear x y + x * y) (sliceComplementLinear leftLinear) (sliceComplementLinear rightLinear + sliceVaryingLinear x y) (sliceComplementLinear correctionLinear) (correctionCoeff 1) x y

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_sliceTypeInfinityFullModel (leftConst : F₂) (leftLinear : LinearForm) (rightConst : F₂) (rightLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfLinearProjection (sliceTypeInfinityFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x y) = sliceProductLinear (leftConst + sliceAnchorValue leftLinear x y + x * y) (rightConst + sliceAnchorValue rightLinear x y) (sliceComplementLinear leftLinear) (sliceComplementLinear rightLinear) (sliceComplementLinear correctionLinear) (correctionCoeff 1) x y