Cryptographic Boolean Functions in Lean

9.4. Resiliency🔗

Theorem9.4.1
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 1used by 0✓L∃∀N
Tagscarletchapter-10symmetric-functionsnumerical-degreepage-145fidelity-exact-integer-form

Numerical-degree lower bound (Carlet, p. 145). Let n>0 and let f:V_n\to\mathbb F_2 be a nonconstant symmetric Boolean function. Then its numerical degree satisfies 2\deg_{\mathrm{NNF}}(f)\ge n. Equivalently, \deg_{\mathrm{NNF}}(f)\ge\left\lceil\frac n2\right\rceil.

Lean code for Theorem9.4.1●3 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.eq_zero_or_eq_one_of_two_mul_functionNumericalDegree_lt_succ
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hdegree :
    2 * FABL.functionNumericalDegree (FABL.booleanRealEmbedding f) <
      n + 1) :
  f = 0 ∨ f = 1
    theorem CryptBoolean.eq_zero_or_eq_one_of_two_mul_functionNumericalDegree_lt_succ
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hdegree :
    2 *
        FABL.functionNumericalDegree
          (FABL.booleanRealEmbedding f) <
      n + 1) :
  f = 0 ∨ f = 1
    If twice the numerical degree is smaller than the number of weight
layers, a symmetric Boolean function is constant.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.ceiling_half_dimension_le_functionNumericalDegree_of_symmetric
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hnonconstant : f ≠ 0 ∧ f ≠ 1) :
  (n + 1) / 2 ≤
    FABL.functionNumericalDegree (FABL.booleanRealEmbedding f)
    theorem CryptBoolean.ceiling_half_dimension_le_functionNumericalDegree_of_symmetric
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hnonconstant : f ≠ 0 ∧ f ≠ 1) :
  (n + 1) / 2 ≤
    FABL.functionNumericalDegree
      (FABL.booleanRealEmbedding f)
    Every nonconstant symmetric Boolean function has numerical degree at least
the ceiling of half the number of variables.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.half_dimension_le_functionNumericalDegree_of_symmetric
  {n : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hnonconstant : f ≠ 0 ∧ f ≠ 1) :
  n / 2 ≤ FABL.functionNumericalDegree (FABL.booleanRealEmbedding f)
    theorem CryptBoolean.half_dimension_le_functionNumericalDegree_of_symmetric
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hnonconstant : f ≠ 0 ∧ f ≠ 1) :
  n / 2 ≤
    FABL.functionNumericalDegree
      (FABL.booleanRealEmbedding f)
    The printed half-dimension form of the numerical-degree lower bound.
Theorem9.4.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.
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 9.4.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-10relation-73symmetric-functionsnumerical-degreeweight-profilepage-145fidelity-exact

Relation (73) (Carlet, p. 145). Let f:V_n\to\mathbb F_2 be symmetric with weight profile f^\#, and let d be a nonnegative integer. Then \deg_{\mathrm{NNF}}(f)\le d if and only if, for every integer k with d<k\le n, \sum_{r=0}^{k}(-1)^r\binom kr f^\#(r)=0 as an equality of integers.

Lean code for Theorem9.4.2●7 declarations
  • defdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    def CryptBoolean.symmetricNumericalCoefficientInt (profile : ℕ → FABL.𝔽₂)
  (k : ℕ) : ℤ
    def CryptBoolean.symmetricNumericalCoefficientInt
  (profile : ℕ → FABL.𝔽₂) (k : ℕ) : ℤ
    The integral finite-difference coefficient of a binary weight profile.
  • defdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    def CryptBoolean.relation73AlternatingSumInt (profile : ℕ → FABL.𝔽₂)
  (k : ℕ) : ℤ
    def CryptBoolean.relation73AlternatingSumInt
  (profile : ℕ → FABL.𝔽₂) (k : ℕ) : ℤ
    The literal integer alternating sum in Relation (73).
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.symmetricNumericalCoefficientInt_eq_sign_mul_relation73AlternatingSumInt
  (profile : ℕ → FABL.𝔽₂) (k : ℕ) :
  CryptBoolean.symmetricNumericalCoefficientInt profile k =
    (-1) ^ k * CryptBoolean.relation73AlternatingSumInt profile k
    theorem CryptBoolean.symmetricNumericalCoefficientInt_eq_sign_mul_relation73AlternatingSumInt
  (profile : ℕ → FABL.𝔽₂) (k : ℕ) :
  CryptBoolean.symmetricNumericalCoefficientInt
      profile k =
    (-1) ^ k *
      CryptBoolean.relation73AlternatingSumInt
        profile k
    Relation (71)'s integral coefficient differs from Relation (73)'s
literal alternating sum by the invertible sign `(-1)^k`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.symmetricNumericalCoefficientInt_eq_zero_iff_relation73AlternatingSumInt_eq_zero
  (profile : ℕ → FABL.𝔽₂) (k : ℕ) :
  CryptBoolean.symmetricNumericalCoefficientInt profile k = 0 ↔
    CryptBoolean.relation73AlternatingSumInt profile k = 0
    theorem CryptBoolean.symmetricNumericalCoefficientInt_eq_zero_iff_relation73AlternatingSumInt_eq_zero
  (profile : ℕ → FABL.𝔽₂) (k : ℕ) :
  CryptBoolean.symmetricNumericalCoefficientInt
        profile k =
      0 ↔
    CryptBoolean.relation73AlternatingSumInt
        profile k =
      0
    The integral coefficient from Relation (71) vanishes exactly when the
literal integer alternating sum from Relation (73) vanishes.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.symmetricNumericalCoefficient_eq_intCast {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (k : ℕ) :
  CryptBoolean.symmetricNumericalCoefficient
      (CryptBoolean.symmetricRealWeightProfile f) k =
    ↑(CryptBoolean.symmetricNumericalCoefficientInt
        (CryptBoolean.symmetricWeightProfileNat f) k)
    theorem CryptBoolean.symmetricNumericalCoefficient_eq_intCast
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (k : ℕ) :
  CryptBoolean.symmetricNumericalCoefficient
      (CryptBoolean.symmetricRealWeightProfile
        f)
      k =
    ↑(CryptBoolean.symmetricNumericalCoefficientInt
        (CryptBoolean.symmetricWeightProfileNat
          f)
        k)
    The real coefficient transform is the cast of its integral binary
finite-difference form.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.relation_73_functionNumericalDegree_le_iff {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (d : ℕ) :
  FABL.functionNumericalDegree (FABL.booleanRealEmbedding f) ≤ d ↔
    ∀ k ≤ n,
      d < k →
        CryptBoolean.symmetricNumericalCoefficient
            (CryptBoolean.symmetricRealWeightProfile f) k =
          0
    theorem CryptBoolean.relation_73_functionNumericalDegree_le_iff
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (d : ℕ) :
  FABL.functionNumericalDegree
        (FABL.booleanRealEmbedding f) ≤
      d ↔
    ∀ k ≤ n,
      d < k →
        CryptBoolean.symmetricNumericalCoefficient
            (CryptBoolean.symmetricRealWeightProfile
              f)
            k =
          0
    The numerical degree bound is equivalent to vanishing of all higher real
binomial finite-difference coefficients of the weight profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/NumericalDegree.lean
    complete
    theorem CryptBoolean.relation_73_functionNumericalDegree_le_iff_int {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (d : ℕ) :
  FABL.functionNumericalDegree (FABL.booleanRealEmbedding f) ≤ d ↔
    ∀ k ≤ n,
      d < k →
        CryptBoolean.relation73AlternatingSumInt
            (CryptBoolean.symmetricWeightProfileNat f) k =
          0
    theorem CryptBoolean.relation_73_functionNumericalDegree_le_iff_int
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (d : ℕ) :
  FABL.functionNumericalDegree
        (FABL.booleanRealEmbedding f) ≤
      d ↔
    ∀ k ≤ n,
      d < k →
        CryptBoolean.relation73AlternatingSumInt
            (CryptBoolean.symmetricWeightProfileNat
              f)
            k =
          0
    Relation (73): the numerical degree bound is equivalent to the literal
integer alternating-binomial equations of the source.
Theorem9.4.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.
Statement uses 3
Statement dependency previews
Preview
Proposition 6.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-10symmetric-functionsnumerical-degreeresiliencyprimereference-159page-146fidelity-exact

Prime-successor numerical degree (Carlet, p. 146). Let n>0 and suppose that n+1 is prime. Every nonconstant symmetric Boolean function f:V_n\to\mathbb F_2 has numerical degree exactly n.

Consequently, every non-affine symmetric Boolean function on V_n is unbalanced, equivalently it is not 0-resilient.

Lean code for Theorem9.4.3●10 declarations
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.natCast_choose_prime_sub_one {p : ℕ} (hp : Nat.Prime p)
  {r : ℕ} (hr : r < p) : ↑((p - 1).choose r) = (-1) ^ r
    theorem CryptBoolean.natCast_choose_prime_sub_one
  {p : ℕ} (hp : Nat.Prime p) {r : ℕ}
  (hr : r < p) :
  ↑((p - 1).choose r) = (-1) ^ r
    For prime `p`, the binomial row `p-1` alternates modulo `p`.
  • defdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    def CryptBoolean.weightProfileOneCount (profile : ℕ → FABL.𝔽₂) (p : ℕ) : ℕ
    def CryptBoolean.weightProfileOneCount
  (profile : ℕ → FABL.𝔽₂) (p : ℕ) : ℕ
    The number of ones in an initial segment of a binary weight profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.sum_profile_val_eq_weightProfileOneCount
  (profile : ℕ → FABL.𝔽₂) (p : ℕ) :
  ∑ r ∈ Finset.range p, ZMod.val (profile r) =
    CryptBoolean.weightProfileOneCount profile p
    theorem CryptBoolean.sum_profile_val_eq_weightProfileOneCount
  (profile : ℕ → FABL.𝔽₂) (p : ℕ) :
  ∑ r ∈ Finset.range p,
      ZMod.val (profile r) =
    CryptBoolean.weightProfileOneCount
      profile p
    Summing the canonical representatives of profile bits counts its ones.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.intCast_symmetricNumericalCoefficientInt_prime_sub_one
  {p : ℕ} (hp : Nat.Prime p) (profile : ℕ → FABL.𝔽₂) :
  ↑(CryptBoolean.symmetricNumericalCoefficientInt profile (p - 1)) =
    (-1) ^ (p - 1) * ↑(CryptBoolean.weightProfileOneCount profile p)
    theorem CryptBoolean.intCast_symmetricNumericalCoefficientInt_prime_sub_one
  {p : ℕ} (hp : Nat.Prime p)
  (profile : ℕ → FABL.𝔽₂) :
  ↑(CryptBoolean.symmetricNumericalCoefficientInt
        profile (p - 1)) =
    (-1) ^ (p - 1) *
      ↑(CryptBoolean.weightProfileOneCount
          profile p)
    Modulo a prime `p`, the top finite difference is a unit times the
number of ones in the length-`p` profile.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.weightProfile_constant_on_prime_range_of_coefficient_zero
  {p : ℕ} (hp : Nat.Prime p) (profile : ℕ → FABL.𝔽₂)
  (hcoefficient :
    CryptBoolean.symmetricNumericalCoefficientInt profile (p - 1) = 0) :
  (∀ r < p, profile r = 0) ∨ ∀ r < p, profile r = 1
    theorem CryptBoolean.weightProfile_constant_on_prime_range_of_coefficient_zero
  {p : ℕ} (hp : Nat.Prime p)
  (profile : ℕ → FABL.𝔽₂)
  (hcoefficient :
    CryptBoolean.symmetricNumericalCoefficientInt
        profile (p - 1) =
      0) :
  (∀ r < p, profile r = 0) ∨
    ∀ r < p, profile r = 1
    If a prime-length initial binary profile has vanishing top finite
difference, then that initial profile is constant.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.eq_zero_or_eq_one_of_functionNumericalDegree_lt_prime_sub_one
  {n p : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f) (hp : Nat.Prime p)
  (hpn : p ≤ n + 1)
  (hdegree :
    FABL.functionNumericalDegree (FABL.booleanRealEmbedding f) <
      p - 1) :
  f = 0 ∨ f = 1
    theorem CryptBoolean.eq_zero_or_eq_one_of_functionNumericalDegree_lt_prime_sub_one
  {n p : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hp : Nat.Prime p) (hpn : p ≤ n + 1)
  (hdegree :
    FABL.functionNumericalDegree
        (FABL.booleanRealEmbedding f) <
      p - 1) :
  f = 0 ∨ f = 1
    A symmetric Boolean function whose numerical degree is smaller than
`p - 1`, for a prime `p ≤ n + 1`, is constant.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.functionNumericalDegree_eq_dimension_of_symmetric_of_succ_prime
  {n : ℕ} {f : CryptBoolean.BooleanFunction n} (_hn : 0 < n)
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hnonconstant : f ≠ 0 ∧ f ≠ 1) (hp : Nat.Prime (n + 1)) :
  FABL.functionNumericalDegree (FABL.booleanRealEmbedding f) = n
    theorem CryptBoolean.functionNumericalDegree_eq_dimension_of_symmetric_of_succ_prime
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (_hn : 0 < n)
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hnonconstant : f ≠ 0 ∧ f ≠ 1)
  (hp : Nat.Prime (n + 1)) :
  FABL.functionNumericalDegree
      (FABL.booleanRealEmbedding f) =
    n
    If `n + 1` is prime, every nonconstant symmetric Boolean function on
`n` variables has numerical degree exactly `n`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.isResilient_zero_iff_isBalanced {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) :
  CryptBoolean.IsResilient 0 f ↔ CryptBoolean.IsBalanced f
    theorem CryptBoolean.isResilient_zero_iff_isBalanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) :
  CryptBoolean.IsResilient 0 f ↔
    CryptBoolean.IsBalanced f
    In positive dimension, zero-resiliency is equivalent to balancedness.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.not_isResilient_zero_of_symmetric_of_succ_prime {n : ℕ}
  {f : CryptBoolean.BooleanFunction n} (hn : 0 < n)
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hnonaffine : ¬CryptBoolean.IsAffineBooleanFunction f)
  (hp : Nat.Prime (n + 1)) : ¬CryptBoolean.IsResilient 0 f
    theorem CryptBoolean.not_isResilient_zero_of_symmetric_of_succ_prime
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hn : 0 < n)
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hnonaffine :
    ¬CryptBoolean.IsAffineBooleanFunction
        f)
  (hp : Nat.Prime (n + 1)) :
  ¬CryptBoolean.IsResilient 0 f
    If `n + 1` is prime, no non-affine symmetric Boolean function on `n`
variables is zero-resilient.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.not_isBalanced_of_symmetric_of_succ_prime {n : ℕ}
  {f : CryptBoolean.BooleanFunction n} (hn : 0 < n)
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hnonaffine : ¬CryptBoolean.IsAffineBooleanFunction f)
  (hp : Nat.Prime (n + 1)) : ¬CryptBoolean.IsBalanced f
    theorem CryptBoolean.not_isBalanced_of_symmetric_of_succ_prime
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hn : 0 < n)
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hnonaffine :
    ¬CryptBoolean.IsAffineBooleanFunction
        f)
  (hp : Nat.Prime (n + 1)) :
  ¬CryptBoolean.IsBalanced f
    If `n + 1` is prime, every non-affine symmetric Boolean function on
`n` variables is unbalanced.
Theorem9.4.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 3
Statement dependency previews
Preview
Proposition 6.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-10symmetric-functionsnumerical-degreeresiliencyprimepage-146fidelity-exact

Largest-prime numerical-degree bound (Carlet, p. 146). Let n>0 and let p be the largest prime with p\le n+1. Every nonconstant symmetric Boolean function f:V_n\to\mathbb F_2 satisfies \deg_{\mathrm{NNF}}(f)\ge p-1. Equivalently, no non-affine symmetric Boolean function on V_n is (n-p+1)-resilient.

Lean code for Theorem9.4.4●3 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.prime_sub_one_le_functionNumericalDegree_of_symmetric
  {n p : ℕ} {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hnonconstant : f ≠ 0 ∧ f ≠ 1) (hp : Nat.Prime p) (hpn : p ≤ n + 1) :
  p - 1 ≤ FABL.functionNumericalDegree (FABL.booleanRealEmbedding f)
    theorem CryptBoolean.prime_sub_one_le_functionNumericalDegree_of_symmetric
  {n p : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hnonconstant : f ≠ 0 ∧ f ≠ 1)
  (hp : Nat.Prime p) (hpn : p ≤ n + 1) :
  p - 1 ≤
    FABL.functionNumericalDegree
      (FABL.booleanRealEmbedding f)
    Every nonconstant symmetric Boolean function has numerical degree at
least `p - 1` for every prime `p ≤ n + 1`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.largestPrime_sub_one_le_functionNumericalDegree_of_symmetric
  {n p : ℕ} {f : CryptBoolean.BooleanFunction n} (_hn : 0 < n)
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hnonconstant : f ≠ 0 ∧ f ≠ 1) (hp : Nat.Prime p) (hpn : p ≤ n + 1)
  (_hlargest : ∀ (q : ℕ), Nat.Prime q → q ≤ n + 1 → q ≤ p) :
  p - 1 ≤ FABL.functionNumericalDegree (FABL.booleanRealEmbedding f)
    theorem CryptBoolean.largestPrime_sub_one_le_functionNumericalDegree_of_symmetric
  {n p : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (_hn : 0 < n)
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hnonconstant : f ≠ 0 ∧ f ≠ 1)
  (hp : Nat.Prime p) (hpn : p ≤ n + 1)
  (_hlargest :
    ∀ (q : ℕ),
      Nat.Prime q → q ≤ n + 1 → q ≤ p) :
  p - 1 ≤
    FABL.functionNumericalDegree
      (FABL.booleanRealEmbedding f)
    If `p` is the largest prime not exceeding `n + 1`, every nonconstant
symmetric Boolean function has numerical degree at least `p - 1`.
  • theoremdefined in CryptBoolean/Carlet/Chapter10/PrimeDegree.lean
    complete
    theorem CryptBoolean.not_isResilient_largestPrime_sub_one_of_symmetric {n p : ℕ}
  {f : CryptBoolean.BooleanFunction n} (hn : 0 < n)
  (hf : CryptBoolean.IsSymmetricBooleanFunction f)
  (hnonaffine : ¬CryptBoolean.IsAffineBooleanFunction f)
  (hp : Nat.Prime p) (hpn : p ≤ n + 1)
  (hlargest : ∀ (q : ℕ), Nat.Prime q → q ≤ n + 1 → q ≤ p) :
  ¬CryptBoolean.IsResilient (n + 1 - p) f
    theorem CryptBoolean.not_isResilient_largestPrime_sub_one_of_symmetric
  {n p : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hn : 0 < n)
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hnonaffine :
    ¬CryptBoolean.IsAffineBooleanFunction
        f)
  (hp : Nat.Prime p) (hpn : p ≤ n + 1)
  (hlargest :
    ∀ (q : ℕ),
      Nat.Prime q → q ≤ n + 1 → q ≤ p) :
  ¬CryptBoolean.IsResilient (n + 1 - p) f
    Let `p` be the largest prime not exceeding `n + 1`. No non-affine
symmetric Boolean function on `n` variables is `(n + 1 - p)`-resilient.