Boolean-ring identities used by feedback gates

Every canonical Boolean ANF is idempotent. Consequently, if f = u * c, then both factors absorb f. The manuscript uses these identities at the quartic seed and at both feedback stages; proving them once at the ANF level prevents those arguments from silently treating Boolean multiplication as ordinary polynomial multiplication.

theorem UnrestrictedBooleanMul.N4.monomial_mul_self {m : ℕ} (s : Monomial m) : s * s = s

@[simp]

theorem UnrestrictedBooleanMul.N4.anf_mul_self {m : ℕ} (p : ANF m) : p * p = p

Frobenius is the identity on the Boolean ANF algebra.

theorem UnrestrictedBooleanMul.N4.left_absorbs_product {m : ℕ} (u c : ANF m) : u * (u * c) = u * c

A factor absorbs its product in the Boolean function algebra.

theorem UnrestrictedBooleanMul.N4.right_absorbs_product {m : ℕ} (u c : ANF m) : u * c * c = u * c

The other factor absorbs the same product.

theorem UnrestrictedBooleanMul.N4.absorption_of_eq {m : ℕ} {u c f : ANF m} (hf : f = u * c) : u * f = f ∧ f * c = f