Cryptographic Boolean Functions in Lean

1.6. Algebraic normal form existence and uniqueness🔗

Theorem1.6.1
uses 1
Used by 4
Reverse dependency previews
Preview
Definition 1.9.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2proposition-1pages-10-11fidelity-exact

Existence and uniqueness of the ANF, and Proposition 1 (Carlet, pp. 10--11). For every f:V_n\to\mathbb F_2, there exists a unique family (c_S)_{S\subseteq[n]} such that f(x)=\bigoplus_{S\subseteq[n]}c_S\prod_{i\in S}x_i \qquad(x\in V_n). If \mathbf 1_T denotes the indicator vector of T\subseteq[n], then the coefficient of x^S is c_S =\bigoplus_{\substack{x\in V_n\\\operatorname{supp}(x)\subseteq S}}f(x) =\bigoplus_{T\subseteq S}f(\mathbf 1_T) \qquad(S\subseteq[n]).

Lean code for Theorem1.6.1●8 declarations
  • theoremdefined in CryptBoolean/Carlet/Chapter02/ANFExistence.lean
    complete
    theorem CryptBoolean.anfMonomial_f₂CubeOfFinset {n : ℕ} (S U : Finset (Fin n)) :
  CryptBoolean.anfMonomial S (FABL.f₂CubeOfFinset U) =
    if S ⊆ U then 1 else 0
    theorem CryptBoolean.anfMonomial_f₂CubeOfFinset
  {n : ℕ} (S U : Finset (Fin n)) :
  CryptBoolean.anfMonomial S
      (FABL.f₂CubeOfFinset U) =
    if S ⊆ U then 1 else 0
    The square-free monomial evaluated at a subset indicator is one exactly on subsets.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/ANFExistence.lean
    complete
    theorem CryptBoolean.anfEval_f₂CubeOfFinset {n : ℕ}
  (c : CryptBoolean.ANFCoefficients n) (U : Finset (Fin n)) :
  CryptBoolean.anfEval c (FABL.f₂CubeOfFinset U) = ∑ S ∈ U.powerset, c S
    theorem CryptBoolean.anfEval_f₂CubeOfFinset
  {n : ℕ}
  (c : CryptBoolean.ANFCoefficients n)
  (U : Finset (Fin n)) :
  CryptBoolean.anfEval c
      (FABL.f₂CubeOfFinset U) =
    ∑ S ∈ U.powerset, c S
    ANF evaluation at a subset indicator is the zeta partial sum over the powerset.
  • defdefined in CryptBoolean/Carlet/Chapter02/ANFExistence.lean
    complete
    def CryptBoolean.anfCoeff {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.ANFCoefficients n
    def CryptBoolean.anfCoeff {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.ANFCoefficients n
    The canonical `𝔽₂` Möbius-inverse coefficient family of a Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/ANFExistence.lean
    complete
    theorem CryptBoolean.anfEval_anfCoeff_f₂CubeOfFinset {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (U : Finset (Fin n)) :
  CryptBoolean.anfEval (CryptBoolean.anfCoeff f)
      (FABL.f₂CubeOfFinset U) =
    f (FABL.f₂CubeOfFinset U)
    theorem CryptBoolean.anfEval_anfCoeff_f₂CubeOfFinset
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (U : Finset (Fin n)) :
  CryptBoolean.anfEval
      (CryptBoolean.anfCoeff f)
      (FABL.f₂CubeOfFinset U) =
    f (FABL.f₂CubeOfFinset U)
    Existence at an indicator input: the canonical coefficients reproduce `f` on every `1_U`.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/ANFExistence.lean
    complete
    theorem CryptBoolean.anfEval_anfCoeff {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.anfEval (CryptBoolean.anfCoeff f) = f
    theorem CryptBoolean.anfEval_anfCoeff {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.anfEval
      (CryptBoolean.anfCoeff f) =
    f
    Existence: the canonical coefficient family evaluates to the original Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/ANFExistence.lean
    complete
    theorem CryptBoolean.anfCoeff_unique_of_powerset_sum {n : ℕ}
  (c d : CryptBoolean.ANFCoefficients n)
  (h :
    ∀ (U : Finset (Fin n)),
      ∑ T ∈ U.powerset, c T = ∑ T ∈ U.powerset, d T) :
  c = d
    theorem CryptBoolean.anfCoeff_unique_of_powerset_sum
  {n : ℕ}
  (c d : CryptBoolean.ANFCoefficients n)
  (h :
    ∀ (U : Finset (Fin n)),
      ∑ T ∈ U.powerset, c T =
        ∑ T ∈ U.powerset, d T) :
  c = d
    Uniqueness of the zeta transform on the subset lattice: equal powerset partial sums
force equal coefficient families.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/ANFExistence.lean
    complete
    theorem CryptBoolean.anfEval_injective {n : ℕ}
  {c d : CryptBoolean.ANFCoefficients n}
  (h : CryptBoolean.anfEval c = CryptBoolean.anfEval d) : c = d
    theorem CryptBoolean.anfEval_injective {n : ℕ}
  {c d : CryptBoolean.ANFCoefficients n}
  (h :
    CryptBoolean.anfEval c =
      CryptBoolean.anfEval d) :
  c = d
    Uniqueness: coefficient families with equal ANF evaluation are equal.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/ANFExistence.lean
    complete
    theorem CryptBoolean.existsUnique_anfEval {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∃! c, CryptBoolean.anfEval c = f
    theorem CryptBoolean.existsUnique_anfEval {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∃! c, CryptBoolean.anfEval c = f
    Carlet, Section 2.1: every Boolean function has a unique algebraic normal form.

Formalization note. The Lean proof establishes existence by the characteristic-two subset-lattice transform and uniqueness by injectivity of its zeta sums. The interval-cardinality calculation is a proof mechanism, not part of the theorem statement.