1.7. Numerical normal form🔗

Theorem1.7.1

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 1.3.10

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.7.1●10 declarations

abbrevdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

abbrev CryptBoolean.PseudoBooleanFunction (n : ℕ) : Type

abbrev CryptBoolean.PseudoBooleanFunction
  (n : ℕ) : Type

A real-valued pseudo-Boolean function on the binary cube.

abbrevdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

abbrev CryptBoolean.NumericalCoefficients (n : ℕ) : Type

abbrev CryptBoolean.NumericalCoefficients
  (n : ℕ) : Type

Coefficients of a square-free numerical normal form.

defdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

def CryptBoolean.numericalMonomial {n : ℕ} (S : Finset (Fin n))
  (x : FABL.F₂Cube n) : ℝ

def CryptBoolean.numericalMonomial {n : ℕ}
  (S : Finset (Fin n))
  (x : FABL.F₂Cube n) : ℝ

The real square-free monomial indexed by `S`.

defdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

def CryptBoolean.numericalEval {n : ℕ}
  (c : CryptBoolean.NumericalCoefficients n) :
  CryptBoolean.PseudoBooleanFunction n

def CryptBoolean.numericalEval {n : ℕ}
  (c :
    CryptBoolean.NumericalCoefficients
      n) :
  CryptBoolean.PseudoBooleanFunction n

Evaluation of a numerical normal form.

defdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

def CryptBoolean.numericalEvalLinear (n : ℕ) :
  CryptBoolean.NumericalCoefficients n →ₗ[ℝ]
    CryptBoolean.PseudoBooleanFunction n

def CryptBoolean.numericalEvalLinear (n : ℕ) :
  CryptBoolean.NumericalCoefficients
      n →ₗ[ℝ]
    CryptBoolean.PseudoBooleanFunction n

Numerical evaluation as a real-linear map.

theoremdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

theorem CryptBoolean.numericalEval_injective {n : ℕ} :
  Function.Injective ⇑(CryptBoolean.numericalEvalLinear n)

theorem CryptBoolean.numericalEval_injective
  {n : ℕ} :
  Function.Injective
    ⇑(CryptBoolean.numericalEvalLinear n)

Numerical evaluation is injective.

theoremdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

theorem CryptBoolean.existsUnique_numericalEval {n : ℕ}
  (φ : CryptBoolean.PseudoBooleanFunction n) :
  ∃! c, CryptBoolean.numericalEval c = φ

theorem CryptBoolean.existsUnique_numericalEval
  {n : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction
      n) :
  ∃! c, CryptBoolean.numericalEval c = φ

Every pseudo-Boolean function has a unique numerical normal form.

defdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

def CryptBoolean.numericalCoeff {n : ℕ}
  (φ : CryptBoolean.PseudoBooleanFunction n) :
  CryptBoolean.NumericalCoefficients n

def CryptBoolean.numericalCoeff {n : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction
      n) :
  CryptBoolean.NumericalCoefficients n

The canonical numerical coefficients supplied by the unique representation theorem.

theoremdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

theorem CryptBoolean.numericalEval_numericalCoeff {n : ℕ}
  (φ : CryptBoolean.PseudoBooleanFunction n) :
  CryptBoolean.numericalEval (CryptBoolean.numericalCoeff φ) = φ

theorem CryptBoolean.numericalEval_numericalCoeff
  {n : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction
      n) :
  CryptBoolean.numericalEval
      (CryptBoolean.numericalCoeff φ) =
    φ

The canonical numerical normal form evaluates to the original function.

theoremdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

theorem CryptBoolean.numericalCoeff_eq_value_sub_lower {n : ℕ}
  (φ : CryptBoolean.PseudoBooleanFunction n) (S : Finset (Fin n)) :
  CryptBoolean.numericalCoeff φ S =
    φ (FABL.f₂CubeOfFinset S) -
      ∑ T ∈ S.powerset.erase S, CryptBoolean.numericalCoeff φ T

theorem CryptBoolean.numericalCoeff_eq_value_sub_lower
  {n : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction n)
  (S : Finset (Fin n)) :
  CryptBoolean.numericalCoeff φ S =
    φ (FABL.f₂CubeOfFinset S) -
      ∑ T ∈ S.powerset.erase S,
        CryptBoolean.numericalCoeff φ T

Each numerical coefficient is determined from the value at `1_S` and lower coefficients.

Proposition1.7.2

uses 1used by 1✓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.7.2●5 declarations

theoremdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

theorem CryptBoolean.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 CryptBoolean.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 CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

def CryptBoolean.numericalMobiusCoeff {n : ℕ}
  (φ : CryptBoolean.PseudoBooleanFunction n) :
  CryptBoolean.NumericalCoefficients n

def CryptBoolean.numericalMobiusCoeff {n : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction
      n) :
  CryptBoolean.NumericalCoefficients n

Carlet Proposition 4: the explicit real Möbius coefficient formula for NNF.

theoremdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

theorem CryptBoolean.numericalEval_numericalMobiusCoeff_f₂CubeOfFinset {n : ℕ}
  (φ : CryptBoolean.PseudoBooleanFunction n) (U : Finset (Fin n)) :
  CryptBoolean.numericalEval (CryptBoolean.numericalMobiusCoeff φ)
      (FABL.f₂CubeOfFinset U) =
    φ (FABL.f₂CubeOfFinset U)

theorem CryptBoolean.numericalEval_numericalMobiusCoeff_f₂CubeOfFinset
  {n : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction n)
  (U : Finset (Fin n)) :
  CryptBoolean.numericalEval
      (CryptBoolean.numericalMobiusCoeff
        φ)
      (FABL.f₂CubeOfFinset U) =
    φ (FABL.f₂CubeOfFinset U)

The explicit real Möbius coefficients reproduce every indicator input.

theoremdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

theorem CryptBoolean.numericalMobiusCoeff_eq_numericalCoeff {n : ℕ}
  (φ : CryptBoolean.PseudoBooleanFunction n) :
  CryptBoolean.numericalMobiusCoeff φ = CryptBoolean.numericalCoeff φ

theorem CryptBoolean.numericalMobiusCoeff_eq_numericalCoeff
  {n : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction
      n) :
  CryptBoolean.numericalMobiusCoeff φ =
    CryptBoolean.numericalCoeff φ

The explicit Möbius coefficient family is the canonical NNF family.

theoremdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

theorem CryptBoolean.numericalCoeff_eq_mobius_sum {n : ℕ}
  (φ : CryptBoolean.PseudoBooleanFunction n) (S : Finset (Fin n)) :
  CryptBoolean.numericalCoeff φ S =
    ∑ T ∈ S.powerset,
      (-1) ^ (S.card - T.card) * φ (FABL.f₂CubeOfFinset T)

theorem CryptBoolean.numericalCoeff_eq_mobius_sum
  {n : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction n)
  (S : Finset (Fin n)) :
  CryptBoolean.numericalCoeff φ S =
    ∑ T ∈ S.powerset,
      (-1) ^ (S.card - T.card) *
        φ (FABL.f₂CubeOfFinset T)

Proposition1.7.3

uses 1used by 0✓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.7.3●4 declarations

defdefined in CryptBoolean/Carlet/Chapter02/NumericalNormalForm.lean

complete

def CryptBoolean.IsIntegerValued {n : ℕ}
  (φ : CryptBoolean.PseudoBooleanFunction n) : Prop

def CryptBoolean.IsIntegerValued {n : ℕ}
  (φ :
    CryptBoolean.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 : ℕ}
  (φ : CryptBoolean.PseudoBooleanFunction n) : Prop

def CryptBoolean.IsBooleanValued {n : ℕ}
  (φ :
    CryptBoolean.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 : CryptBoolean.NumericalCoefficients n) :
  CryptBoolean.IsIntegerValued (CryptBoolean.numericalEval c) ↔
    ∀ (S : Finset (Fin n)), ∃ z, c S = ↑z

theorem CryptBoolean.numericalEval_integerValued_iff
  {n : ℕ}
  (c :
    CryptBoolean.NumericalCoefficients
      n) :
  CryptBoolean.IsIntegerValued
      (CryptBoolean.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 : CryptBoolean.NumericalCoefficients n)
  (hc : ∀ (S : Finset (Fin n)), ∃ z, c S = ↑z) :
  CryptBoolean.IsBooleanValued (CryptBoolean.numericalEval c) ↔
    ∑ x, CryptBoolean.numericalEval c x ^ 2 =
      ∑ x, CryptBoolean.numericalEval c x

theorem CryptBoolean.numericalEval_booleanValued_iff_sum_sq_eq_sum
  {n : ℕ}
  (c :
    CryptBoolean.NumericalCoefficients n)
  (hc :
    ∀ (S : Finset (Fin n)),
      ∃ z, c S = ↑z) :
  CryptBoolean.IsBooleanValued
      (CryptBoolean.numericalEval c) ↔
    ∑ x,
        CryptBoolean.numericalEval c x ^
          2 =
      ∑ x, CryptBoolean.numericalEval c x

Carlet Proposition 5: for integral NNF coefficients, the sum-of-squares identity
characterizes Boolean-valued evaluation.