Cryptographic Boolean Functions in Lean

1.6. Numerical normal form🔗

Theorem1.6.1
Group: Chapter 1: Generalities on Boolean functions (40)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 6
Reverse dependency previews
Preview
Theorem 1.6.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2numerical-normal-formpages-18-19fidelity-exact

Numerical normal form (Carlet, pp. 18--19). Every pseudo-Boolean function \varphi:V_n\to\mathbb R admits a unique family (\lambda_S)_{S\subseteq[n]} such that \varphi(x)=\sum_{S\subseteq[n]}\lambda_S\prod_{i\in S}x_i \qquad(x\in V_n). Equivalently, \varphi(x)=\sum_{S\subseteq\operatorname{supp}(x)}\lambda_S. For every S\subseteq[n], the coefficients therefore satisfy \lambda_S =\varphi(\mathbf 1_S)-\sum_{T\subsetneq S}\lambda_T.

Lean code for Theorem1.6.1●10 declarations
  • abbrevdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    abbrev FABL.PseudoBooleanFunction (n : ℕ) : Type
    abbrev FABL.PseudoBooleanFunction (n : ℕ) : Type
    A real-valued pseudo-Boolean function on the binary cube.
  • abbrevdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    abbrev FABL.NumericalCoefficients (n : ℕ) : Type
    abbrev FABL.NumericalCoefficients (n : ℕ) : Type
    Coefficients of a square-free numerical normal form.
  • defdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    def FABL.numericalMonomial {n : ℕ} (S : Finset (Fin n))
  (x : FABL.F₂Cube n) : ℝ
    def FABL.numericalMonomial {n : ℕ}
  (S : Finset (Fin n))
  (x : FABL.F₂Cube n) : ℝ
    The real square-free monomial indexed by `S`.
  • defdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    def FABL.numericalEval {n : ℕ} (c : FABL.NumericalCoefficients n) :
  FABL.PseudoBooleanFunction n
    def FABL.numericalEval {n : ℕ}
  (c : FABL.NumericalCoefficients n) :
  FABL.PseudoBooleanFunction n
    Evaluation of a numerical normal form.
  • defdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    def FABL.numericalEvalLinear (n : ℕ) :
  FABL.NumericalCoefficients n →ₗ[ℝ] FABL.PseudoBooleanFunction n
    def FABL.numericalEvalLinear (n : ℕ) :
  FABL.NumericalCoefficients n →ₗ[ℝ]
    FABL.PseudoBooleanFunction n
    Numerical evaluation as a real-linear map.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    theorem FABL.numericalEval_injective {n : ℕ} :
  Function.Injective ⇑(FABL.numericalEvalLinear n)
    theorem FABL.numericalEval_injective {n : ℕ} :
  Function.Injective
    ⇑(FABL.numericalEvalLinear n)
    Numerical evaluation is injective.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    theorem FABL.existsUnique_numericalEval {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) : ∃! c, FABL.numericalEval c = φ
    theorem FABL.existsUnique_numericalEval {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  ∃! c, FABL.numericalEval c = φ
    Every pseudo-Boolean function has a unique numerical normal form.
  • defdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    def FABL.numericalCoeff {n : ℕ} (φ : FABL.PseudoBooleanFunction n) :
  FABL.NumericalCoefficients n
    def FABL.numericalCoeff {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  FABL.NumericalCoefficients n
    The canonical numerical coefficients supplied by the unique representation theorem.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    theorem FABL.numericalEval_numericalCoeff {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  FABL.numericalEval (FABL.numericalCoeff φ) = φ
    theorem FABL.numericalEval_numericalCoeff {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  FABL.numericalEval
      (FABL.numericalCoeff φ) =
    φ
    The canonical numerical normal form evaluates to the original function.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    theorem FABL.numericalCoeff_eq_value_sub_lower {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) (S : Finset (Fin n)) :
  FABL.numericalCoeff φ S =
    φ (FABL.f₂CubeOfFinset S) -
      ∑ T ∈ S.powerset.erase S, FABL.numericalCoeff φ T
    theorem FABL.numericalCoeff_eq_value_sub_lower
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (S : Finset (Fin n)) :
  FABL.numericalCoeff φ S =
    φ (FABL.f₂CubeOfFinset S) -
      ∑ T ∈ S.powerset.erase S,
        FABL.numericalCoeff φ T
    Each numerical coefficient is determined from the value at `1_S` and lower coefficients.
Theorem1.6.2
Group: Chapter 1: Generalities on Boolean functions (40)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.6.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Theorem 5.2.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2relation-30page-32fidelity-exact

Relation (30) (Carlet, p. 32). If \varphi(x)=\sum_{S\subseteq[n]}\lambda_S\prod_{i\in S}x_i, then for every u\in V_n, \widehat\varphi(u) =(-1)^{w_H(u)} \sum_{\operatorname{supp}(u)\subseteq S} 2^{n-|S|}\lambda_S.

Lean code for Theorem1.6.2●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter02/FourierNNF.lean
    complete
    theorem CryptBoolean.rawFourierTransform_numericalMonomial {n : ℕ}
  (S : Finset (Fin n)) (u : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform (FABL.numericalMonomial S) u =
    if FABL.f₂Support u ⊆ S then
      (-1) ^ (FABL.f₂Support u).card * 2 ^ (n - S.card)
    else 0
    theorem CryptBoolean.rawFourierTransform_numericalMonomial
  {n : ℕ} (S : Finset (Fin n))
  (u : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.numericalMonomial S) u =
    if FABL.f₂Support u ⊆ S then
      (-1) ^ (FABL.f₂Support u).card *
        2 ^ (n - S.card)
    else 0
    The raw Fourier coefficient of a numerical monomial.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/FourierNNF.lean
    complete
    theorem CryptBoolean.rawFourierTransform_numericalEval {n : ℕ}
  (c : FABL.NumericalCoefficients n) (u : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform (FABL.numericalEval c) u =
    (-1) ^ (FABL.f₂Support u).card *
      ∑ S with FABL.f₂Support u ⊆ S, 2 ^ (n - S.card) * c S
    theorem CryptBoolean.rawFourierTransform_numericalEval
  {n : ℕ}
  (c : FABL.NumericalCoefficients n)
  (u : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.numericalEval c) u =
    (-1) ^ (FABL.f₂Support u).card *
      ∑ S with FABL.f₂Support u ⊆ S,
        2 ^ (n - S.card) * c S
    Carlet Relation (30): the raw Fourier transform of a numerical normal form.
Proposition1.6.3
Group: Chapter 1: Generalities on Boolean functions (40)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 3
Reverse dependency previews
Preview
Proposition 1.6.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2proposition-4relation-8page-19fidelity-exact

Proposition 4 (Carlet, Relation (8), p. 19). If \varphi(x)=\sum_{S\subseteq[n]}\lambda_Sx^S, then for every S\subseteq[n], \lambda_S =(-1)^{|S|} \sum_{\substack{x\in V_n\\\operatorname{supp}(x)\subseteq S}} (-1)^{w_H(x)}\varphi(x) =\sum_{T\subseteq S}(-1)^{|S|-|T|}\varphi(\mathbf 1_T).

Lean code for Proposition1.6.3●5 declarations
  • theoremdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    theorem FABL.sum_Icc_neg_one_pow_card_sub {n : ℕ} (T U : Finset (Fin n))
  (hTU : T ⊆ U) :
  ∑ S ∈ Finset.Icc T U, (-1) ^ (S.card - T.card) =
    if T = U then 1 else 0
    theorem FABL.sum_Icc_neg_one_pow_card_sub {n : ℕ}
  (T U : Finset (Fin n)) (hTU : T ⊆ U) :
  ∑ S ∈ Finset.Icc T U,
      (-1) ^ (S.card - T.card) =
    if T = U then 1 else 0
    The alternating sum over a Boolean-lattice interval vanishes off the diagonal.
  • defdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    def FABL.numericalMobiusCoeff {n : ℕ} (φ : FABL.PseudoBooleanFunction n) :
  FABL.NumericalCoefficients n
    def FABL.numericalMobiusCoeff {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  FABL.NumericalCoefficients n
    The explicit real Möbius coefficient family for numerical normal form.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    theorem FABL.numericalEval_numericalMobiusCoeff_f₂CubeOfFinset {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) (U : Finset (Fin n)) :
  FABL.numericalEval (FABL.numericalMobiusCoeff φ)
      (FABL.f₂CubeOfFinset U) =
    φ (FABL.f₂CubeOfFinset U)
    theorem FABL.numericalEval_numericalMobiusCoeff_f₂CubeOfFinset
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (U : Finset (Fin n)) :
  FABL.numericalEval
      (FABL.numericalMobiusCoeff φ)
      (FABL.f₂CubeOfFinset U) =
    φ (FABL.f₂CubeOfFinset U)
    The explicit real Möbius coefficients reproduce every indicator input.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    theorem FABL.numericalMobiusCoeff_eq_numericalCoeff {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  FABL.numericalMobiusCoeff φ = FABL.numericalCoeff φ
    theorem FABL.numericalMobiusCoeff_eq_numericalCoeff
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  FABL.numericalMobiusCoeff φ =
    FABL.numericalCoeff φ
    The explicit Möbius coefficient family is the canonical numerical normal form family.
  • theoremdefined in FABL/Chapter06/F₂Polynomials/NumericalNormalForm.lean
    complete
    theorem FABL.numericalCoeff_eq_mobius_sum {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) (S : Finset (Fin n)) :
  FABL.numericalCoeff φ S =
    ∑ T ∈ S.powerset,
      (-1) ^ (S.card - T.card) * φ (FABL.f₂CubeOfFinset T)
    theorem FABL.numericalCoeff_eq_mobius_sum {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (S : Finset (Fin n)) :
  FABL.numericalCoeff φ S =
    ∑ T ∈ S.powerset,
      (-1) ^ (S.card - T.card) *
        φ (FABL.f₂CubeOfFinset T)
    The canonical numerical coefficient is the real Möbius sum over lower cube points.
Proposition1.6.4
Group: Chapter 1: Generalities on Boolean functions (40)
Group member previews
Preview
Definition 1.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Proposition 5.2.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-2proposition-5page-21fidelity-exact

Proposition 5 (Carlet, p. 21). Let P(x)=\sum_{S\subseteq[n]}\lambda_Sx^S \in\mathbb R[x_1,\ldots,x_n]/(x_1^2-x_1,\ldots,x_n^2-x_n). The function represented by P is integer-valued on V_n if and only if \lambda_S\in\mathbb Z for every S\subseteq[n]. Under this integrality hypothesis, P is Boolean-valued if and only if \sum_{x\in V_n}P(x)^2=\sum_{x\in V_n}P(x).

Lean code for Proposition1.6.4●4 declarations
  • defdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean
    complete
    def CryptBoolean.IsIntegerValued {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) : Prop
    def CryptBoolean.IsIntegerValued {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  Prop
    A pseudo-Boolean function is integer-valued when each value is the cast of an integer.
  • defdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean
    complete
    def CryptBoolean.IsBooleanValued {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) : Prop
    def CryptBoolean.IsBooleanValued {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  Prop
    A pseudo-Boolean function is Boolean-valued when every value is zero or one.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean
    complete
    theorem CryptBoolean.numericalEval_integerValued_iff {n : ℕ}
  (c : FABL.NumericalCoefficients n) :
  CryptBoolean.IsIntegerValued (FABL.numericalEval c) ↔
    ∀ (S : Finset (Fin n)), ∃ z, c S = ↑z
    theorem CryptBoolean.numericalEval_integerValued_iff
  {n : ℕ}
  (c : FABL.NumericalCoefficients n) :
  CryptBoolean.IsIntegerValued
      (FABL.numericalEval c) ↔
    ∀ (S : Finset (Fin n)), ∃ z, c S = ↑z
    Carlet Proposition 5: an NNF is integer-valued exactly when all coefficients are integers.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean
    complete
    theorem CryptBoolean.numericalEval_booleanValued_iff_sum_sq_eq_sum {n : ℕ}
  (c : FABL.NumericalCoefficients n)
  (hc : ∀ (S : Finset (Fin n)), ∃ z, c S = ↑z) :
  CryptBoolean.IsBooleanValued (FABL.numericalEval c) ↔
    ∑ x, FABL.numericalEval c x ^ 2 = ∑ x, FABL.numericalEval c x
    theorem CryptBoolean.numericalEval_booleanValued_iff_sum_sq_eq_sum
  {n : ℕ}
  (c : FABL.NumericalCoefficients n)
  (hc :
    ∀ (S : Finset (Fin n)),
      ∃ z, c S = ↑z) :
  CryptBoolean.IsBooleanValued
      (FABL.numericalEval c) ↔
    ∑ x, FABL.numericalEval c x ^ 2 =
      ∑ x, FABL.numericalEval c x
    Carlet Proposition 5: for integral NNF coefficients, the sum-of-squares identity
characterizes Boolean-valued evaluation.