The feedback factor at a zero-place tangent

Right idempotence for a target tangent at the rational place zero forces the linear part of the rational feedback factor to use only the two anchor variables. Thus the factor has the manuscript form δ + ρ x + σ y + x y. The proof uses only the cubic homogeneous projection and six explicit exterior coordinates.

theorem UnrestrictedBooleanMul.N4.rZeroCoeff_eq_targetBasis_zero : rZeroCoeff = targetBasis 0

theorem UnrestrictedBooleanMul.N4.rationalCoeffRep_singleton_zero : rationalCoeffRep (rationalSingleton 0) = rZeroCoeff

theorem UnrestrictedBooleanMul.N4.rationalTwo_singleton_zero : rationalTwo (rationalSingleton 0) = zeroPlaceTwo

theorem UnrestrictedBooleanMul.N4.targetTwo_zero_tangent (eps : F₂) : targetTwo (rationalTangentAt 0 eps) = eps • zeroPlaceTwo + zeroFirstJetTwo

theorem UnrestrictedBooleanMul.N4.targetANF_targetBasis_feedback (s : Fin 7) : targetANF (targetBasis s) = Mul 4 s

theorem UnrestrictedBooleanMul.N4.targetANF_zero_tangent (eps : F₂) : targetANF (rationalTangentAt 0 eps) = eps • Mul 4 0 + Mul 4 1

theorem UnrestrictedBooleanMul.N4.rationalANF_singleton_zero : rationalANF (rationalSingleton 0) = Mul 4 0

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

theorem UnrestrictedBooleanMul.N4.aLinear_eq_coordinateLinear (i : Fin 4) : aLinear i = coordinateLinear (aCoord i)

theorem UnrestrictedBooleanMul.N4.bLinear_eq_coordinateLinear (i : Fin 4) : bLinear i = coordinateLinear (bCoord i)

theorem UnrestrictedBooleanMul.N4.zero_tangent_cubic_coordinate_form : monomialThree {0, 4, 5} + monomialThree {0, 1, 4} = vectorWedgeTwo (sliceU + sliceV) zeroPlaceTwo

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_zero_tangent_mul_singleton (eps : F₂) : anfThreeProjection (targetANF (rationalTangentAt 0 eps) * rationalANF (rationalSingleton 0)) = vectorWedgeTwo (sliceU + sliceV) zeroPlaceTwo

The only cubic terms in tangent times anchor-place are x y u and x y v.

theorem UnrestrictedBooleanMul.N4.zero_tangent_right_idempotence_cubic {F factor : ANF 8} {targetConst factorConst eps : F₂} {targetLinear factorLinear : LinearForm} (hFRep : F = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps)) (hfactorRep : factor = affineANF factorConst factorLinear + rationalANF (rationalSingleton 0)) (hright : F * factor = F) : vectorWedgeTwo factorLinear (eps • zeroPlaceTwo + zeroFirstJetTwo) + vectorWedgeTwo targetLinear zeroPlaceTwo + vectorWedgeTwo (sliceU + sliceV) zeroPlaceTwo = 0

Cubic form of right idempotence at the zero rational place.

theorem UnrestrictedBooleanMul.N4.factorLinear_mem_anchor_plane {F factor : ANF 8} {targetConst factorConst eps : F₂} {targetLinear factorLinear : LinearForm} (hFRep : F = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps)) (hfactorRep : factor = affineANF factorConst factorLinear + rationalANF (rationalSingleton 0)) (hright : F * factor = F) : ∃ (rho : F₂) (sigma : F₂), factorLinear = rho • sliceX + sigma • sliceY

The six complementary coordinates of the feedback linear form vanish.

def UnrestrictedBooleanMul.N4.ZeroPlaceFeedbackForm (factor : ANF 8) : Prop

The affine perturbations of the zero-place product supported on its two inputs.

Equations

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

theorem UnrestrictedBooleanMul.N4.zeroPlaceFeedbackForm_of_right_idempotence {F factor : ANF 8} {targetConst factorConst eps : F₂} {targetLinear factorLinear : LinearForm} (hFRep : F = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps)) (hfactorRep : factor = affineANF factorConst factorLinear + rationalANF (rationalSingleton 0)) (hright : F * factor = F) : ZeroPlaceFeedbackForm factor

ANF-level feedback normal form δ + ρx + σy + xy.