Algebraic normalization of a rational place

The two nontrivial changes of variable are translation t ↦ t + 1 and reversal t ↦ 1/t on coefficient vectors. Their substitutions on the eight input coordinates define ANF algebra homomorphisms. They carry the selected rational place and its first tangent to the zero place. No circuit states or Boolean functions are enumerated.

def UnrestrictedBooleanMul.N4.inputPlaceChange : Fin 3 → Fin 8 → LinearForm

Images of the eight coordinate linear forms under the identity, translation, and reversal substitutions.

Equations

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

def UnrestrictedBooleanMul.N4.normalizePlaceLinear (theta : Fin 3) (ell : LinearForm) : LinearForm

Apply the input coordinate change moving the chosen rational place to zero.

Equations

• UnrestrictedBooleanMul.N4.normalizePlaceLinear theta ell = ∑ i : Fin 8, ell i • UnrestrictedBooleanMul.N4.inputPlaceChange theta i

def UnrestrictedBooleanMul.N4.normalizeRationalCoeff (theta : Fin 3) (alpha : Fin 3 → F₂) : Fin 3 → F₂

Permute rational-place coefficients under the chosen place normalization.

Equations

• UnrestrictedBooleanMul.N4.normalizeRationalCoeff theta alpha = ![![alpha 0, alpha 1, alpha 2], ![alpha 1, alpha 0, alpha 2], ![alpha 2, alpha 1, alpha 0]] theta

theorem UnrestrictedBooleanMul.N4.normalizePlaceLinear_add (theta : Fin 3) (ell m : LinearForm) : normalizePlaceLinear theta (ell + m) = normalizePlaceLinear theta ell + normalizePlaceLinear theta m

theorem UnrestrictedBooleanMul.N4.normalizePlaceLinear_smul (theta : Fin 3) (a : F₂) (ell : LinearForm) : normalizePlaceLinear theta (a • ell) = a • normalizePlaceLinear theta ell

theorem UnrestrictedBooleanMul.N4.normalizeRationalCoeff_add (theta : Fin 3) (alpha beta : Fin 3 → F₂) : normalizeRationalCoeff theta (alpha + beta) = normalizeRationalCoeff theta alpha + normalizeRationalCoeff theta beta

theorem UnrestrictedBooleanMul.N4.normalizeRationalCoeff_smul (theta : Fin 3) (a : F₂) (alpha : Fin 3 → F₂) : normalizeRationalCoeff theta (a • alpha) = a • normalizeRationalCoeff theta alpha

theorem UnrestrictedBooleanMul.N4.normalizeRationalCoeff_injective (theta : Fin 3) : Function.Injective (normalizeRationalCoeff theta)

@[simp]

theorem UnrestrictedBooleanMul.N4.normalizeRationalCoeff_zero (theta : Fin 3) : normalizeRationalCoeff theta 0 = 0

theorem UnrestrictedBooleanMul.N4.normalizeRationalCoeff_ne_zero (theta : Fin 3) {alpha : Fin 3 → F₂} (h : alpha ≠ 0) : normalizeRationalCoeff theta alpha ≠ 0

theorem UnrestrictedBooleanMul.N4.normalizeRationalCoeff_ne (theta : Fin 3) {alpha beta : Fin 3 → F₂} (h : alpha ≠ beta) : normalizeRationalCoeff theta alpha ≠ normalizeRationalCoeff theta beta

theorem UnrestrictedBooleanMul.N4.normalizeRationalCoeff_singleton_self (theta : Fin 3) : normalizeRationalCoeff theta (rationalSingleton theta) = rationalSingleton 0

theorem UnrestrictedBooleanMul.N4.anf_prod_absorb_subset {s t : Finset (Fin 8)} (h : t ⊆ s) (f : Fin 8 → ANF 8) : (∏ i ∈ s, f i) * ∏ i ∈ t, f i = ∏ i ∈ s, f i

theorem UnrestrictedBooleanMul.N4.anf_prod_union (s t : Finset (Fin 8)) (f : Fin 8 → ANF 8) : ∏ i ∈ s ∪ t, f i = (∏ i ∈ s, f i) * ∏ i ∈ t, f i

noncomputable def UnrestrictedBooleanMul.N4.placeSubstitutionMonoid (theta : Fin 3) : Monomial 8 →* ANF 8

Substitute the normalized linear inputs into a squarefree monomial.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.anfPlaceNormalize (theta : Fin 3) : ANF 8 →ₐ[F₂] ANF 8

The Boolean ANF algebra homomorphism induced by a rational-place normalization.

Equations

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

@[simp]

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_monomial (theta : Fin 3) (s : Finset (Fin 8)) : (anfPlaceNormalize theta) (monomial s) = ∏ i ∈ s, linearANF (inputPlaceChange theta i)

@[simp]

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_X (theta : Fin 3) (i : Fin 8) : (anfPlaceNormalize theta) (X i) = linearANF (inputPlaceChange theta i)

noncomputable def UnrestrictedBooleanMul.N4.linearANFMap : LinearForm →ₗ[F₂] ANF 8

Convert a coefficient vector to its linear ANF, as a linear map.

Equations

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

@[simp]

theorem UnrestrictedBooleanMul.N4.linearANFMap_apply (ell : LinearForm) : linearANFMap ell = linearANF ell

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_linearANF (theta : Fin 3) (ell : LinearForm) : (anfPlaceNormalize theta) (linearANF ell) = linearANF (normalizePlaceLinear theta ell)

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_affineANF (theta : Fin 3) (a : F₂) (ell : LinearForm) : (anfPlaceNormalize theta) (affineANF a ell) = affineANF a (normalizePlaceLinear theta ell)

def UnrestrictedBooleanMul.N4.normalizePlaceIndex : Fin 3 → Fin 3 → Fin 3

The permutation exchanging the chosen rational place with zero.

Equations

• UnrestrictedBooleanMul.N4.normalizePlaceIndex = ![![0, 1, 2], ![1, 0, 2], ![2, 1, 0]]

theorem UnrestrictedBooleanMul.N4.normalizePlaceLinear_placeA (theta k : Fin 3) : normalizePlaceLinear theta (placeA k) = placeA (normalizePlaceIndex theta k)

theorem UnrestrictedBooleanMul.N4.normalizePlaceLinear_placeB (theta k : Fin 3) : normalizePlaceLinear theta (placeB k) = placeB (normalizePlaceIndex theta k)

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_rationalPlaceANF (theta k : Fin 3) : (anfPlaceNormalize theta) (targetANF (rationalPlaceCoeff k)) = targetANF (rationalPlaceCoeff (normalizePlaceIndex theta k))

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_rationalANF (theta : Fin 3) (alpha : Fin 3 → F₂) : (anfPlaceNormalize theta) (rationalANF alpha) = rationalANF (normalizeRationalCoeff theta alpha)

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_representedLowFactor (theta : Fin 3) (a : F₂) (ell : LinearForm) (alpha : Fin 3 → F₂) : (anfPlaceNormalize theta) (representedLowFactor a ell alpha) = representedLowFactor a (normalizePlaceLinear theta ell) (normalizeRationalCoeff theta alpha)

theorem UnrestrictedBooleanMul.N4.aVar_four_eq_X_aCoord (i : Fin 4) : aVar 4 i = X (aCoord i)

theorem UnrestrictedBooleanMul.N4.bVar_four_eq_X_bCoord (i : Fin 4) : bVar 4 i = X (bCoord i)

@[simp]

theorem UnrestrictedBooleanMul.N4.aVar_mul_bVar_eq_targetPair (i j : Fin 4) : aVar 4 i * bVar 4 j = monomial (targetPair i j)

theorem UnrestrictedBooleanMul.N4.targetANF_eq_bilinear_sum (c : TargetCoeff) : targetANF c = ∑ i : Fin 4, ∑ j : Fin 4, c (hankelIndex i j) • (aVar 4 i * bVar 4 j)

@[simp]

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_aVar (theta : Fin 3) (i : Fin 4) : (anfPlaceNormalize theta) (aVar 4 i) = linearANF (inputPlaceChange theta (aCoord i))

@[simp]

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_bVar (theta : Fin 3) (i : Fin 4) : (anfPlaceNormalize theta) (bVar 4 i) = linearANF (inputPlaceChange theta (bCoord i))

theorem UnrestrictedBooleanMul.N4.anfPlaceNormalize_tangent_self (theta : Fin 3) (eps : F₂) : (anfPlaceNormalize theta) (targetANF (rationalTangentAt theta eps)) = targetANF (rationalTangentAt 0 eps)