Cryptographic Boolean Functions in Lean

9.1. Representations🔗

Definition9.1.1
Group: Chapter 9: Symmetric and rotation-symmetric functions (22)
Group member previews
Preview
Theorem 9.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 11
Reverse dependency previews
Preview
Theorem 9.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-10symmetric-functionsdefinitionpage-140page-141fidelity-exact

Symmetric Boolean functions (Carlet, pp. 140--141). Let n\ge0 and f:V_n\to\mathbb F_2. The following conditions are equivalent:

  1. f is invariant under every permutation of its n input coordinates;

  2. f(x)=f(y) whenever w_H(x)=w_H(y);

  3. there is a unique function f^\#: \{0,\ldots,n\}\to\mathbb F_2 such that f(x)=f^\#(w_H(x)) for every x\in V_n.

A function satisfying these conditions is symmetric, and f^\# is its weight profile.

Lean code for Definition9.1.1●18 declarations
  • defdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    def CryptBoolean.IsSymmetricBooleanFunction {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.IsSymmetricBooleanFunction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    A binary Boolean function is symmetric when its sign-cube transport is
invariant under every coordinate permutation.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.positiveCoordinateCount_binaryCubeSignEquiv {n : ℕ}
  (x : FABL.F₂Cube n) :
  FABL.positiveCoordinateCount ((FABL.binaryCubeSignEquiv n) x) =
    n - (FABL.f₂Support x).card
    theorem CryptBoolean.positiveCoordinateCount_binaryCubeSignEquiv
  {n : ℕ} (x : FABL.F₂Cube n) :
  FABL.positiveCoordinateCount
      ((FABL.binaryCubeSignEquiv n) x) =
    n - (FABL.f₂Support x).card
    The sign-cube positive-coordinate count is binary co-weight.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.negativeCoordinateCount_binaryCubeSignEquiv {n : ℕ}
  (x : FABL.F₂Cube n) :
  FABL.negativeCoordinateCount ((FABL.binaryCubeSignEquiv n) x) =
    (FABL.f₂Support x).card
    theorem CryptBoolean.negativeCoordinateCount_binaryCubeSignEquiv
  {n : ℕ} (x : FABL.F₂Cube n) :
  FABL.negativeCoordinateCount
      ((FABL.binaryCubeSignEquiv n) x) =
    (FABL.f₂Support x).card
    The sign-cube negative-coordinate count is binary Hamming weight.
  • defdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    def CryptBoolean.supportCardIndex {n : ℕ} (x : FABL.F₂Cube n) : Fin (n + 1)
    def CryptBoolean.supportCardIndex {n : ℕ}
  (x : FABL.F₂Cube n) : Fin (n + 1)
    The Hamming weight of a binary input as an index in `0, …, n`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.supportCardIndex_val {n : ℕ} (x : FABL.F₂Cube n) :
  ↑(CryptBoolean.supportCardIndex x) = (FABL.f₂Support x).card
    theorem CryptBoolean.supportCardIndex_val {n : ℕ}
  (x : FABL.F₂Cube n) :
  ↑(CryptBoolean.supportCardIndex x) =
    (FABL.f₂Support x).card
  • defdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    def CryptBoolean.canonicalWeightInput (n : ℕ) (r : Fin (n + 1)) :
  FABL.F₂Cube n
    def CryptBoolean.canonicalWeightInput (n : ℕ)
  (r : Fin (n + 1)) : FABL.F₂Cube n
    The canonical binary input of weight `r`, with its first `r` coordinates
equal to one.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.canonicalWeightInput_support_card {n : ℕ}
  (r : Fin (n + 1)) :
  (FABL.f₂Support (CryptBoolean.canonicalWeightInput n r)).card = ↑r
    theorem CryptBoolean.canonicalWeightInput_support_card
  {n : ℕ} (r : Fin (n + 1)) :
  (FABL.f₂Support
        (CryptBoolean.canonicalWeightInput
          n r)).card =
    ↑r
    The canonical weight-`r` input has support cardinality `r`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.supportCardIndex_canonicalWeightInput {n : ℕ}
  (r : Fin (n + 1)) :
  CryptBoolean.supportCardIndex
      (CryptBoolean.canonicalWeightInput n r) =
    r
    theorem CryptBoolean.supportCardIndex_canonicalWeightInput
  {n : ℕ} (r : Fin (n + 1)) :
  CryptBoolean.supportCardIndex
      (CryptBoolean.canonicalWeightInput n
        r) =
    r
  • defdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    def CryptBoolean.symmetricWeightProfile {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Fin (n + 1) → FABL.𝔽₂
    def CryptBoolean.symmetricWeightProfile
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Fin (n + 1) → FABL.𝔽₂
    The canonical weight profile of a Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.isSymmetricBooleanFunction_iff_eq_of_support_card_eq
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsSymmetricBooleanFunction f ↔
    ∀ (x y : FABL.F₂Cube n),
      (FABL.f₂Support x).card = (FABL.f₂Support y).card → f x = f y
    theorem CryptBoolean.isSymmetricBooleanFunction_iff_eq_of_support_card_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsSymmetricBooleanFunction
      f ↔
    ∀ (x y : FABL.F₂Cube n),
      (FABL.f₂Support x).card =
          (FABL.f₂Support y).card →
        f x = f y
    Binary symmetry is equivalent to constancy on every Hamming-weight layer.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.IsSymmetricBooleanFunction.eq_of_support_card_eq {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) {x y : FABL.F₂Cube n}
  (hweight : (FABL.f₂Support x).card = (FABL.f₂Support y).card) :
  f x = f y
    theorem CryptBoolean.IsSymmetricBooleanFunction.eq_of_support_card_eq
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  {x y : FABL.F₂Cube n}
  (hweight :
    (FABL.f₂Support x).card =
      (FABL.f₂Support y).card) :
  f x = f y
    A symmetric Boolean function takes equal values on equal-weight inputs.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.IsSymmetricBooleanFunction.eq_profile {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (x : FABL.F₂Cube n) :
  f x =
    CryptBoolean.symmetricWeightProfile f
      (CryptBoolean.supportCardIndex x)
    theorem CryptBoolean.IsSymmetricBooleanFunction.eq_profile
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (x : FABL.F₂Cube n) :
  f x =
    CryptBoolean.symmetricWeightProfile f
      (CryptBoolean.supportCardIndex x)
    A symmetric Boolean function is recovered from its canonical weight
profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.isSymmetricBooleanFunction_iff_eq_profile {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsSymmetricBooleanFunction f ↔
    ∀ (x : FABL.F₂Cube n),
      f x =
        CryptBoolean.symmetricWeightProfile f
          (CryptBoolean.supportCardIndex x)
    theorem CryptBoolean.isSymmetricBooleanFunction_iff_eq_profile
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsSymmetricBooleanFunction
      f ↔
    ∀ (x : FABL.F₂Cube n),
      f x =
        CryptBoolean.symmetricWeightProfile
          f
          (CryptBoolean.supportCardIndex
            x)
    Symmetry is equivalent to representation by the canonical weight profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.isSymmetricBooleanFunction_iff_existsUnique_weightProfile
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsSymmetricBooleanFunction f ↔
    ∃! profile,
      ∀ (x : FABL.F₂Cube n),
        f x = profile (CryptBoolean.supportCardIndex x)
    theorem CryptBoolean.isSymmetricBooleanFunction_iff_existsUnique_weightProfile
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsSymmetricBooleanFunction
      f ↔
    ∃! profile,
      ∀ (x : FABL.F₂Cube n),
        f x =
          profile
            (CryptBoolean.supportCardIndex
              x)
    A Boolean function is symmetric exactly when it has a unique profile on
the finite set of Hamming weights.
  • defdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    def CryptBoolean.symmetricWeightProfileNat {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (ℓ : ℕ) : FABL.𝔽₂
    def CryptBoolean.symmetricWeightProfileNat
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (ℓ : ℕ) : FABL.𝔽₂
    The canonical weight profile extended by zero outside the cube's weight
range.
  • defdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    def CryptBoolean.symmetricRealWeightProfile {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (ℓ : ℕ) : ℝ
    def CryptBoolean.symmetricRealWeightProfile
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (ℓ : ℕ) : ℝ
    The real `0/1` embedding of the canonical binary weight profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.symmetricWeightProfileNat_supportCardIndex {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) :
  CryptBoolean.symmetricWeightProfileNat f (FABL.f₂Support x).card =
    CryptBoolean.symmetricWeightProfile f
      (CryptBoolean.supportCardIndex x)
    theorem CryptBoolean.symmetricWeightProfileNat_supportCardIndex
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  CryptBoolean.symmetricWeightProfileNat f
      (FABL.f₂Support x).card =
    CryptBoolean.symmetricWeightProfile f
      (CryptBoolean.supportCardIndex x)
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.IsSymmetricBooleanFunction.booleanRealEmbedding_eq_profile
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding f x =
    CryptBoolean.symmetricRealWeightProfile f (FABL.f₂Support x).card
    theorem CryptBoolean.IsSymmetricBooleanFunction.booleanRealEmbedding_eq_profile
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding f x =
    CryptBoolean.symmetricRealWeightProfile
      f (FABL.f₂Support x).card
    The real embedding of a symmetric Boolean function is recovered from its
real weight profile.
Theorem9.1.2
Group: Chapter 9: Symmetric and rotation-symmetric functions (22)
Group member previews
Preview
Definition 9.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 2
Reverse dependency previews
Preview
Theorem 9.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-10relation-71symmetric-functionsnumerical-normal-formelementary-symmetric-functionspage-141fidelity-exact

Relation (71) (Carlet, p. 141). For 0\le r\le n, let \varphi_r:V_n\to\mathbb F_2 be the indicator of the vectors of Hamming weight r. The coefficient of x^I in the numerical normal form of \varphi_r is zero when r>|I| and otherwise is (-1)^{|I|-r}\binom{|I|}{r}. For 0\le i\le n, define the i-th elementary symmetric pseudo-Boolean function by S_i(x)=\sum_{\substack{I\subseteq\{1,\ldots,n\}\\|I|=i}} \prod_{j\in I}x_j. If f is symmetric with weight profile f^\#, identify \mathbb F_2 with \{0,1\}\subset\mathbb Z and set c_i=\sum_{r=0}^{i}f^\#(r)(-1)^{i-r}\binom ir. Then the numerical normal form of f is f(x)=\sum_{i=0}^{n}c_iS_i(x), and its numerical degree is \max\{i\mid c_i\ne0\}, with value zero for the zero function.

Lean code for Theorem9.1.2●16 declarations
  • defdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    def CryptBoolean.weightLayerIndicator {n : ℕ} (r : Fin (n + 1)) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.weightLayerIndicator {n : ℕ}
  (r : Fin (n + 1)) :
  CryptBoolean.BooleanFunction n
    The Boolean indicator of the Hamming-weight layer indexed by `r`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.weightLayerIndicator_apply_self {n : ℕ}
  (x : FABL.F₂Cube n) :
  CryptBoolean.weightLayerIndicator (CryptBoolean.supportCardIndex x)
      x =
    1
    theorem CryptBoolean.weightLayerIndicator_apply_self
  {n : ℕ} (x : FABL.F₂Cube n) :
  CryptBoolean.weightLayerIndicator
      (CryptBoolean.supportCardIndex x)
      x =
    1
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.isSymmetricBooleanFunction_weightLayerIndicator {n : ℕ}
  (r : Fin (n + 1)) :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.weightLayerIndicator r)
    theorem CryptBoolean.isSymmetricBooleanFunction_weightLayerIndicator
  {n : ℕ} (r : Fin (n + 1)) :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.weightLayerIndicator r)
    Every Hamming-weight layer indicator is symmetric.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Symmetric.lean
    complete
    theorem CryptBoolean.IsSymmetricBooleanFunction.sum_weightLayerIndicator {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  f =
    ∑ r,
      CryptBoolean.symmetricWeightProfile f r •
        CryptBoolean.weightLayerIndicator r
    theorem CryptBoolean.IsSymmetricBooleanFunction.sum_weightLayerIndicator
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  f =
    ∑ r,
      CryptBoolean.symmetricWeightProfile
          f r •
        CryptBoolean.weightLayerIndicator
          r
    Every symmetric Boolean function is the sum of its profile-weighted layer
indicators.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.symmetricWeightProfileNat_weightLayerIndicator {n : ℕ}
  (r : Fin (n + 1)) (ℓ : ℕ) :
  CryptBoolean.symmetricWeightProfileNat
      (CryptBoolean.weightLayerIndicator r) ℓ =
    if ℓ = ↑r then 1 else 0
    theorem CryptBoolean.symmetricWeightProfileNat_weightLayerIndicator
  {n : ℕ} (r : Fin (n + 1)) (ℓ : ℕ) :
  CryptBoolean.symmetricWeightProfileNat
      (CryptBoolean.weightLayerIndicator
        r)
      ℓ =
    if ℓ = ↑r then 1 else 0
    The binary profile of a weight-layer indicator is the corresponding
Kronecker delta.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.symmetricRealWeightProfile_weightLayerIndicator {n : ℕ}
  (r : Fin (n + 1)) (ℓ : ℕ) :
  CryptBoolean.symmetricRealWeightProfile
      (CryptBoolean.weightLayerIndicator r) ℓ =
    if ℓ = ↑r then 1 else 0
    theorem CryptBoolean.symmetricRealWeightProfile_weightLayerIndicator
  {n : ℕ} (r : Fin (n + 1)) (ℓ : ℕ) :
  CryptBoolean.symmetricRealWeightProfile
      (CryptBoolean.weightLayerIndicator
        r)
      ℓ =
    if ℓ = ↑r then 1 else 0
    The real profile of a weight-layer indicator is the corresponding
Kronecker delta.
  • defdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    def CryptBoolean.elementarySymmetricNumericalCoefficients (n i : ℕ) :
  FABL.NumericalCoefficients n
    def CryptBoolean.elementarySymmetricNumericalCoefficients
  (n i : ℕ) : FABL.NumericalCoefficients n
    The degree-`i` elementary symmetric numerical coefficient family.
  • defdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    def CryptBoolean.elementarySymmetricNumerical (n i : ℕ) :
  FABL.PseudoBooleanFunction n
    def CryptBoolean.elementarySymmetricNumerical
  (n i : ℕ) : FABL.PseudoBooleanFunction n
    The degree-`i` elementary symmetric pseudo-Boolean function.
  • defdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    def CryptBoolean.symmetricNumericalExpansion (n : ℕ) (coefficient : ℕ → ℝ) :
  FABL.PseudoBooleanFunction n
    def CryptBoolean.symmetricNumericalExpansion
  (n : ℕ) (coefficient : ℕ → ℝ) :
  FABL.PseudoBooleanFunction n
    A numerical linear combination of the elementary symmetric basis.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.elementarySymmetricNumerical_apply {n : ℕ} (i : ℕ)
  (x : FABL.F₂Cube n) :
  CryptBoolean.elementarySymmetricNumerical n i x =
    ↑((FABL.f₂Support x).card.choose i)
    theorem CryptBoolean.elementarySymmetricNumerical_apply
  {n : ℕ} (i : ℕ) (x : FABL.F₂Cube n) :
  CryptBoolean.elementarySymmetricNumerical
      n i x =
    ↑((FABL.f₂Support x).card.choose i)
    The numerical elementary symmetric function is the binomial coefficient of
the input weight.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.numericalEval_cardCoefficients_eq_symmetricNumericalExpansion
  {n : ℕ} (coefficient : ℕ → ℝ) :
  (FABL.numericalEval fun S => coefficient S.card) =
    CryptBoolean.symmetricNumericalExpansion n coefficient
    theorem CryptBoolean.numericalEval_cardCoefficients_eq_symmetricNumericalExpansion
  {n : ℕ} (coefficient : ℕ → ℝ) :
  (FABL.numericalEval fun S =>
      coefficient S.card) =
    CryptBoolean.symmetricNumericalExpansion
      n coefficient
    Coefficients depending only on subset cardinality evaluate in the
numerical elementary symmetric basis.
  • defdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    def CryptBoolean.symmetricNumericalCoefficient (profile : ℕ → ℝ) (i : ℕ) : ℝ
    def CryptBoolean.symmetricNumericalCoefficient
  (profile : ℕ → ℝ) (i : ℕ) : ℝ
    Relation (71)'s coefficient transform for a real weight profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.numericalCoeff_eq_symmetricNumericalCoefficient {n : ℕ}
  (f : FABL.PseudoBooleanFunction n) (profile : ℕ → ℝ)
  (hf : ∀ (x : FABL.F₂Cube n), f x = profile (FABL.f₂Support x).card)
  (S : Finset (Fin n)) :
  FABL.numericalCoeff f S =
    CryptBoolean.symmetricNumericalCoefficient profile S.card
    theorem CryptBoolean.numericalCoeff_eq_symmetricNumericalCoefficient
  {n : ℕ}
  (f : FABL.PseudoBooleanFunction n)
  (profile : ℕ → ℝ)
  (hf :
    ∀ (x : FABL.F₂Cube n),
      f x =
        profile (FABL.f₂Support x).card)
  (S : Finset (Fin n)) :
  FABL.numericalCoeff f S =
    CryptBoolean.symmetricNumericalCoefficient
      profile S.card
    Relation (71): the NNF coefficient of a function depending only on weight
depends only on the size of its variable set and is the binomial Möbius
transform of the weight profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.numericalCoeff_booleanRealEmbedding_weightLayerIndicator
  {n : ℕ} (r : Fin (n + 1)) (S : Finset (Fin n)) :
  FABL.numericalCoeff
      (FABL.booleanRealEmbedding (CryptBoolean.weightLayerIndicator r))
      S =
    if ↑r ≤ S.card then (-1) ^ (S.card - ↑r) * ↑(S.card.choose ↑r)
    else 0
    theorem CryptBoolean.numericalCoeff_booleanRealEmbedding_weightLayerIndicator
  {n : ℕ} (r : Fin (n + 1))
  (S : Finset (Fin n)) :
  FABL.numericalCoeff
      (FABL.booleanRealEmbedding
        (CryptBoolean.weightLayerIndicator
          r))
      S =
    if ↑r ≤ S.card then
      (-1) ^ (S.card - ↑r) *
        ↑(S.card.choose ↑r)
    else 0
    Relation (71) for a single Hamming-weight layer: its numerical-normal-form
coefficient is the signed binomial coefficient supported in degrees at least
the layer weight.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.symmetricNumericalExpansion_symmetricNumericalCoefficient_eq
  {n : ℕ} (f : FABL.PseudoBooleanFunction n) (profile : ℕ → ℝ)
  (hf : ∀ (x : FABL.F₂Cube n), f x = profile (FABL.f₂Support x).card) :
  CryptBoolean.symmetricNumericalExpansion n
      (CryptBoolean.symmetricNumericalCoefficient profile) =
    f
    theorem CryptBoolean.symmetricNumericalExpansion_symmetricNumericalCoefficient_eq
  {n : ℕ}
  (f : FABL.PseudoBooleanFunction n)
  (profile : ℕ → ℝ)
  (hf :
    ∀ (x : FABL.F₂Cube n),
      f x =
        profile (FABL.f₂Support x).card) :
  CryptBoolean.symmetricNumericalExpansion
      n
      (CryptBoolean.symmetricNumericalCoefficient
        profile) =
    f
    Relation (71): a pseudo-Boolean function depending only on Hamming weight
is its binomial-Möbius linear combination of the numerical elementary
symmetric functions.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.relation_71_symmetricNumericalExpansion {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  CryptBoolean.symmetricNumericalExpansion n
      (CryptBoolean.symmetricNumericalCoefficient
        (CryptBoolean.symmetricRealWeightProfile f)) =
    FABL.booleanRealEmbedding f
    theorem CryptBoolean.relation_71_symmetricNumericalExpansion
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.symmetricNumericalExpansion
      n
      (CryptBoolean.symmetricNumericalCoefficient
        (CryptBoolean.symmetricRealWeightProfile
          f)) =
    FABL.booleanRealEmbedding f
    Relation (71) for a symmetric Boolean function in its canonical real
weight profile.
Theorem9.1.3
Group: Chapter 9: Symmetric and rotation-symmetric functions (22)
Group member previews
Preview
Definition 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 9.4.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-10symmetric-functionsunivariate-representationnumerical-normal-formpage-141page-142fidelity-exact

Univariate binomial representation (Carlet, pp. 141--142). Let f:V_n\to\mathbb F_2 be symmetric, let f^\# be its weight profile, and let c_0,\ldots,c_n be the coefficients in Relation (71). For an indeterminate z, put \binom zi=\frac{z(z-1)\cdots(z-i+1)}{i!}, \qquad \binom z0=1, and P_f(z)=\sum_{i=0}^{n}c_i\binom zi. Then P_f(r)=f^\#(r) for every integer 0\le r\le n. It is the unique rational polynomial of degree at most n with these n+1 prescribed values, and \deg(P_f)=\deg_{\mathrm{NNF}}(f). Moreover S_i(x)=\binom{w_H(x)}i, so the multivariate numerical normal form of f is obtained by substituting z=w_H(x) in P_f.

Lean code for Theorem9.1.3●21 declarations
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.functionNumericalDegree_le_dimension {n : ℕ}
  (f : FABL.PseudoBooleanFunction n) :
  FABL.functionNumericalDegree f ≤ n
    theorem CryptBoolean.functionNumericalDegree_le_dimension
  {n : ℕ}
  (f : FABL.PseudoBooleanFunction n) :
  FABL.functionNumericalDegree f ≤ n
    Numerical degree is bounded by the ambient cube dimension.
  • defdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    def CryptBoolean.binomialBasisPolynomial (i : ℕ) : Polynomial ℝ
    def CryptBoolean.binomialBasisPolynomial
  (i : ℕ) : Polynomial ℝ
    The binomial polynomial `z ↦ choose(z,i)` over the reals.
  • defdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    def CryptBoolean.binomialBasisPolynomialRat (i : ℕ) : Polynomial ℚ
    def CryptBoolean.binomialBasisPolynomialRat
  (i : ℕ) : Polynomial ℚ
    The binomial polynomial `z ↦ choose(z,i)` over the rationals.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.map_binomialBasisPolynomialRat (i : ℕ) :
  Polynomial.map (algebraMap ℚ ℝ)
      (CryptBoolean.binomialBasisPolynomialRat i) =
    CryptBoolean.binomialBasisPolynomial i
    theorem CryptBoolean.map_binomialBasisPolynomialRat
  (i : ℕ) :
  Polynomial.map (algebraMap ℚ ℝ)
      (CryptBoolean.binomialBasisPolynomialRat
        i) =
    CryptBoolean.binomialBasisPolynomial i
    Rational binomial-basis polynomials map to their real counterparts.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.eval_binomialBasisPolynomial_nat (z i : ℕ) :
  Polynomial.eval (↑z) (CryptBoolean.binomialBasisPolynomial i) =
    ↑(z.choose i)
    theorem CryptBoolean.eval_binomialBasisPolynomial_nat
  (z i : ℕ) :
  Polynomial.eval (↑z)
      (CryptBoolean.binomialBasisPolynomial
        i) =
    ↑(z.choose i)
    The binomial basis polynomial takes the expected value at every natural
number.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.natDegree_binomialBasisPolynomial (i : ℕ) :
  (CryptBoolean.binomialBasisPolynomial i).natDegree = i
    theorem CryptBoolean.natDegree_binomialBasisPolynomial
  (i : ℕ) :
  (CryptBoolean.binomialBasisPolynomial
        i).natDegree =
    i
    The degree of the `i`th binomial basis polynomial is `i`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.eval_binomialBasisPolynomialRat_nat (z i : ℕ) :
  Polynomial.eval (↑z) (CryptBoolean.binomialBasisPolynomialRat i) =
    ↑(z.choose i)
    theorem CryptBoolean.eval_binomialBasisPolynomialRat_nat
  (z i : ℕ) :
  Polynomial.eval (↑z)
      (CryptBoolean.binomialBasisPolynomialRat
        i) =
    ↑(z.choose i)
    The rational binomial-basis polynomial takes the expected value at every
natural number.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.natDegree_binomialBasisPolynomialRat (i : ℕ) :
  (CryptBoolean.binomialBasisPolynomialRat i).natDegree = i
    theorem CryptBoolean.natDegree_binomialBasisPolynomialRat
  (i : ℕ) :
  (CryptBoolean.binomialBasisPolynomialRat
        i).natDegree =
    i
    The degree of the rational `i`th binomial-basis polynomial is `i`.
  • defdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    def CryptBoolean.symmetricProfilePolynomial {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Polynomial ℝ
    def CryptBoolean.symmetricProfilePolynomial
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Polynomial ℝ
    The univariate binomial-basis polynomial representing a symmetric Boolean
function's real weight profile.
  • defdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    def CryptBoolean.symmetricProfilePolynomialRat {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Polynomial ℚ
    def CryptBoolean.symmetricProfilePolynomialRat
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Polynomial ℚ
    The rational univariate polynomial whose binomial-basis coefficients are
the integral coefficients from Relation (71).
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.map_symmetricProfilePolynomialRat {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Polynomial.map (algebraMap ℚ ℝ)
      (CryptBoolean.symmetricProfilePolynomialRat f) =
    CryptBoolean.symmetricProfilePolynomial f
    theorem CryptBoolean.map_symmetricProfilePolynomialRat
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Polynomial.map (algebraMap ℚ ℝ)
      (CryptBoolean.symmetricProfilePolynomialRat
        f) =
    CryptBoolean.symmetricProfilePolynomial
      f
    The rational profile polynomial maps to the real profile polynomial.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.booleanRealEmbedding_eq_zero_iff {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding f x = 0 ↔ f x = 0
    theorem CryptBoolean.booleanRealEmbedding_eq_zero_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding f x = 0 ↔
    f x = 0
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.booleanRealEmbedding_eq_one_iff {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding f x = 1 ↔ f x = 1
    theorem CryptBoolean.booleanRealEmbedding_eq_one_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding f x = 1 ↔
    f x = 1
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.booleanRealEmbedding_apply_eq_val {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding f x = ↑(ZMod.val (f x))
    theorem CryptBoolean.booleanRealEmbedding_apply_eq_val
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding f x =
    ↑(ZMod.val (f x))
    The real Boolean embedding is the real cast of the canonical
representative of its bit value.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.eval_symmetricProfilePolynomial {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (r : Fin (n + 1)) :
  Polynomial.eval (↑↑r) (CryptBoolean.symmetricProfilePolynomial f) =
    FABL.booleanRealEmbedding f (CryptBoolean.canonicalWeightInput n r)
    theorem CryptBoolean.eval_symmetricProfilePolynomial
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (r : Fin (n + 1)) :
  Polynomial.eval (↑↑r)
      (CryptBoolean.symmetricProfilePolynomial
        f) =
    FABL.booleanRealEmbedding f
      (CryptBoolean.canonicalWeightInput n
        r)
    The binomial-basis polynomial represents the real weight profile at every
weight in the cube.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.eval_symmetricProfilePolynomialRat {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (r : Fin (n + 1)) :
  Polynomial.eval (↑↑r) (CryptBoolean.symmetricProfilePolynomialRat f) =
    ↑(ZMod.val (CryptBoolean.symmetricWeightProfile f r))
    theorem CryptBoolean.eval_symmetricProfilePolynomialRat
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (r : Fin (n + 1)) :
  Polynomial.eval (↑↑r)
      (CryptBoolean.symmetricProfilePolynomialRat
        f) =
    ↑(ZMod.val
        (CryptBoolean.symmetricWeightProfile
          f r))
    The rational profile polynomial represents the binary weight profile at
every weight in the cube.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.natDegree_symmetricProfilePolynomial_le {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  (CryptBoolean.symmetricProfilePolynomial f).natDegree ≤
    FABL.functionNumericalDegree (FABL.booleanRealEmbedding f)
    theorem CryptBoolean.natDegree_symmetricProfilePolynomial_le
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  (CryptBoolean.symmetricProfilePolynomial
        f).natDegree ≤
    FABL.functionNumericalDegree
      (FABL.booleanRealEmbedding f)
    The representing univariate polynomial has degree at most the numerical
degree of the symmetric Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.natDegree_symmetricProfilePolynomial_eq {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  (CryptBoolean.symmetricProfilePolynomial f).natDegree =
    FABL.functionNumericalDegree (FABL.booleanRealEmbedding f)
    theorem CryptBoolean.natDegree_symmetricProfilePolynomial_eq
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  (CryptBoolean.symmetricProfilePolynomial
        f).natDegree =
    FABL.functionNumericalDegree
      (FABL.booleanRealEmbedding f)
    The univariate profile polynomial has exactly the numerical degree of a
symmetric Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.natDegree_symmetricProfilePolynomialRat_eq {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  (CryptBoolean.symmetricProfilePolynomialRat f).natDegree =
    FABL.functionNumericalDegree (FABL.booleanRealEmbedding f)
    theorem CryptBoolean.natDegree_symmetricProfilePolynomialRat_eq
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  (CryptBoolean.symmetricProfilePolynomialRat
        f).natDegree =
    FABL.functionNumericalDegree
      (FABL.booleanRealEmbedding f)
    The rational univariate profile polynomial has exactly the numerical
degree of a symmetric Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.eq_symmetricProfilePolynomial_of_natDegree_le_of_eval_eq
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (p : Polynomial ℝ)
  (hp : p.natDegree ≤ n)
  (heval :
    ∀ (r : Fin (n + 1)),
      Polynomial.eval (↑↑r) p =
        FABL.booleanRealEmbedding f
          (CryptBoolean.canonicalWeightInput n r)) :
  p = CryptBoolean.symmetricProfilePolynomial f
    theorem CryptBoolean.eq_symmetricProfilePolynomial_of_natDegree_le_of_eval_eq
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (p : Polynomial ℝ)
  (hp : p.natDegree ≤ n)
  (heval :
    ∀ (r : Fin (n + 1)),
      Polynomial.eval (↑↑r) p =
        FABL.booleanRealEmbedding f
          (CryptBoolean.canonicalWeightInput
            n r)) :
  p =
    CryptBoolean.symmetricProfilePolynomial
      f
    The profile polynomial is the unique real polynomial of degree at most
`n` taking the prescribed binary values on the weights `0,…,n`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.eq_symmetricProfilePolynomialRat_of_natDegree_le_of_eval_eq
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (p : Polynomial ℚ)
  (hp : p.natDegree ≤ n)
  (heval :
    ∀ (r : Fin (n + 1)),
      Polynomial.eval (↑↑r) p =
        ↑(ZMod.val (CryptBoolean.symmetricWeightProfile f r))) :
  p = CryptBoolean.symmetricProfilePolynomialRat f
    theorem CryptBoolean.eq_symmetricProfilePolynomialRat_of_natDegree_le_of_eval_eq
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (p : Polynomial ℚ)
  (hp : p.natDegree ≤ n)
  (heval :
    ∀ (r : Fin (n + 1)),
      Polynomial.eval (↑↑r) p =
        ↑(ZMod.val
            (CryptBoolean.symmetricWeightProfile
              f r))) :
  p =
    CryptBoolean.symmetricProfilePolynomialRat
      f
    The rational profile polynomial is the unique rational polynomial of
degree at most `n` taking the prescribed binary values on weights `0,…,n`.
Theorem9.1.4
Group: Chapter 9: Symmetric and rotation-symmetric functions (22)
Group member previews
Preview
Definition 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 1.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 9.1.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-10relation-72symmetric-functionsalgebraic-normal-formelementary-symmetric-functionslucas-theorempage-142fidelity-exact

Relation (72) (Carlet, p. 142). For 0\le i\le n, define the i-th elementary symmetric Boolean function by \sigma_i(x)=\sum_{\substack{I\subseteq\{1,\ldots,n\}\\|I|=i}} \prod_{j\in I}x_j \quad\text{in }\mathbb F_2. Then \sigma_i(x)=\binom{w_H(x)}i\pmod 2. Write j\preceq i when every one-bit of j is also a one-bit of i. If f is symmetric with weight profile f^\#, then its algebraic normal form is f(x)=\sum_{i=0}^{n}\lambda_i\sigma_i(x), \qquad \lambda_i=\sum_{j\preceq i}f^\#(j) \quad\text{in }\mathbb F_2. Conversely, f^\#(i)=\sum_{j\preceq i}\lambda_j \quad\text{in }\mathbb F_2. Thus these transforms are inverse, and the algebraic degree of f is \max\{i\mid\lambda_i=1\}, with value zero for the zero function.

Lean code for Theorem9.1.4●15 declarations
  • defdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    def CryptBoolean.elementarySymmetricANFCoefficients (n i : ℕ) :
  FABL.ANFCoefficients n
    def CryptBoolean.elementarySymmetricANFCoefficients
  (n i : ℕ) : FABL.ANFCoefficients n
    The degree-`i` elementary symmetric algebraic coefficient family.
  • defdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    def CryptBoolean.elementarySymmetricBoolean (n i : ℕ) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.elementarySymmetricBoolean
  (n i : ℕ) :
  CryptBoolean.BooleanFunction n
    The degree-`i` elementary symmetric Boolean function.
  • defdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    def CryptBoolean.symmetricANFExpansion (n : ℕ) (coefficient : ℕ → FABL.𝔽₂) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.symmetricANFExpansion (n : ℕ)
  (coefficient : ℕ → FABL.𝔽₂) :
  CryptBoolean.BooleanFunction n
    A binary linear combination of the elementary symmetric ANF basis.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.elementarySymmetricBoolean_apply {n : ℕ} (i : ℕ)
  (x : FABL.F₂Cube n) :
  CryptBoolean.elementarySymmetricBoolean n i x =
    ↑((FABL.f₂Support x).card.choose i)
    theorem CryptBoolean.elementarySymmetricBoolean_apply
  {n : ℕ} (i : ℕ) (x : FABL.F₂Cube n) :
  CryptBoolean.elementarySymmetricBoolean
      n i x =
    ↑((FABL.f₂Support x).card.choose i)
    The Boolean elementary symmetric function is the binomial coefficient of
the input weight reduced modulo two.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.isSymmetricBooleanFunction_elementarySymmetricBoolean
  {n : ℕ} (i : ℕ) :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.elementarySymmetricBoolean n i)
    theorem CryptBoolean.isSymmetricBooleanFunction_elementarySymmetricBoolean
  {n : ℕ} (i : ℕ) :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.elementarySymmetricBoolean
      n i)
    Every algebraic elementary symmetric Boolean function is symmetric.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.anfCoeff_elementarySymmetricBoolean {n : ℕ} (i : ℕ) :
  FABL.anfCoeff (CryptBoolean.elementarySymmetricBoolean n i) =
    CryptBoolean.elementarySymmetricANFCoefficients n i
    theorem CryptBoolean.anfCoeff_elementarySymmetricBoolean
  {n : ℕ} (i : ℕ) :
  FABL.anfCoeff
      (CryptBoolean.elementarySymmetricBoolean
        n i) =
    CryptBoolean.elementarySymmetricANFCoefficients
      n i
    The declared algebraic coefficient family is the canonical ANF of the
elementary symmetric Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.anfEval_cardCoefficients_eq_symmetricANFExpansion {n : ℕ}
  (coefficient : ℕ → FABL.𝔽₂) :
  (FABL.anfEval fun S => coefficient S.card) =
    CryptBoolean.symmetricANFExpansion n coefficient
    theorem CryptBoolean.anfEval_cardCoefficients_eq_symmetricANFExpansion
  {n : ℕ} (coefficient : ℕ → FABL.𝔽₂) :
  (FABL.anfEval fun S =>
      coefficient S.card) =
    CryptBoolean.symmetricANFExpansion n
      coefficient
    Coefficients depending only on subset cardinality evaluate in the binary
elementary symmetric basis.
  • defdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    def CryptBoolean.symmetricANFCoefficient (profile : ℕ → FABL.𝔽₂) (i : ℕ) :
  FABL.𝔽₂
    def CryptBoolean.symmetricANFCoefficient
  (profile : ℕ → FABL.𝔽₂) (i : ℕ) :
  FABL.𝔽₂
    Relation (72)'s coefficient transform for a binary weight profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.anfCoeff_eq_symmetricANFCoefficient {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (profile : ℕ → FABL.𝔽₂)
  (hf : ∀ (x : FABL.F₂Cube n), f x = profile (FABL.f₂Support x).card)
  (S : Finset (Fin n)) :
  FABL.anfCoeff f S =
    CryptBoolean.symmetricANFCoefficient profile S.card
    theorem CryptBoolean.anfCoeff_eq_symmetricANFCoefficient
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (profile : ℕ → FABL.𝔽₂)
  (hf :
    ∀ (x : FABL.F₂Cube n),
      f x =
        profile (FABL.f₂Support x).card)
  (S : Finset (Fin n)) :
  FABL.anfCoeff f S =
    CryptBoolean.symmetricANFCoefficient
      profile S.card
    Relation (72): the ANF coefficient of a symmetric Boolean function depends
only on the size of its variable set and is the characteristic-two binomial
transform of its weight profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.symmetricANFExpansion_symmetricANFCoefficient_eq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (profile : ℕ → FABL.𝔽₂)
  (hf : ∀ (x : FABL.F₂Cube n), f x = profile (FABL.f₂Support x).card) :
  CryptBoolean.symmetricANFExpansion n
      (CryptBoolean.symmetricANFCoefficient profile) =
    f
    theorem CryptBoolean.symmetricANFExpansion_symmetricANFCoefficient_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (profile : ℕ → FABL.𝔽₂)
  (hf :
    ∀ (x : FABL.F₂Cube n),
      f x =
        profile (FABL.f₂Support x).card) :
  CryptBoolean.symmetricANFExpansion n
      (CryptBoolean.symmetricANFCoefficient
        profile) =
    f
    Relation (72): a symmetric Boolean function is its binomial transform in
the algebraic elementary symmetric basis.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean
    complete
    theorem CryptBoolean.relation_72_symmetricANFExpansion {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  CryptBoolean.symmetricANFExpansion n
      (CryptBoolean.symmetricANFCoefficient
        (CryptBoolean.symmetricWeightProfileNat f)) =
    f
    theorem CryptBoolean.relation_72_symmetricANFExpansion
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.symmetricANFExpansion n
      (CryptBoolean.symmetricANFCoefficient
        (CryptBoolean.symmetricWeightProfileNat
          f)) =
    f
    Relation (72) for a symmetric Boolean function in its canonical binary
weight profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_le_iff_symmetricANFCoefficient
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (d : ℕ) :
  FABL.functionAlgebraicDegree f ≤ d ↔
    ∀ k ≤ n,
      d < k →
        CryptBoolean.symmetricANFCoefficient
            (CryptBoolean.symmetricWeightProfileNat f) k =
          0
    theorem CryptBoolean.functionAlgebraicDegree_le_iff_symmetricANFCoefficient
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (d : ℕ) :
  FABL.functionAlgebraicDegree f ≤ d ↔
    ∀ k ≤ n,
      d < k →
        CryptBoolean.symmetricANFCoefficient
            (CryptBoolean.symmetricWeightProfileNat
              f)
            k =
          0
    The algebraic-degree analogue of Relation (73): higher characteristic-two
binomial differences of the profile are exactly the higher ANF layers.
  • defdefined in CryptBoolean/Carlet/Chapter10/Periodicity.lean
    complete
    def CryptBoolean.BitCovers (n k : ℕ) : Prop
    def CryptBoolean.BitCovers (n k : ℕ) : Prop
    `n` covers `k` in binary when every set bit of `k` is also set in `n`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Periodicity.lean
    complete
    theorem CryptBoolean.natCast_choose_eq_one_iff_bitCovers (n k : ℕ) :
  ↑(n.choose k) = 1 ↔ CryptBoolean.BitCovers n k
    theorem CryptBoolean.natCast_choose_eq_one_iff_bitCovers
  (n k : ℕ) :
  ↑(n.choose k) = 1 ↔
    CryptBoolean.BitCovers n k
    Lucas's theorem modulo two: a binomial coefficient is odd exactly when
its lower index is covered bitwise by its upper index.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Periodicity.lean
    complete
    theorem CryptBoolean.symmetricANFCoefficient_involution (profile : ℕ → FABL.𝔽₂)
  (k : ℕ) :
  CryptBoolean.symmetricANFCoefficient
      (CryptBoolean.symmetricANFCoefficient profile) k =
    profile k
    theorem CryptBoolean.symmetricANFCoefficient_involution
  (profile : ℕ → FABL.𝔽₂) (k : ℕ) :
  CryptBoolean.symmetricANFCoefficient
      (CryptBoolean.symmetricANFCoefficient
        profile)
      k =
    profile k
    In characteristic two the binomial transform is an involution.
Theorem9.1.5
Group: Chapter 9: Symmetric and rotation-symmetric functions (22)
Group member previews
Preview
Definition 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Definition 1.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 9.3.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-10symmetric-functionsalgebraic-degreeaffine-functionsquadratic-functionsclassificationpage-142fidelity-explicit-nonvacuous-ranges

Linear and quadratic symmetric functions (Carlet, p. 142). Over \mathbb F_2, let p_n(x)=x_1+\cdots+x_n, \qquad q_n(x)=\sum_{1\le i<j\le n}x_ix_j. If n>0, a symmetric function f:V_n\to\mathbb F_2 has algebraic degree exactly one if and only if f=p_n+b for some b\in\mathbb F_2. Equivalently, f^\#(r+1)=f^\#(r)+1\qquad(0\le r<n). If n\ge2, the function f has algebraic degree exactly two if and only if f=q_n+ap_n+b for some a,b\in\mathbb F_2. Equivalently, f^\#(r)=\binom r2+ar+b\pmod2\qquad(0\le r\le n), or, equivalently, f^\#(r+2)=f^\#(r)+1\qquad(0\le r\le n-2).

Lean code for Theorem9.1.5●24 declarations
  • defdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    def CryptBoolean.symmetricAffineNormalForm (n : ℕ) (a b : FABL.𝔽₂) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.symmetricAffineNormalForm
  (n : ℕ) (a b : FABL.𝔽₂) :
  CryptBoolean.BooleanFunction n
    The symmetric affine normal form `a p_n + b`.
  • defdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    def CryptBoolean.symmetricQuadraticNormalForm (n : ℕ) (a b : FABL.𝔽₂) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.symmetricQuadraticNormalForm
  (n : ℕ) (a b : FABL.𝔽₂) :
  CryptBoolean.BooleanFunction n
    The symmetric quadratic normal form `q_n + a p_n + b`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.isSymmetricBooleanFunction_symmetricAffineNormalForm
  {n : ℕ} (a b : FABL.𝔽₂) :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.symmetricAffineNormalForm n a b)
    theorem CryptBoolean.isSymmetricBooleanFunction_symmetricAffineNormalForm
  {n : ℕ} (a b : FABL.𝔽₂) :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.symmetricAffineNormalForm
      n a b)
    Every symmetric affine normal form is symmetric.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.isSymmetricBooleanFunction_symmetricQuadraticNormalForm
  {n : ℕ} (a b : FABL.𝔽₂) :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.symmetricQuadraticNormalForm n a b)
    theorem CryptBoolean.isSymmetricBooleanFunction_symmetricQuadraticNormalForm
  {n : ℕ} (a b : FABL.𝔽₂) :
  CryptBoolean.IsSymmetricBooleanFunction
    (CryptBoolean.symmetricQuadraticNormalForm
      n a b)
    Every symmetric quadratic normal form is symmetric.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.symmetricWeightProfileNat_symmetricAffineNormalForm {n : ℕ}
  (a b : FABL.𝔽₂) {r : ℕ} (hr : r ≤ n) :
  CryptBoolean.symmetricWeightProfileNat
      (CryptBoolean.symmetricAffineNormalForm n a b) r =
    a * ↑r + b
    theorem CryptBoolean.symmetricWeightProfileNat_symmetricAffineNormalForm
  {n : ℕ} (a b : FABL.𝔽₂) {r : ℕ}
  (hr : r ≤ n) :
  CryptBoolean.symmetricWeightProfileNat
      (CryptBoolean.symmetricAffineNormalForm
        n a b)
      r =
    a * ↑r + b
    The weight profile of the symmetric affine normal form.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.symmetricWeightProfileNat_symmetricQuadraticNormalForm
  {n : ℕ} (a b : FABL.𝔽₂) {r : ℕ} (hr : r ≤ n) :
  CryptBoolean.symmetricWeightProfileNat
      (CryptBoolean.symmetricQuadraticNormalForm n a b) r =
    ↑(r.choose 2) + a * ↑r + b
    theorem CryptBoolean.symmetricWeightProfileNat_symmetricQuadraticNormalForm
  {n : ℕ} (a b : FABL.𝔽₂) {r : ℕ}
  (hr : r ≤ n) :
  CryptBoolean.symmetricWeightProfileNat
      (CryptBoolean.symmetricQuadraticNormalForm
        n a b)
      r =
    ↑(r.choose 2) + a * ↑r + b
    The weight profile of the symmetric quadratic normal form.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.elementarySymmetricBoolean_zero {n : ℕ} :
  CryptBoolean.elementarySymmetricBoolean n 0 = 1
    theorem CryptBoolean.elementarySymmetricBoolean_zero
  {n : ℕ} :
  CryptBoolean.elementarySymmetricBoolean
      n 0 =
    1
    The zeroth elementary symmetric Boolean function is constant one.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.elementarySymmetricBoolean_one_eq_coordinateSum {n : ℕ} :
  CryptBoolean.elementarySymmetricBoolean n 1 =
    ⇑(FABL.coordinateSum Finset.univ)
    theorem CryptBoolean.elementarySymmetricBoolean_one_eq_coordinateSum
  {n : ℕ} :
  CryptBoolean.elementarySymmetricBoolean
      n 1 =
    ⇑(FABL.coordinateSum Finset.univ)
    The first elementary symmetric Boolean function is full parity.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.elementarySymmetricBoolean_two_eq_completeQuadraticBit
  {n : ℕ} :
  CryptBoolean.elementarySymmetricBoolean n 2 =
    FABL.completeQuadraticBit
    theorem CryptBoolean.elementarySymmetricBoolean_two_eq_completeQuadraticBit
  {n : ℕ} :
  CryptBoolean.elementarySymmetricBoolean
      n 2 =
    FABL.completeQuadraticBit
    The second elementary symmetric Boolean function is the complete
quadratic function.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.anfCoeff_smul {n : ℕ} (a : FABL.𝔽₂)
  (f : CryptBoolean.BooleanFunction n) :
  FABL.anfCoeff (a • f) = fun S => a * FABL.anfCoeff f S
    theorem CryptBoolean.anfCoeff_smul {n : ℕ}
  (a : FABL.𝔽₂)
  (f : CryptBoolean.BooleanFunction n) :
  FABL.anfCoeff (a • f) = fun S =>
    a * FABL.anfCoeff f S
    Scalar multiplication commutes with the canonical ANF transform.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.anfCoeff_symmetricAffineNormalForm {n : ℕ}
  (a b : FABL.𝔽₂) :
  FABL.anfCoeff (CryptBoolean.symmetricAffineNormalForm n a b) =
    fun S =>
    a * CryptBoolean.elementarySymmetricANFCoefficients n 1 S +
      b * CryptBoolean.elementarySymmetricANFCoefficients n 0 S
    theorem CryptBoolean.anfCoeff_symmetricAffineNormalForm
  {n : ℕ} (a b : FABL.𝔽₂) :
  FABL.anfCoeff
      (CryptBoolean.symmetricAffineNormalForm
        n a b) =
    fun S =>
    a *
        CryptBoolean.elementarySymmetricANFCoefficients
          n 1 S +
      b *
        CryptBoolean.elementarySymmetricANFCoefficients
          n 0 S
    The canonical ANF coefficients of the symmetric affine normal form.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.anfCoeff_symmetricQuadraticNormalForm {n : ℕ}
  (a b : FABL.𝔽₂) :
  FABL.anfCoeff (CryptBoolean.symmetricQuadraticNormalForm n a b) =
    fun S =>
    CryptBoolean.elementarySymmetricANFCoefficients n 2 S +
      (a * CryptBoolean.elementarySymmetricANFCoefficients n 1 S +
        b * CryptBoolean.elementarySymmetricANFCoefficients n 0 S)
    theorem CryptBoolean.anfCoeff_symmetricQuadraticNormalForm
  {n : ℕ} (a b : FABL.𝔽₂) :
  FABL.anfCoeff
      (CryptBoolean.symmetricQuadraticNormalForm
        n a b) =
    fun S =>
    CryptBoolean.elementarySymmetricANFCoefficients
        n 2 S +
      (a *
          CryptBoolean.elementarySymmetricANFCoefficients
            n 1 S +
        b *
          CryptBoolean.elementarySymmetricANFCoefficients
            n 0 S)
    The canonical ANF coefficients of the symmetric quadratic normal form.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.symmetricAffineNormalForm_eq_coordinateSum_add_constant
  {n : ℕ} (a b : FABL.𝔽₂) :
  CryptBoolean.symmetricAffineNormalForm n a b =
    a • ⇑(FABL.coordinateSum Finset.univ) + fun x => b
    theorem CryptBoolean.symmetricAffineNormalForm_eq_coordinateSum_add_constant
  {n : ℕ} (a b : FABL.𝔽₂) :
  CryptBoolean.symmetricAffineNormalForm n
      a b =
    a •
        ⇑(FABL.coordinateSum
            Finset.univ) +
      fun x => b
    The affine normal form is the source's full parity plus a constant.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.symmetricQuadraticNormalForm_eq_completeQuadratic_add_coordinateSum
  {n : ℕ} (a b : FABL.𝔽₂) :
  CryptBoolean.symmetricQuadraticNormalForm n a b =
    FABL.completeQuadraticBit + a • ⇑(FABL.coordinateSum Finset.univ) +
      fun x => b
    theorem CryptBoolean.symmetricQuadraticNormalForm_eq_completeQuadratic_add_coordinateSum
  {n : ℕ} (a b : FABL.𝔽₂) :
  CryptBoolean.symmetricQuadraticNormalForm
      n a b =
    FABL.completeQuadraticBit +
        a •
          ⇑(FABL.coordinateSum
              Finset.univ) +
      fun x => b
    The quadratic normal form is the source's complete quadratic, full parity,
and constant combination.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.exists_symmetricAffineNormalForm_of_degree_le_one {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hdegree : FABL.functionAlgebraicDegree f ≤ 1) :
  ∃ a b, f = CryptBoolean.symmetricAffineNormalForm n a b
    theorem CryptBoolean.exists_symmetricAffineNormalForm_of_degree_le_one
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 1) :
  ∃ a b,
    f =
      CryptBoolean.symmetricAffineNormalForm
        n a b
    Every symmetric Boolean function of algebraic degree at most one has a
symmetric affine normal form.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_eq_one_iff_exists_symmetricAffineNormalForm
  {n : ℕ} (hn : 0 < n) {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  FABL.functionAlgebraicDegree f = 1 ↔
    ∃ b, f = CryptBoolean.symmetricAffineNormalForm n 1 b
    theorem CryptBoolean.functionAlgebraicDegree_eq_one_iff_exists_symmetricAffineNormalForm
  {n : ℕ} (hn : 0 < n)
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  FABL.functionAlgebraicDegree f = 1 ↔
    ∃ b,
      f =
        CryptBoolean.symmetricAffineNormalForm
          n 1 b
    Every positive-dimensional symmetric Boolean function of algebraic degree
exactly one is full parity plus a constant.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.exists_symmetricQuadraticLayerNormalForm_of_degree_le_two
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hdegree : FABL.functionAlgebraicDegree f ≤ 2) :
  ∃ c a b,
    f =
      c • CryptBoolean.elementarySymmetricBoolean n 2 +
        CryptBoolean.symmetricAffineNormalForm n a b
    theorem CryptBoolean.exists_symmetricQuadraticLayerNormalForm_of_degree_le_two
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  ∃ c a b,
    f =
      c •
          CryptBoolean.elementarySymmetricBoolean
            n 2 +
        CryptBoolean.symmetricAffineNormalForm
          n a b
    Every symmetric Boolean function of algebraic degree at most two has a
quadratic-layer coefficient followed by a symmetric affine normal form.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_eq_two_iff_exists_symmetricQuadraticNormalForm
  {n : ℕ} (hn : 2 ≤ n) {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  FABL.functionAlgebraicDegree f = 2 ↔
    ∃ a b, f = CryptBoolean.symmetricQuadraticNormalForm n a b
    theorem CryptBoolean.functionAlgebraicDegree_eq_two_iff_exists_symmetricQuadraticNormalForm
  {n : ℕ} (hn : 2 ≤ n)
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  FABL.functionAlgebraicDegree f = 2 ↔
    ∃ a b,
      f =
        CryptBoolean.symmetricQuadraticNormalForm
          n a b
    Every symmetric Boolean function of algebraic degree exactly two is the
complete quadratic function plus full parity and a constant.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.symmetricWeightProfileNat_symmetricAffineNormalForm_succ
  {n : ℕ} (b : FABL.𝔽₂) {r : ℕ} (hr : r < n) :
  CryptBoolean.symmetricWeightProfileNat
      (CryptBoolean.symmetricAffineNormalForm n 1 b) (r + 1) =
    CryptBoolean.symmetricWeightProfileNat
        (CryptBoolean.symmetricAffineNormalForm n 1 b) r +
      1
    theorem CryptBoolean.symmetricWeightProfileNat_symmetricAffineNormalForm_succ
  {n : ℕ} (b : FABL.𝔽₂) {r : ℕ}
  (hr : r < n) :
  CryptBoolean.symmetricWeightProfileNat
      (CryptBoolean.symmetricAffineNormalForm
        n 1 b)
      (r + 1) =
    CryptBoolean.symmetricWeightProfileNat
        (CryptBoolean.symmetricAffineNormalForm
          n 1 b)
        r +
      1
    The affine symmetric profile toggles at every successive weight.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.symmetricWeightProfileNat_symmetricQuadraticNormalForm_add_two
  {n : ℕ} (a b : FABL.𝔽₂) {r : ℕ} (hr : r + 2 ≤ n) :
  CryptBoolean.symmetricWeightProfileNat
      (CryptBoolean.symmetricQuadraticNormalForm n a b) (r + 2) =
    CryptBoolean.symmetricWeightProfileNat
        (CryptBoolean.symmetricQuadraticNormalForm n a b) r +
      1
    theorem CryptBoolean.symmetricWeightProfileNat_symmetricQuadraticNormalForm_add_two
  {n : ℕ} (a b : FABL.𝔽₂) {r : ℕ}
  (hr : r + 2 ≤ n) :
  CryptBoolean.symmetricWeightProfileNat
      (CryptBoolean.symmetricQuadraticNormalForm
        n a b)
      (r + 2) =
    CryptBoolean.symmetricWeightProfileNat
        (CryptBoolean.symmetricQuadraticNormalForm
          n a b)
        r +
      1
    The quadratic symmetric profile toggles after every two weight layers.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.exists_symmetricAffineNormalForm_of_profile_succ {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hprofile :
    ∀ r < n,
      CryptBoolean.symmetricWeightProfileNat f (r + 1) =
        CryptBoolean.symmetricWeightProfileNat f r + 1) :
  ∃ b, f = CryptBoolean.symmetricAffineNormalForm n 1 b
    theorem CryptBoolean.exists_symmetricAffineNormalForm_of_profile_succ
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hprofile :
    ∀ r < n,
      CryptBoolean.symmetricWeightProfileNat
          f (r + 1) =
        CryptBoolean.symmetricWeightProfileNat
            f r +
          1) :
  ∃ b,
    f =
      CryptBoolean.symmetricAffineNormalForm
        n 1 b
    A symmetric profile that toggles at each step is full parity plus its
weight-zero value.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.exists_symmetricQuadraticNormalForm_of_profile_add_two
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hprofile :
    ∀ (r : ℕ),
      r + 2 ≤ n →
        CryptBoolean.symmetricWeightProfileNat f (r + 2) =
          CryptBoolean.symmetricWeightProfileNat f r + 1) :
  ∃ a b, f = CryptBoolean.symmetricQuadraticNormalForm n a b
    theorem CryptBoolean.exists_symmetricQuadraticNormalForm_of_profile_add_two
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hprofile :
    ∀ (r : ℕ),
      r + 2 ≤ n →
        CryptBoolean.symmetricWeightProfileNat
            f (r + 2) =
          CryptBoolean.symmetricWeightProfileNat
              f r +
            1) :
  ∃ a b,
    f =
      CryptBoolean.symmetricQuadraticNormalForm
        n a b
    A symmetric profile that toggles after two layers is the complete
quadratic function plus parity and a constant.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_eq_one_iff_profile_succ {n : ℕ}
  (hn : 0 < n) {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  FABL.functionAlgebraicDegree f = 1 ↔
    ∀ r < n,
      CryptBoolean.symmetricWeightProfileNat f (r + 1) =
        CryptBoolean.symmetricWeightProfileNat f r + 1
    theorem CryptBoolean.functionAlgebraicDegree_eq_one_iff_profile_succ
  {n : ℕ} (hn : 0 < n)
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  FABL.functionAlgebraicDegree f = 1 ↔
    ∀ r < n,
      CryptBoolean.symmetricWeightProfileNat
          f (r + 1) =
        CryptBoolean.symmetricWeightProfileNat
            f r +
          1
    The degree-one classification in its equivalent profile-recurrence form.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/LowDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_eq_two_iff_profile_add_two {n : ℕ}
  (hn : 2 ≤ n) {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) :
  FABL.functionAlgebraicDegree f = 2 ↔
    ∀ (r : ℕ),
      r + 2 ≤ n →
        CryptBoolean.symmetricWeightProfileNat f (r + 2) =
          CryptBoolean.symmetricWeightProfileNat f r + 1
    theorem CryptBoolean.functionAlgebraicDegree_eq_two_iff_profile_add_two
  {n : ℕ} (hn : 2 ≤ n)
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  FABL.functionAlgebraicDegree f = 2 ↔
    ∀ (r : ℕ),
      r + 2 ≤ n →
        CryptBoolean.symmetricWeightProfileNat
            f (r + 2) =
          CryptBoolean.symmetricWeightProfileNat
              f r +
            1
    The degree-two classification in its equivalent two-step profile
recurrence form.
Theorem9.1.6
Group: Chapter 9: Symmetric and rotation-symmetric functions (22)
Group member previews
Preview
Definition 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-10symmetric-functionsalgebraic-degreeperiodicityreference-48page-142fidelity-finite-profile-correction

Degree and weight-profile periodicity (Carlet, p. 142). Let f:V_n\to\mathbb F_2 be symmetric with weight profile f^\#, and let t>0. Then \deg_{\mathrm{alg}}(f)\le2^t-1 if and only if f^\#(r+2^t)=f^\#(r) for every r such that r+2^t\le n. Equivalently, the finite word f^\#(0),f^\#(1),\ldots,f^\#(n) is the restriction of a sequence having period 2^t.

Lean code for Theorem9.1.6●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Periodicity.lean
    complete
    theorem CryptBoolean.symmetricANFCoefficient_add_two_pow (profile : ℕ → FABL.𝔽₂)
  (t r : ℕ) :
  CryptBoolean.symmetricANFCoefficient profile (r + 2 ^ t) =
    CryptBoolean.symmetricANFCoefficient profile r +
      CryptBoolean.symmetricANFCoefficient
        (fun i => profile (i + 2 ^ t)) r
    theorem CryptBoolean.symmetricANFCoefficient_add_two_pow
  (profile : ℕ → FABL.𝔽₂) (t r : ℕ) :
  CryptBoolean.symmetricANFCoefficient
      profile (r + 2 ^ t) =
    CryptBoolean.symmetricANFCoefficient
        profile r +
      CryptBoolean.symmetricANFCoefficient
        (fun i => profile (i + 2 ^ t)) r
    Translation by `2^t` splits the characteristic-two binomial transform
into its original and shifted transforms.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/Periodicity.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_le_two_pow_sub_one_iff_profile_periodic
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) {t : ℕ}
  (_ht : 0 < t) :
  FABL.functionAlgebraicDegree f ≤ 2 ^ t - 1 ↔
    ∀ (r : ℕ),
      r + 2 ^ t ≤ n →
        CryptBoolean.symmetricWeightProfileNat f (r + 2 ^ t) =
          CryptBoolean.symmetricWeightProfileNat f r
    theorem CryptBoolean.functionAlgebraicDegree_le_two_pow_sub_one_iff_profile_periodic
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  {t : ℕ} (_ht : 0 < t) :
  FABL.functionAlgebraicDegree f ≤
      2 ^ t - 1 ↔
    ∀ (r : ℕ),
      r + 2 ^ t ≤ n →
        CryptBoolean.symmetricWeightProfileNat
            f (r + 2 ^ t) =
          CryptBoolean.symmetricWeightProfileNat
            f r
    A symmetric Boolean function has algebraic degree below `2^t` exactly
when its finite weight profile has period `2^t` wherever both entries are
within the cube.