Cryptographic Boolean Functions in Lean

2.1.Ā Reed--Muller codesšŸ”—

Theorem2.1.1
Group: Chapter 2: Boolean functions and coding (6)
Group member previews
Preview
Definition 2.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.4.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Theorem 2.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
āœ“Lāˆƒāˆ€N
Tagscarletchapter-3affine-weightpage-38fidelity-exact

Weight of a nonconstant affine function (Carlet, p. 38). For a\in V_n, b\in\mathbb F_2, and x\in V_n, (A_{a,b})_\chi(x)=(-1)^b(-1)^{a\mathbin\cdot x}. If a\ne0, then A_{a,b} is balanced and w_H(A_{a,b})=2^{n-1}.

Lean code for Theorem2.1.1ā—3 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Affine.lean
    complete
    theorem CryptBoolean.realSignView_affineFunction {n : ā„•} (b : FABL.š”½ā‚‚)
  (a x : FABL.Fā‚‚Cube n) :
  CryptBoolean.realSignView (FABL.affineFunction b a) x =
    FABL.binarySign b * (FABL.vectorWalshCharacter a) x
    theorem CryptBoolean.realSignView_affineFunction
  {n : ā„•} (b : FABL.š”½ā‚‚)
  (a x : FABL.Fā‚‚Cube n) :
  CryptBoolean.realSignView
      (FABL.affineFunction b a) x =
    FABL.binarySign b *
      (FABL.vectorWalshCharacter a) x
    The real sign view of an affine function is a constant sign times a Walsh character.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Affine.lean
    complete
    theorem CryptBoolean.isBalanced_affineFunction_of_ne_zero {n : ā„•} (b : FABL.š”½ā‚‚)
  (a : FABL.Fā‚‚Cube n) (ha : a ā‰  0) :
  CryptBoolean.IsBalanced (FABL.affineFunction b a)
    theorem CryptBoolean.isBalanced_affineFunction_of_ne_zero
  {n : ā„•} (b : FABL.š”½ā‚‚)
  (a : FABL.Fā‚‚Cube n) (ha : a ā‰  0) :
  CryptBoolean.IsBalanced
    (FABL.affineFunction b a)
    A nonconstant affine Boolean function is balanced.
  • theoremdefined in CryptBoolean/Carlet/Chapter02/Affine.lean
    complete
    theorem CryptBoolean.hammingWeight_affineFunction_of_ne_zero {n : ā„•}
  (b : FABL.š”½ā‚‚) (a : FABL.Fā‚‚Cube n) (ha : a ā‰  0) :
  CryptBoolean.hammingWeight (FABL.affineFunction b a) = 2 ^ (n - 1)
    theorem CryptBoolean.hammingWeight_affineFunction_of_ne_zero
  {n : ā„•} (b : FABL.š”½ā‚‚)
  (a : FABL.Fā‚‚Cube n) (ha : a ā‰  0) :
  CryptBoolean.hammingWeight
      (FABL.affineFunction b a) =
    2 ^ (n - 1)
    A nonconstant affine Boolean function has weight `2^(n-1)`.
Definition2.1.2
Group: Chapter 2: Boolean functions and coding (6)
Group member previews
Preview
Theorem 2.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 14
Reverse dependency previews
Preview
Theorem 2.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
āœ“Lāˆƒāˆ€N
Tagscarletchapter-3reed-muller-codepages-37-38fidelity-exact-with-derived-laws

Reed--Muller code (Carlet, pp. 37--38). The Reed--Muller code of order r in n variables is R(r,n) =\{f:V_n\to\mathbb F_2:\deg_{\mathrm{alg}}(f)\le r\}. It is an \mathbb F_2-linear subspace of the space of Boolean functions. If r\le s, then R(r,n)\subseteq R(s,n), and every affine function belongs to R(1,n). Moreover, if f,g\in R(r,n) and f\ne g, then d_H(f,g)>0.

Lean code for Definition2.1.2ā—5 declarations
  • defdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    def CryptBoolean.reedMuller (r n : ā„•) :
  Submodule FABL.š”½ā‚‚ (CryptBoolean.BooleanFunction n)
    def CryptBoolean.reedMuller (r n : ā„•) :
  Submodule FABL.š”½ā‚‚
    (CryptBoolean.BooleanFunction n)
    Carlet's Reed--Muller code `R(r,n)`, represented without a redundant
general coding-theory wrapper.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.mem_reedMuller_iff {n r : ā„•}
  (f : CryptBoolean.BooleanFunction n) :
  f āˆˆ CryptBoolean.reedMuller r n ā†” FABL.functionAlgebraicDegree f ā‰¤ r
    theorem CryptBoolean.mem_reedMuller_iff {n r : ā„•}
  (f : CryptBoolean.BooleanFunction n) :
  f āˆˆ CryptBoolean.reedMuller r n ā†”
    FABL.functionAlgebraicDegree f ā‰¤ r
    Membership in `R(r,n)` is exactly the algebraic-degree bound.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.reedMuller_mono {n r s : ā„•} (hrs : r ā‰¤ s) :
  CryptBoolean.reedMuller r n ā‰¤ CryptBoolean.reedMuller s n
    theorem CryptBoolean.reedMuller_mono {n r s : ā„•}
  (hrs : r ā‰¤ s) :
  CryptBoolean.reedMuller r n ā‰¤
    CryptBoolean.reedMuller s n
    Reed--Muller codes are nested in their order.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.affineFunction_mem_reedMuller_one {n : ā„•} (b : FABL.š”½ā‚‚)
  (a : FABL.Fā‚‚Cube n) :
  FABL.affineFunction b a āˆˆ CryptBoolean.reedMuller 1 n
    theorem CryptBoolean.affineFunction_mem_reedMuller_one
  {n : ā„•} (b : FABL.š”½ā‚‚)
  (a : FABL.Fā‚‚Cube n) :
  FABL.affineFunction b a āˆˆ
    CryptBoolean.reedMuller 1 n
    Every affine function belongs to the first-order Reed--Muller code.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.reedMuller_distance_pos {n r : ā„•}
  {f g : CryptBoolean.BooleanFunction n}
  (_hf : f āˆˆ CryptBoolean.reedMuller r n)
  (_hg : g āˆˆ CryptBoolean.reedMuller r n) (hfg : f ā‰  g) :
  0 < CryptBoolean.hammingDistance f g
    theorem CryptBoolean.reedMuller_distance_pos
  {n r : ā„•}
  {f g : CryptBoolean.BooleanFunction n}
  (_hf : f āˆˆ CryptBoolean.reedMuller r n)
  (_hg : g āˆˆ CryptBoolean.reedMuller r n)
  (hfg : f ā‰  g) :
  0 < CryptBoolean.hammingDistance f g
    Distinct Reed--Muller codewords always have positive raw Hamming distance.
Theorem2.1.3
Group: Chapter 2: Boolean functions and coding (6)
Group member previews
Preview
Theorem 2.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 5
Statement dependency previews
Preview
Lemma 1.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0āœ“Lāˆƒāˆ€N
Tagscarletchapter-3theorem-1order-onefidelity-derived-specialization

Derived order-one specialization of Carlet's Theorem 1. Let n\ge1. If f:V_n\to\mathbb F_2 is nonzero and \deg_{\mathrm{alg}}(f)\le1, then w_H(f)\ge2^{n-1}. Equivalently, for all distinct f,g\in R(1,n), d_H(f,g)\ge2^{n-1}.

Lean code for Theorem2.1.3ā—3 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.hammingWeight_affineFunction_one_zero {n : ā„•} :
  CryptBoolean.hammingWeight (FABL.affineFunction 1 0) = 2 ^ n
    theorem CryptBoolean.hammingWeight_affineFunction_one_zero
  {n : ā„•} :
  CryptBoolean.hammingWeight
      (FABL.affineFunction 1 0) =
    2 ^ n
    The weight of the constant-one Boolean function is the cube cardinality.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.two_pow_sub_one_le_hammingWeight_of_degree_le_one {n : ā„•}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree : FABL.functionAlgebraicDegree f ā‰¤ 1) (hf : f ā‰  0) :
  2 ^ (n - 1) ā‰¤ CryptBoolean.hammingWeight f
    theorem CryptBoolean.two_pow_sub_one_le_hammingWeight_of_degree_le_one
  {n : ā„•}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ā‰¤ 1)
  (hf : f ā‰  0) :
  2 ^ (n - 1) ā‰¤
    CryptBoolean.hammingWeight f
    A nonzero Boolean function of degree at most one has weight at least
`2^(n-1)`.  This is Carlet Theorem 1 for first-order Reed--Muller codes.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.reedMuller_one_distance_lower_bound {n : ā„•}
  {f g : CryptBoolean.BooleanFunction n}
  (hf : f āˆˆ CryptBoolean.reedMuller 1 n)
  (hg : g āˆˆ CryptBoolean.reedMuller 1 n) (hfg : f ā‰  g) :
  2 ^ (n - 1) ā‰¤ CryptBoolean.hammingDistance f g
    theorem CryptBoolean.reedMuller_one_distance_lower_bound
  {n : ā„•}
  {f g : CryptBoolean.BooleanFunction n}
  (hf : f āˆˆ CryptBoolean.reedMuller 1 n)
  (hg : g āˆˆ CryptBoolean.reedMuller 1 n)
  (hfg : f ā‰  g) :
  2 ^ (n - 1) ā‰¤
    CryptBoolean.hammingDistance f g
    Distinct first-order Reed--Muller codewords have distance at least
`2^(n-1)`.
Theorem2.1.4
Group: Chapter 2: Boolean functions and coding (6)
Group member previews
Preview
Theorem 2.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
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
Proposition 2.1.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
āœ“Lāˆƒāˆ€N
Tagscarletchapter-3theorem-1page-36fidelity-exact

Theorem 1 (Carlet, p. 36). Let 0\le r\le n. If f,g:V_n\to\mathbb F_2 are distinct and \deg_{\mathrm{alg}}(f)\le r, \qquad \deg_{\mathrm{alg}}(g)\le r, then d_H(f,g)\ge2^{n-r}. Equivalently, every nonzero Boolean function h of algebraic degree at most r satisfies w_H(h)\ge2^{n-r}.

Lean code for Theorem2.1.4ā—2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.two_pow_sub_le_hammingWeight_of_degree_le {n r : ā„•}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree : FABL.functionAlgebraicDegree f ā‰¤ r) (hf : f ā‰  0) :
  2 ^ (n - r) ā‰¤ CryptBoolean.hammingWeight f
    theorem CryptBoolean.two_pow_sub_le_hammingWeight_of_degree_le
  {n r : ā„•}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ā‰¤ r)
  (hf : f ā‰  0) :
  2 ^ (n - r) ā‰¤
    CryptBoolean.hammingWeight f
    Carlet Theorem 1: a nonzero Boolean function of algebraic degree at most `r`
has Hamming weight at least `2^(n-r)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.reedMuller_distance_lower_bound {n r : ā„•}
  {f g : CryptBoolean.BooleanFunction n}
  (hf : f āˆˆ CryptBoolean.reedMuller r n)
  (hg : g āˆˆ CryptBoolean.reedMuller r n) (hfg : f ā‰  g) :
  2 ^ (n - r) ā‰¤ CryptBoolean.hammingDistance f g
    theorem CryptBoolean.reedMuller_distance_lower_bound
  {n r : ā„•}
  {f g : CryptBoolean.BooleanFunction n}
  (hf : f āˆˆ CryptBoolean.reedMuller r n)
  (hg : g āˆˆ CryptBoolean.reedMuller r n)
  (hfg : f ā‰  g) :
  2 ^ (n - r) ā‰¤
    CryptBoolean.hammingDistance f g
    Carlet Theorem 1 in coding form: distinct words of `R(r,n)` have raw
Hamming distance at least `2^(n-r)`.
Proposition2.1.5
Group: Chapter 2: Boolean functions and coding (6)
Group member previews
Preview
Theorem 2.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 5
Reverse dependency previews
Preview
Theorem 3.2.19
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
āœ“Lāˆƒāˆ€N
Tagscarletchapter-3proposition-12pages-36-37fidelity-exact

Proposition 12 (Carlet, pp. 36--37). Let 0\le r\le n. A Boolean function f:V_n\to\mathbb F_2 satisfies \deg_{\mathrm{alg}}(f)=r \qquad\text{and}\qquad w_H(f)=2^{n-r} if and only if f is the indicator of an (n-r)-dimensional affine subspace of V_n.

Lean code for Proposition2.1.5ā—11 declarations
  • defdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    def CryptBoolean.affineFlatIndicator {n : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n)) (a : FABL.Fā‚‚Cube n) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.affineFlatIndicator {n : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n))
  (a : FABL.Fā‚‚Cube n) :
  CryptBoolean.BooleanFunction n
    The `š”½ā‚‚`-valued indicator of the affine flat `H + a`.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    theorem CryptBoolean.affineFlatIndicator_apply_eq_one_iff {n : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n)) (a x : FABL.Fā‚‚Cube n) :
  CryptBoolean.affineFlatIndicator H a x = 1 ā†”
    x āˆˆ FABL.binaryAffineSubspace H a
    theorem CryptBoolean.affineFlatIndicator_apply_eq_one_iff
  {n : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n))
  (a x : FABL.Fā‚‚Cube n) :
  CryptBoolean.affineFlatIndicator H a x =
      1 ā†”
    x āˆˆ FABL.binaryAffineSubspace H a
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    theorem CryptBoolean.mem_support_affineFlatIndicator {n : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n)) (a x : FABL.Fā‚‚Cube n) :
  x āˆˆ CryptBoolean.support (CryptBoolean.affineFlatIndicator H a) ā†”
    x āˆˆ FABL.binaryAffineSubspace H a
    theorem CryptBoolean.mem_support_affineFlatIndicator
  {n : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n))
  (a x : FABL.Fā‚‚Cube n) :
  x āˆˆ
      CryptBoolean.support
        (CryptBoolean.affineFlatIndicator
          H a) ā†”
    x āˆˆ FABL.binaryAffineSubspace H a
  • defdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    def CryptBoolean.IsBinaryAffineSet {n : ā„•} (S : Set (FABL.Fā‚‚Cube n)) : Prop
    def CryptBoolean.IsBinaryAffineSet {n : ā„•}
  (S : Set (FABL.Fā‚‚Cube n)) : Prop
    A nonempty set closed under ternary sums is an affine set over `š”½ā‚‚`.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    theorem CryptBoolean.hammingWeight_affineFlatIndicator {n : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n)) (a : FABL.Fā‚‚Cube n) :
  CryptBoolean.hammingWeight (CryptBoolean.affineFlatIndicator H a) =
    2 ^ Module.finrank FABL.š”½ā‚‚ ā†„H
    theorem CryptBoolean.hammingWeight_affineFlatIndicator
  {n : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n))
  (a : FABL.Fā‚‚Cube n) :
  CryptBoolean.hammingWeight
      (CryptBoolean.affineFlatIndicator H
        a) =
    2 ^ Module.finrank FABL.š”½ā‚‚ ā†„H
    The Hamming weight of an affine-flat indicator is the cardinality of its direction.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_affineFlatIndicator {n : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n)) (a : FABL.Fā‚‚Cube n) :
  FABL.functionAlgebraicDegree (CryptBoolean.affineFlatIndicator H a) =
    FABL.fā‚‚Codimension H
    theorem CryptBoolean.functionAlgebraicDegree_affineFlatIndicator
  {n : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n))
  (a : FABL.Fā‚‚Cube n) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.affineFlatIndicator H
        a) =
    FABL.fā‚‚Codimension H
    An affine flat of codimension `k` has indicator of algebraic degree exactly `k`.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    theorem CryptBoolean.degree_eq_and_hammingWeight_eq_affineFlatIndicator
  {n r : ā„•} (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n)) (a : FABL.Fā‚‚Cube n)
  (hrn : r ā‰¤ n) (hfinrank : Module.finrank FABL.š”½ā‚‚ ā†„H = n - r) :
  FABL.functionAlgebraicDegree (CryptBoolean.affineFlatIndicator H a) =
      r āˆ§
    CryptBoolean.hammingWeight (CryptBoolean.affineFlatIndicator H a) =
      2 ^ (n - r)
    theorem CryptBoolean.degree_eq_and_hammingWeight_eq_affineFlatIndicator
  {n r : ā„•}
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n))
  (a : FABL.Fā‚‚Cube n) (hrn : r ā‰¤ n)
  (hfinrank :
    Module.finrank FABL.š”½ā‚‚ ā†„H = n - r) :
  FABL.functionAlgebraicDegree
        (CryptBoolean.affineFlatIndicator
          H a) =
      r āˆ§
    CryptBoolean.hammingWeight
        (CryptBoolean.affineFlatIndicator
          H a) =
      2 ^ (n - r)
    Reverse direction of Carlet Proposition 12: every affine flat of dimension `n - r` has
degree `r` and minimum Reed--Muller weight.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    theorem CryptBoolean.eq_affineFlatIndicator_iff_support_eq {n : ā„•}
  (f : CryptBoolean.BooleanFunction n)
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n)) (a : FABL.Fā‚‚Cube n) :
  f = CryptBoolean.affineFlatIndicator H a ā†”
    ā†‘(CryptBoolean.support f) = ā†‘(FABL.binaryAffineSubspace H a)
    theorem CryptBoolean.eq_affineFlatIndicator_iff_support_eq
  {n : ā„•}
  (f : CryptBoolean.BooleanFunction n)
  (H : Submodule FABL.š”½ā‚‚ (FABL.Fā‚‚Cube n))
  (a : FABL.Fā‚‚Cube n) :
  f =
      CryptBoolean.affineFlatIndicator H
        a ā†”
    ā†‘(CryptBoolean.support f) =
      ā†‘(FABL.binaryAffineSubspace H a)
    A binary Boolean function is the affine-flat indicator exactly when its support is that flat.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    theorem CryptBoolean.exists_affineFlatIndicator_of_degree_eq_and_hammingWeight_eq
  {n r : ā„•} (f : CryptBoolean.BooleanFunction n) (hrn : r ā‰¤ n)
  (hdegree : FABL.functionAlgebraicDegree f = r)
  (hweight : CryptBoolean.hammingWeight f = 2 ^ (n - r)) :
  āˆƒ H a,
    Module.finrank FABL.š”½ā‚‚ ā†„H = n - r āˆ§
      f = CryptBoolean.affineFlatIndicator H a
    theorem CryptBoolean.exists_affineFlatIndicator_of_degree_eq_and_hammingWeight_eq
  {n r : ā„•}
  (f : CryptBoolean.BooleanFunction n)
  (hrn : r ā‰¤ n)
  (hdegree :
    FABL.functionAlgebraicDegree f = r)
  (hweight :
    CryptBoolean.hammingWeight f =
      2 ^ (n - r)) :
  āˆƒ H a,
    Module.finrank FABL.š”½ā‚‚ ā†„H = n - r āˆ§
      f =
        CryptBoolean.affineFlatIndicator H
          a
    Forward direction of Carlet Proposition 12: every minimum-weight word is an affine-flat
indicator of dimension `n - r`.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    theorem CryptBoolean.degree_eq_and_hammingWeight_eq_iff_exists_affineFlatIndicator
  {n r : ā„•} (f : CryptBoolean.BooleanFunction n) (hrn : r ā‰¤ n) :
  FABL.functionAlgebraicDegree f = r āˆ§
      CryptBoolean.hammingWeight f = 2 ^ (n - r) ā†”
    āˆƒ H a,
      Module.finrank FABL.š”½ā‚‚ ā†„H = n - r āˆ§
        f = CryptBoolean.affineFlatIndicator H a
    theorem CryptBoolean.degree_eq_and_hammingWeight_eq_iff_exists_affineFlatIndicator
  {n r : ā„•}
  (f : CryptBoolean.BooleanFunction n)
  (hrn : r ā‰¤ n) :
  FABL.functionAlgebraicDegree f = r āˆ§
      CryptBoolean.hammingWeight f =
        2 ^ (n - r) ā†”
    āˆƒ H a,
      Module.finrank FABL.š”½ā‚‚ ā†„H = n - r āˆ§
        f =
          CryptBoolean.affineFlatIndicator
            H a
    Carlet Proposition 12: for `0 ā‰¤ r ā‰¤ n`, the Boolean functions of degree `r` and
weight `2^(n-r)` are exactly the indicators of affine flats of dimension `n-r`.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerMinimumWeight.lean
    complete
    theorem CryptBoolean.degree_eq_and_hammingWeight_eq_iff_support_is_affineFlat
  {n r : ā„•} (f : CryptBoolean.BooleanFunction n) (hrn : r ā‰¤ n) :
  FABL.functionAlgebraicDegree f = r āˆ§
      CryptBoolean.hammingWeight f = 2 ^ (n - r) ā†”
    āˆƒ H a,
      Module.finrank FABL.š”½ā‚‚ ā†„H = n - r āˆ§
        ā†‘(CryptBoolean.support f) = ā†‘(FABL.binaryAffineSubspace H a)
    theorem CryptBoolean.degree_eq_and_hammingWeight_eq_iff_support_is_affineFlat
  {n r : ā„•}
  (f : CryptBoolean.BooleanFunction n)
  (hrn : r ā‰¤ n) :
  FABL.functionAlgebraicDegree f = r āˆ§
      CryptBoolean.hammingWeight f =
        2 ^ (n - r) ā†”
    āˆƒ H a,
      Module.finrank FABL.š”½ā‚‚ ā†„H = n - r āˆ§
        ā†‘(CryptBoolean.support f) =
          ā†‘(FABL.binaryAffineSubspace H a)
    Carlet Proposition 12 in support form: the minimum-weight words of degree `r` are exactly
the Boolean functions whose support is an affine flat of dimension `n-r`.

The forward proof makes Carlet's equality case explicit through first-coordinate slices: equality forces the nonzero slices, and when necessary their difference, to attain the lower bound recursively; their supports then assemble into a ternary-closed affine set. The reverse proof represents a flat by a basis of its perpendicular space, bounds the degree of the product of the corresponding affine equations, and uses Theorem 1 to show that the bound is exact.

Theorem2.1.6
Group: Chapter 2: Boolean functions and coding (6)
Group member previews
Preview
Theorem 2.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 5
Reverse dependency previews
Preview
Theorem 2.1.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
āœ“Lāˆƒāˆ€N
Tagscarletchapter-3reed-muller-dimensionpage-38fidelity-exact

Dimension of the Reed--Muller code (Carlet, p. 38). For 0\le r\le n, \dim_{\mathbb F_2}R(r,n)=\sum_{i=0}^{r}\binom ni. Consequently, |R(r,n)|=2^{\sum_{i=0}^{r}\binom ni}.

Lean code for Theorem2.1.6ā—2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.reedMuller_card {n r : ā„•} :
  Nat.card ā†„(CryptBoolean.reedMuller r n) =
    2 ^ āˆ‘ j āˆˆ Finset.range (r + 1), n.choose j
    theorem CryptBoolean.reedMuller_card {n r : ā„•} :
  Nat.card
      ā†„(CryptBoolean.reedMuller r n) =
    2 ^
      āˆ‘ j āˆˆ Finset.range (r + 1),
        n.choose j
    The number of Reed--Muller codewords is `2` raised to the number of
square-free monomials of degree at most `r`.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMuller.lean
    complete
    theorem CryptBoolean.reedMuller_finrank {n r : ā„•} :
  Module.finrank FABL.š”½ā‚‚ ā†„(CryptBoolean.reedMuller r n) =
    āˆ‘ j āˆˆ Finset.range (r + 1), n.choose j
    theorem CryptBoolean.reedMuller_finrank
  {n r : ā„•} :
  Module.finrank FABL.š”½ā‚‚
      ā†„(CryptBoolean.reedMuller r n) =
    āˆ‘ j āˆˆ Finset.range (r + 1), n.choose j
    Carlet's dimension formula for the Reed--Muller code `R(r,n)`.
Theorem2.1.7
Group: Chapter 2: Boolean functions and coding (6)
Group member previews
Preview
Theorem 2.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 6
Reverse dependency previews
Preview
Lemma 3.2.12
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
āœ“Lāˆƒāˆ€N
Tagscarletchapter-3theorem-2pages-38-39fidelity-exact

Theorem 2 (Carlet, pp. 38--39). Let 0\le r<n. Equip Boolean functions with the \mathbb F_2-valued inner product \langle f,g\rangle =\bigoplus_{x\in V_n}f(x)g(x). Then R(r,n)^\perp=R(n-r-1,n).

Lean code for Theorem2.1.7ā—6 declarations
  • defdefined in CryptBoolean/Carlet/Chapter03/ReedMullerDuality.lean
    complete
    def CryptBoolean.booleanFunctionPairing (n : ā„•) :
  LinearMap.BilinForm FABL.š”½ā‚‚ (CryptBoolean.BooleanFunction n)
    def CryptBoolean.booleanFunctionPairing
  (n : ā„•) :
  LinearMap.BilinForm FABL.š”½ā‚‚
    (CryptBoolean.BooleanFunction n)
    The standard binary pairing on scalar Boolean functions.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerDuality.lean
    complete
    theorem CryptBoolean.booleanFunctionPairing_apply {n : ā„•}
  (f g : CryptBoolean.BooleanFunction n) :
  ((CryptBoolean.booleanFunctionPairing n) f) g = āˆ‘ x, f x * g x
    theorem CryptBoolean.booleanFunctionPairing_apply
  {n : ā„•}
  (f g : CryptBoolean.BooleanFunction n) :
  ((CryptBoolean.booleanFunctionPairing n)
        f)
      g =
    āˆ‘ x, f x * g x
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerDuality.lean
    complete
    theorem CryptBoolean.booleanFunctionPairing_nondegenerate {n : ā„•} :
  (CryptBoolean.booleanFunctionPairing n).Nondegenerate
    theorem CryptBoolean.booleanFunctionPairing_nondegenerate
  {n : ā„•} :
  (CryptBoolean.booleanFunctionPairing
      n).Nondegenerate
    The standard binary pairing on Boolean functions is nondegenerate.
  • defdefined in CryptBoolean/Carlet/Chapter03/ReedMullerDuality.lean
    complete
    def CryptBoolean.reedMullerDual (r n : ā„•) :
  Submodule FABL.š”½ā‚‚ (CryptBoolean.BooleanFunction n)
    def CryptBoolean.reedMullerDual (r n : ā„•) :
  Submodule FABL.š”½ā‚‚
    (CryptBoolean.BooleanFunction n)
    The orthogonal complement of `R(r,n)` under Carlet's binary pairing.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerDuality.lean
    complete
    theorem CryptBoolean.reedMuller_complement_le_dual {n r : ā„•} (h : r < n) :
  CryptBoolean.reedMuller (n - r - 1) n ā‰¤
    CryptBoolean.reedMullerDual r n
    theorem CryptBoolean.reedMuller_complement_le_dual
  {n r : ā„•} (h : r < n) :
  CryptBoolean.reedMuller (n - r - 1) n ā‰¤
    CryptBoolean.reedMullerDual r n
    Functions of complementary Reed--Muller orders are orthogonal.
  • theoremdefined in CryptBoolean/Carlet/Chapter03/ReedMullerDuality.lean
    complete
    theorem CryptBoolean.reedMullerDual_eq {n r : ā„•} (h : r < n) :
  CryptBoolean.reedMullerDual r n =
    CryptBoolean.reedMuller (n - r - 1) n
    theorem CryptBoolean.reedMullerDual_eq {n r : ā„•}
  (h : r < n) :
  CryptBoolean.reedMullerDual r n =
    CryptBoolean.reedMuller (n - r - 1) n
    Carlet, Chapter 3, Theorem 2: `R(r,n)į—® = R(n-r-1,n)` for `r < n`.