Vanishing slices of a zero-place tangent

The feedback factor δ + ρx + σy + xy is zero on an odd number of the four anchor corners. Right idempotence makes the target child vanish on every zero corner. Two such vanishing slices would have equal first differences in the complementary u and v directions, forcing the corners to be equal. Hence there is exactly one zero corner and exactly three active slices.

def UnrestrictedBooleanMul.N4.sliceAssignment (x y : F₂) (z : Fin 6 → F₂) : Fin 8 → F₂

Embed six complementary values between the two anchor variables.

Equations

• UnrestrictedBooleanMul.N4.sliceAssignment x y z = ![x, z 0, z 1, z 2, y, z 3, z 4, z 5]

def UnrestrictedBooleanMul.N4.sliceComplementZero : Fin 6 → F₂

The zero assignment on the six complementary slice inputs.

Equations

• UnrestrictedBooleanMul.N4.sliceComplementZero = ![0, 0, 0, 0, 0, 0]

def UnrestrictedBooleanMul.N4.sliceComplementU : Fin 6 → F₂

The complementary assignment selecting the first polynomial linear coefficient.

Equations

• UnrestrictedBooleanMul.N4.sliceComplementU = ![1, 0, 0, 0, 0, 0]

def UnrestrictedBooleanMul.N4.sliceComplementV : Fin 6 → F₂

The complementary assignment selecting the second polynomial linear coefficient.

Equations

• UnrestrictedBooleanMul.N4.sliceComplementV = ![0, 0, 0, 1, 0, 0]

def UnrestrictedBooleanMul.N4.SliceVanishes (F : ANF 8) (x y : F₂) : Prop

The ANF vanishes on every assignment with the specified anchor values.

Equations

• UnrestrictedBooleanMul.N4.SliceVanishes F x y = ∀ (z : Fin 6 → UnrestrictedBooleanMul.F₂), UnrestrictedBooleanMul.eval F (UnrestrictedBooleanMul.N4.sliceAssignment x y z) = 0

theorem UnrestrictedBooleanMul.N4.mul_target_zero_anf : Mul 4 0 = monomial {0, 4}

theorem UnrestrictedBooleanMul.N4.mul_target_one_anf : Mul 4 1 = monomial {0, 5} + monomial {1, 4}

theorem UnrestrictedBooleanMul.N4.zero_tangent_sliceU_difference {F : ANF 8} {targetConst eps : F₂} {targetLinear : LinearForm} (hFRep : F = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps)) (x y : F₂) : eval F (sliceAssignment x y sliceComplementU) + eval F (sliceAssignment x y sliceComplementZero) = targetLinear 1 + y

First difference of a tangent slice in the complementary u direction.

theorem UnrestrictedBooleanMul.N4.zero_tangent_sliceV_difference {F : ANF 8} {targetConst eps : F₂} {targetLinear : LinearForm} (hFRep : F = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps)) (x y : F₂) : eval F (sliceAssignment x y sliceComplementV) + eval F (sliceAssignment x y sliceComplementZero) = targetLinear 5 + x

First difference of a tangent slice in the complementary v direction.

theorem UnrestrictedBooleanMul.N4.zero_tangent_vanishing_slices_injective {F : ANF 8} {targetConst eps : F₂} {targetLinear : LinearForm} (hFRep : F = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps)) {x y x' y' : F₂} (hxy : SliceVanishes F x y) (hxy' : SliceVanishes F x' y') : x = x' ∧ y = y'

A tangent target cannot vanish on two distinct anchor slices.

def UnrestrictedBooleanMul.N4.feedbackCorner (delta rho sigma x y : F₂) : F₂

The scalar zero-place feedback factor at one anchor corner.

Equations

• UnrestrictedBooleanMul.N4.feedbackCorner delta rho sigma x y = delta + rho * x + sigma * y + x * y

theorem UnrestrictedBooleanMul.N4.eval_zero_place_feedback {factor : ANF 8} {delta rho sigma : F₂} (hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0)) (x y : F₂) (z : Fin 6 → F₂) : eval factor (sliceAssignment x y z) = feedbackCorner delta rho sigma x y

theorem UnrestrictedBooleanMul.N4.slice_vanishes_of_feedbackCorner_zero {F factor : ANF 8} {delta rho sigma : F₂} (hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0)) (hright : F * factor = F) {x y : F₂} (hzero : feedbackCorner delta rho sigma x y = 0) : SliceVanishes F x y

A zero feedback corner makes the target child vanish on that slice.

theorem UnrestrictedBooleanMul.N4.feedbackCorner_has_zero (delta rho sigma : F₂) : ∃ (x : F₂) (y : F₂), feedbackCorner delta rho sigma x y = 0

A Boolean polynomial with xy coefficient one has a zero corner.

def UnrestrictedBooleanMul.N4.ExactlyThreeActiveCorners (delta rho sigma : F₂) : Prop

The feedback factor vanishes at exactly one of the four Boolean anchor corners.

Equations

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

theorem UnrestrictedBooleanMul.N4.exactlyThreeActiveCorners_of_right_idempotence {F factor : ANF 8} {targetConst eps delta rho sigma : F₂} {targetLinear : LinearForm} (hFRep : F = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps)) (hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0)) (hright : F * factor = F) : ExactlyThreeActiveCorners delta rho sigma

Right idempotence and tangent separation leave exactly three active anchor slices.