Cryptographic Boolean Functions in Lean

6.3. Primary constructions🔗

Definition6.3.1
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 4
Reverse dependency previews
Preview
Theorem 6.3.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-7relation-59maiorana-mcfarlandpage-117fidelity-exact

Relation (59) (Carlet, p. 117). Let r>0, let r<n, put s=n-r, let \varphi:V_s\to V_r, and let g:V_s\to\mathbb F_2. Define f_{\varphi,g}(x,y) =x\mathbin\cdot\varphi(y)\oplus g(y) =\bigoplus_{i=1}^r x_i\varphi_i(y)\oplus g(y).

Lean code for Definition6.3.1●2 declarations
  • defdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    def CryptBoolean.booleanMaioranaMcFarlandGeneral {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.BooleanFunction (r + s)
    def CryptBoolean.booleanMaioranaMcFarlandGeneral
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.BooleanFunction (r + s)
    Carlet Relation (59): the general Boolean-valued
Maiorana--McFarland function on two coordinate blocks.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    theorem CryptBoolean.booleanMaioranaMcFarlandGeneral_append {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (x : FABL.F₂Cube r)
  (y : FABL.F₂Cube s) :
  CryptBoolean.booleanMaioranaMcFarlandGeneral φ g (Fin.append x y) =
    FABL.f₂DotProduct x (φ y) + g y
    theorem CryptBoolean.booleanMaioranaMcFarlandGeneral_append
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (x : FABL.F₂Cube r)
  (y : FABL.F₂Cube s) :
  CryptBoolean.booleanMaioranaMcFarlandGeneral
      φ g (Fin.append x y) =
    FABL.f₂DotProduct x (φ y) + g y
    Evaluation of a general Maiorana--McFarland function on its two
coordinate blocks.
Theorem6.3.2
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 1.7.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 6.3.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-7relation-60maiorana-mcfarlandwalsh-transformpage-117fidelity-exact

Relation (60) (Carlet, p. 117). For every a\in V_r and b\in V_s, W_{f_{\varphi,g}}(a,b) =2^r\sum_{y\in\varphi^{-1}(a)} (-1)^{g(y)\oplus b\cdot y}.

Lean code for Theorem6.3.2●1 theorem
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    theorem CryptBoolean.walshTransform_booleanMaioranaMcFarlandGeneral {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  CryptBoolean.walshTransform
      (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)
      (Fin.append a b) =
    2 ^ r * CryptBoolean.maioranaMcFarlandFiberCharacterSum φ g a b
    theorem CryptBoolean.walshTransform_booleanMaioranaMcFarlandGeneral
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  CryptBoolean.walshTransform
      (CryptBoolean.booleanMaioranaMcFarlandGeneral
        φ g)
      (Fin.append a b) =
    2 ^ r *
      CryptBoolean.maioranaMcFarlandFiberCharacterSum
        φ g a b
    Carlet Relation (60): the raw Walsh spectrum of the general
Maiorana--McFarland function is its fiber character sum scaled by `2 ^ r`.
Theorem6.3.3
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 3.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-7maiorana-mcfarlandresiliencypages-117-118fidelity-exact

Resiliency of the general Maiorana--McFarland construction (Carlet, pp. 117--118). If w_H(\varphi(y))>k for every y\in V_s, then f_{\varphi,g} is k-resilient. In particular, it is balanced when 0\notin\operatorname{im}(\varphi). If additionally the restriction of g to every fiber \varphi^{-1}(a) is balanced, then f_{\varphi,g} is (k+1)-resilient. An empty fiber satisfies the latter condition vacuously.

Lean code for Theorem6.3.3●3 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    theorem CryptBoolean.isResilient_booleanMaioranaMcFarlandGeneral {r s : ℕ}
  (k : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hφ : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card) :
  CryptBoolean.IsResilient k
    (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)
    theorem CryptBoolean.isResilient_booleanMaioranaMcFarlandGeneral
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hφ :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card) :
  CryptBoolean.IsResilient k
    (CryptBoolean.booleanMaioranaMcFarlandGeneral
      φ g)
    If every value of the frequency map has weight greater than `k`, the
general Maiorana--McFarland function is `k`-resilient.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    theorem CryptBoolean.isBalanced_booleanMaioranaMcFarlandGeneral {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hφ : ∀ (y : FABL.F₂Cube s), φ y ≠ 0) :
  CryptBoolean.IsBalanced
    (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)
    theorem CryptBoolean.isBalanced_booleanMaioranaMcFarlandGeneral
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hφ : ∀ (y : FABL.F₂Cube s), φ y ≠ 0) :
  CryptBoolean.IsBalanced
    (CryptBoolean.booleanMaioranaMcFarlandGeneral
      φ g)
    Excluding zero from the image of the frequency map makes the general
Maiorana--McFarland function balanced.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    theorem CryptBoolean.isResilient_succ_booleanMaioranaMcFarlandGeneral {r s : ℕ}
  (k : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hs : 0 < s)
  (hφ : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card)
  (hbalancedFiber :
    ∀ (a : FABL.F₂Cube r),
      CryptBoolean.maioranaMcFarlandFiberCharacterSum φ g a 0 = 0) :
  CryptBoolean.IsResilient (k + 1)
    (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)
    theorem CryptBoolean.isResilient_succ_booleanMaioranaMcFarlandGeneral
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hs : 0 < s)
  (hφ :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card)
  (hbalancedFiber :
    ∀ (a : FABL.F₂Cube r),
      CryptBoolean.maioranaMcFarlandFiberCharacterSum
          φ g a 0 =
        0) :
  CryptBoolean.IsResilient (k + 1)
    (CryptBoolean.booleanMaioranaMcFarlandGeneral
      φ g)
    If every frequency-map value has weight greater than `k` and the offset
has zero signed sum on every fiber, the construction is `(k + 1)`-resilient.
Theorem6.3.4
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 1.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-7maiorana-mcfarlandalgebraic-degreepage-118fidelity-corrected-unary-endpoint

Degree of the general Maiorana--McFarland construction (Carlet, p. 118). For f_{\varphi,g} on V_r\times V_s, \deg_{\mathrm{alg}}(f_{\varphi,g})\le s+1, with equality exactly when some coordinate of \varphi has degree s. If every value of \varphi has weight greater than k, equality can hold only when k\le r-2.

Suppose the resiliency order is k. The function reaches Siegenthaler's bound n-k-1 exactly in one of the following cases:

  • k=r-2 and \deg_{\mathrm{alg}}(\varphi)=s=n-k-2;

  • k=r-1, \varphi is the constant all-one map, and either s=1 or \deg_{\mathrm{alg}}(g)=s=n-k-1.

Lean code for Theorem6.3.4●12 declarations
  • defdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    def CryptBoolean.maioranaMcFarlandCoordinate {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) (i : Fin r) :
  CryptBoolean.BooleanFunction s
    def CryptBoolean.maioranaMcFarlandCoordinate
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (i : Fin r) :
  CryptBoolean.BooleanFunction s
    The `i`th Boolean coordinate function of a binary vector-valued map.
  • defdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    def CryptBoolean.maioranaMcFarlandMapAlgebraicDegree {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) : ℕ
    def CryptBoolean.maioranaMcFarlandMapAlgebraicDegree
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) : ℕ
    The algebraic degree of a binary vector-valued map is the largest degree
of one of its coordinate functions.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_maioranaMcFarlandCoordinate_le
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r) (i : Fin r) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.maioranaMcFarlandCoordinate φ i) ≤
    CryptBoolean.maioranaMcFarlandMapAlgebraicDegree φ
    theorem CryptBoolean.functionAlgebraicDegree_maioranaMcFarlandCoordinate_le
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (i : Fin r) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.maioranaMcFarlandCoordinate
        φ i) ≤
    CryptBoolean.maioranaMcFarlandMapAlgebraicDegree
      φ
    Every coordinate degree is bounded by the degree of the vector-valued
map.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.maioranaMcFarlandMapAlgebraicDegree_le_dimension {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) :
  CryptBoolean.maioranaMcFarlandMapAlgebraicDegree φ ≤ s
    theorem CryptBoolean.maioranaMcFarlandMapAlgebraicDegree_le_dimension
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) :
  CryptBoolean.maioranaMcFarlandMapAlgebraicDegree
      φ ≤
    s
    The degree of a vector-valued map is bounded by the dimension of its
domain.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.maioranaMcFarlandMapAlgebraicDegree_eq_dimension_iff
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r) (hr : 0 < r) :
  CryptBoolean.maioranaMcFarlandMapAlgebraicDegree φ = s ↔
    ∃ i,
      FABL.functionAlgebraicDegree
          (CryptBoolean.maioranaMcFarlandCoordinate φ i) =
        s
    theorem CryptBoolean.maioranaMcFarlandMapAlgebraicDegree_eq_dimension_iff
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (hr : 0 < r) :
  CryptBoolean.maioranaMcFarlandMapAlgebraicDegree
        φ =
      s ↔
    ∃ i,
      FABL.functionAlgebraicDegree
          (CryptBoolean.maioranaMcFarlandCoordinate
            φ i) =
        s
    In a nonempty codomain, a vector-valued map has full degree exactly when
one coordinate function has full degree.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_booleanMaioranaMcFarlandGeneral_le
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) ≤
    s + 1
    theorem CryptBoolean.functionAlgebraicDegree_booleanMaioranaMcFarlandGeneral_le
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.booleanMaioranaMcFarlandGeneral
        φ g) ≤
    s + 1
    The general Maiorana--McFarland function on `r+s` variables has
algebraic degree at most `s+1`.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_booleanMaioranaMcFarlandGeneral_eq_iff
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hs : 0 < s) :
  FABL.functionAlgebraicDegree
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
      s + 1 ↔
    ∃ i,
      FABL.functionAlgebraicDegree
          (CryptBoolean.maioranaMcFarlandCoordinate φ i) =
        s
    theorem CryptBoolean.functionAlgebraicDegree_booleanMaioranaMcFarlandGeneral_eq_iff
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hs : 0 < s) :
  FABL.functionAlgebraicDegree
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) =
      s + 1 ↔
    ∃ i,
      FABL.functionAlgebraicDegree
          (CryptBoolean.maioranaMcFarlandCoordinate
            φ i) =
        s
    The degree upper bound is sharp exactly when one coordinate function of
`φ` has full degree `s`.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_booleanMaioranaMcFarlandGeneral_eq_iff_mapDegree
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hr : 0 < r) (hs : 0 < s) :
  FABL.functionAlgebraicDegree
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
      s + 1 ↔
    CryptBoolean.maioranaMcFarlandMapAlgebraicDegree φ = s
    theorem CryptBoolean.functionAlgebraicDegree_booleanMaioranaMcFarlandGeneral_eq_iff_mapDegree
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hr : 0 < r) (hs : 0 < s) :
  FABL.functionAlgebraicDegree
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) =
      s + 1 ↔
    CryptBoolean.maioranaMcFarlandMapAlgebraicDegree
        φ =
      s
    The degree upper bound is sharp exactly when the vector-valued map has
full algebraic degree.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_booleanMaioranaMcFarlandGeneral_constant_one
  {r s : ℕ} (g : CryptBoolean.BooleanFunction s) (hr : 0 < r) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.booleanMaioranaMcFarlandGeneral (fun x => 1) g) =
    max 1 (FABL.functionAlgebraicDegree g)
    theorem CryptBoolean.functionAlgebraicDegree_booleanMaioranaMcFarlandGeneral_constant_one
  {r s : ℕ}
  (g : CryptBoolean.BooleanFunction s)
  (hr : 0 < r) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.booleanMaioranaMcFarlandGeneral
        (fun x => 1) g) =
    max 1 (FABL.functionAlgebraicDegree g)
    For the constant all-one frequency map, the construction is the direct
sum of full parity and `g`, hence has degree `max 1 (deg g)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.le_r_sub_two_of_weight_gt_of_maioranaMcFarland_degree_eq
  {r s : ℕ} (k : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hr : 0 < r) (hs : 0 < s)
  (hweight : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card)
  (hdegree :
    FABL.functionAlgebraicDegree
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
      s + 1) :
  k ≤ r - 2
    theorem CryptBoolean.le_r_sub_two_of_weight_gt_of_maioranaMcFarland_degree_eq
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hr : 0 < r) (hs : 0 < s)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card)
  (hdegree :
    FABL.functionAlgebraicDegree
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) =
      s + 1) :
  k ≤ r - 2
    If every image value has weight greater than `k`, sharpness of the
`s+1` degree bound forces `k ≤ r-2`.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_booleanMaioranaMcFarlandGeneral_eq_siegenthalerBound_iff
  {r s : ℕ} (k : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hr : 0 < r) (hs : 0 < s)
  (hweight : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card) :
  FABL.functionAlgebraicDegree
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
      r + s - k - 1 ↔
    k = r - 2 ∧
        CryptBoolean.maioranaMcFarlandMapAlgebraicDegree φ = s ∧
          s = r + s - k - 2 ∨
      k = r - 1 ∧
        (φ = fun x => 1) ∧
          (s = 1 ∨ FABL.functionAlgebraicDegree g = s) ∧
            s = r + s - k - 1
    theorem CryptBoolean.functionAlgebraicDegree_booleanMaioranaMcFarlandGeneral_eq_siegenthalerBound_iff
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hr : 0 < r) (hs : 0 < s)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card) :
  FABL.functionAlgebraicDegree
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) =
      r + s - k - 1 ↔
    k = r - 2 ∧
        CryptBoolean.maioranaMcFarlandMapAlgebraicDegree
              φ =
            s ∧
          s = r + s - k - 2 ∨
      k = r - 1 ∧
        (φ = fun x => 1) ∧
          (s = 1 ∨
              FABL.functionAlgebraicDegree
                  g =
                s) ∧
            s = r + s - k - 1
    For the construction's weight-guaranteed resiliency order `k`, equality
in Siegenthaler's degree bound occurs exactly in Carlet's two branches. The
constant-map branch includes the corrected unary endpoint, where the full
parity term already has degree one for every `g`.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.isResilient_and_functionAlgebraicDegree_eq_siegenthalerBound_iff
  {r s : ℕ} (k : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hr : 0 < r) (hs : 0 < s)
  (hweight : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card) :
  CryptBoolean.IsResilient k
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) ∧
      FABL.functionAlgebraicDegree
          (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
        r + s - k - 1 ↔
    k = r - 2 ∧
        CryptBoolean.maioranaMcFarlandMapAlgebraicDegree φ = s ∧
          s = r + s - k - 2 ∨
      k = r - 1 ∧
        (φ = fun x => 1) ∧
          (s = 1 ∨ FABL.functionAlgebraicDegree g = s) ∧
            s = r + s - k - 1
    theorem CryptBoolean.isResilient_and_functionAlgebraicDegree_eq_siegenthalerBound_iff
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hr : 0 < r) (hs : 0 < s)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card) :
  CryptBoolean.IsResilient k
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) ∧
      FABL.functionAlgebraicDegree
          (CryptBoolean.booleanMaioranaMcFarlandGeneral
            φ g) =
        r + s - k - 1 ↔
    k = r - 2 ∧
        CryptBoolean.maioranaMcFarlandMapAlgebraicDegree
              φ =
            s ∧
          s = r + s - k - 2 ∨
      k = r - 1 ∧
        (φ = fun x => 1) ∧
          (s = 1 ∨
              FABL.functionAlgebraicDegree
                  g =
                s) ∧
            s = r + s - k - 1
    Under the weight hypothesis, the same classification describes when the
resulting `k`-resilient function reaches Siegenthaler's degree bound.
Theorem6.3.5
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 3.2.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-7relation-61maiorana-mcfarlandnonlinearitypage-118fidelity-exact

Relation (61) (Carlet, p. 118). Let M=\max_{a\in V_r}|\varphi^{-1}(a)|. Then \operatorname{nl}(f_{\varphi,g}) \ge 2^{n-1}-2^{r-1}M.

Lean code for Theorem6.3.5●7 declarations
  • defdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    def CryptBoolean.maioranaMcFarlandFiberCardinality {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) (a : FABL.F₂Cube r) : ℕ
    def CryptBoolean.maioranaMcFarlandFiberCardinality
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (a : FABL.F₂Cube r) : ℕ
    The cardinality of one fiber of a general Maiorana--McFarland frequency
map.
  • defdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    def CryptBoolean.maxMaioranaMcFarlandFiberCardinality {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) : ℕ
    def CryptBoolean.maxMaioranaMcFarlandFiberCardinality
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) : ℕ
    The largest fiber cardinality of a general Maiorana--McFarland frequency
map.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    theorem CryptBoolean.maioranaMcFarlandFiberCardinality_le_max {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) (a : FABL.F₂Cube r) :
  CryptBoolean.maioranaMcFarlandFiberCardinality φ a ≤
    CryptBoolean.maxMaioranaMcFarlandFiberCardinality φ
    theorem CryptBoolean.maioranaMcFarlandFiberCardinality_le_max
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (a : FABL.F₂Cube r) :
  CryptBoolean.maioranaMcFarlandFiberCardinality
      φ a ≤
    CryptBoolean.maxMaioranaMcFarlandFiberCardinality
      φ
    Every fiber cardinality is bounded by the largest fiber cardinality.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    theorem CryptBoolean.maioranaMcFarlandFiberCharacterSum_natAbs_le_cardinality
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  (CryptBoolean.maioranaMcFarlandFiberCharacterSum φ g a b).natAbs ≤
    CryptBoolean.maioranaMcFarlandFiberCardinality φ a
    theorem CryptBoolean.maioranaMcFarlandFiberCharacterSum_natAbs_le_cardinality
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  (CryptBoolean.maioranaMcFarlandFiberCharacterSum
        φ g a b).natAbs ≤
    CryptBoolean.maioranaMcFarlandFiberCardinality
      φ a
    A fiber character sum is bounded by the cardinality of its fiber.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    theorem CryptBoolean.maxWalshMagnitude_booleanMaioranaMcFarlandGeneral_le
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) ≤
    2 ^ r * CryptBoolean.maxMaioranaMcFarlandFiberCardinality φ
    theorem CryptBoolean.maxWalshMagnitude_booleanMaioranaMcFarlandGeneral_le
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.booleanMaioranaMcFarlandGeneral
        φ g) ≤
    2 ^ r *
      CryptBoolean.maxMaioranaMcFarlandFiberCardinality
        φ
    The largest raw Walsh magnitude of a general Maiorana--McFarland
function is bounded by `2 ^ r` times its largest fiber.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    theorem CryptBoolean.relation_61_booleanMaioranaMcFarlandGeneral {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  2 ^ (r + s) ≤
    2 *
        CryptBoolean.nonlinearity
          (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) +
      2 ^ r * CryptBoolean.maxMaioranaMcFarlandFiberCardinality φ
    theorem CryptBoolean.relation_61_booleanMaioranaMcFarlandGeneral
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  2 ^ (r + s) ≤
    2 *
        CryptBoolean.nonlinearity
          (CryptBoolean.booleanMaioranaMcFarlandGeneral
            φ g) +
      2 ^ r *
        CryptBoolean.maxMaioranaMcFarlandFiberCardinality
          φ
    Division-free form of Carlet Relation (61).
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarland.lean
    complete
    theorem CryptBoolean.nonlinearity_booleanMaioranaMcFarlandGeneral_lower_bound
  {r s : ℕ} (hr : 0 < r) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  2 ^ (r + s - 1) -
      2 ^ (r - 1) *
        CryptBoolean.maxMaioranaMcFarlandFiberCardinality φ ≤
    CryptBoolean.nonlinearity
      (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)
    theorem CryptBoolean.nonlinearity_booleanMaioranaMcFarlandGeneral_lower_bound
  {r s : ℕ} (hr : 0 < r)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  2 ^ (r + s - 1) -
      2 ^ (r - 1) *
        CryptBoolean.maxMaioranaMcFarlandFiberCardinality
          φ ≤
    CryptBoolean.nonlinearity
      (CryptBoolean.booleanMaioranaMcFarlandGeneral
        φ g)
    Carlet Relation (61): the nonlinearity lower bound determined by the
largest fiber of the frequency map.
Theorem6.3.6
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.9.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-7relation-62maiorana-mcfarlandnonlinearitypages-118-119fidelity-exact-ceiling

Relation (62) (Carlet, pp. 118--119). With M=\max_a|\varphi^{-1}(a)|, \operatorname{nl}(f_{\varphi,g}) \le 2^{n-1}-2^{r-1}\lceil\sqrt M\rceil. More precisely, for every a\in V_r, \sum_{b\in V_s} \left( \sum_{y\in\varphi^{-1}(a)}(-1)^{g(y)\oplus b\cdot y} \right)^2 =2^s|\varphi^{-1}(a)|.

Lean code for Theorem6.3.6●3 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandUpper.lean
    complete
    theorem CryptBoolean.sum_sq_maioranaMcFarlandFiberCharacterSum {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (a : FABL.F₂Cube r) :
  ∑ b, ↑(CryptBoolean.maioranaMcFarlandFiberCharacterSum φ g a b) ^ 2 =
    2 ^ s * ↑(CryptBoolean.maioranaMcFarlandFiberCardinality φ a)
    theorem CryptBoolean.sum_sq_maioranaMcFarlandFiberCharacterSum
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (a : FABL.F₂Cube r) :
  ∑ b,
      ↑(CryptBoolean.maioranaMcFarlandFiberCharacterSum
            φ g a b) ^
        2 =
    2 ^ s *
      ↑(CryptBoolean.maioranaMcFarlandFiberCardinality
          φ a)
    Parseval on a fiber: the square mass of all fiber character sums is the
cube size times the fiber cardinality.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandUpper.lean
    complete
    theorem CryptBoolean.two_pow_mul_ceil_sqrt_maxFiber_le_maxWalshMagnitude
  {r s : ℕ} (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  2 ^ r * ⌈√↑(CryptBoolean.maxMaioranaMcFarlandFiberCardinality φ)⌉₊ ≤
    CryptBoolean.maxWalshMagnitude
      (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)
    theorem CryptBoolean.two_pow_mul_ceil_sqrt_maxFiber_le_maxWalshMagnitude
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  2 ^ r *
      ⌈√↑(CryptBoolean.maxMaioranaMcFarlandFiberCardinality
              φ)⌉₊ ≤
    CryptBoolean.maxWalshMagnitude
      (CryptBoolean.booleanMaioranaMcFarlandGeneral
        φ g)
    Some Walsh coefficient has magnitude at least `2^r` times the ceiling of
the square root of the largest fiber.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandUpper.lean
    complete
    theorem CryptBoolean.nonlinearity_booleanMaioranaMcFarlandGeneral_upper_bound
  {r s : ℕ} (hr : 0 < r) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.nonlinearity
      (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) ≤
    2 ^ (r + s - 1) -
      2 ^ (r - 1) *
        ⌈√↑(CryptBoolean.maxMaioranaMcFarlandFiberCardinality φ)⌉₊
    theorem CryptBoolean.nonlinearity_booleanMaioranaMcFarlandGeneral_upper_bound
  {r s : ℕ} (hr : 0 < r)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.nonlinearity
      (CryptBoolean.booleanMaioranaMcFarlandGeneral
        φ g) ≤
    2 ^ (r + s - 1) -
      2 ^ (r - 1) *
        ⌈√↑(CryptBoolean.maxMaioranaMcFarlandFiberCardinality
                φ)⌉₊
    Carlet Relation (62): the largest fiber forces an upper bound on the
nonlinearity of a general Maiorana--McFarland function.
Theorem6.3.7
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 6.3.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-7maiorana-mcfarlandclassificationpage-119fidelity-explicit-unary-endpoint

Optimal Maiorana--McFarland parameters (Carlet, p. 119). Suppose w_H(\varphi(y))>k for every y and \operatorname{nl}(f_{\varphi,g})=2^{n-1}-2^{k+1}. Then r=k+1 or r=k+2.

If r=k+1, then \varphi is the constant all-one map, n\le k+3, and either s=1 with arbitrary unary g, or s=2 with g(y_1,y_2)=y_1y_2\oplus\ell(y) for an affine \ell.

If r=k+2, then \varphi is injective, n\le k+2+\log_2(k+3), g is arbitrary, and \deg_{\mathrm{alg}}(f_{\varphi,g})\le1+\log_2(k+3).

Lean code for Theorem6.3.7●18 declarations
  • theoremdefined in CryptBoolean/Carlet/Chapter07/SarkarMaitra.lean
    complete
    theorem CryptBoolean.maxWalshMagnitude_eq_two_pow_m_add_two_of_nonlinearity_eq
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (m : ℕ) (hm : m + 2 ≤ n)
  (hnonlinearity :
    CryptBoolean.nonlinearity f = 2 ^ (n - 1) - 2 ^ (m + 1)) :
  CryptBoolean.maxWalshMagnitude f = 2 ^ (m + 2)
    theorem CryptBoolean.maxWalshMagnitude_eq_two_pow_m_add_two_of_nonlinearity_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m : ℕ) (hm : m + 2 ≤ n)
  (hnonlinearity :
    CryptBoolean.nonlinearity f =
      2 ^ (n - 1) - 2 ^ (m + 1)) :
  CryptBoolean.maxWalshMagnitude f =
    2 ^ (m + 2)
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.map_eq_one_of_weight_gt_natPred {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r) (hr : 0 < r)
  (hweight :
    ∀ (y : FABL.F₂Cube s), r - 1 < (FABL.f₂Support (φ y)).card) :
  φ = fun x => 1
    theorem CryptBoolean.map_eq_one_of_weight_gt_natPred
  {r s : ℕ}
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (hr : 0 < r)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      r - 1 <
        (FABL.f₂Support (φ y)).card) :
  φ = fun x => 1
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandDegree.lean
    complete
    theorem CryptBoolean.booleanMaioranaMcFarlandGeneral_constant_one_eq_directSum
  {r s : ℕ} (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.booleanMaioranaMcFarlandGeneral (fun x => 1) g =
    CryptBoolean.booleanDirectSum (⇑(FABL.coordinateSum Finset.univ)) g
    theorem CryptBoolean.booleanMaioranaMcFarlandGeneral_constant_one_eq_directSum
  {r s : ℕ}
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.booleanMaioranaMcFarlandGeneral
      (fun x => 1) g =
    CryptBoolean.booleanDirectSum
      (⇑(FABL.coordinateSum Finset.univ))
      g
  • defdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    def CryptBoolean.twoVariableProduct : CryptBoolean.BooleanFunction 2
    def CryptBoolean.twoVariableProduct :
  CryptBoolean.BooleanFunction 2
    The quadratic product of the two coordinate functions.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.twoVariableProduct_apply (y : FABL.F₂Cube 2) :
  CryptBoolean.twoVariableProduct y = y 0 * y 1
    theorem CryptBoolean.twoVariableProduct_apply
  (y : FABL.F₂Cube 2) :
  CryptBoolean.twoVariableProduct y =
    y 0 * y 1
  • defdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    def CryptBoolean.twoVariableProductAt {s : ℕ} (hs : s = 2) :
  CryptBoolean.BooleanFunction s
    def CryptBoolean.twoVariableProductAt {s : ℕ}
  (hs : s = 2) :
  CryptBoolean.BooleanFunction s
    The two-coordinate product on a cube whose dimension is identified with
two.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.maxWalshMagnitude_eq_of_maioranaMcFarland_optimal {r s : ℕ}
  (k : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hs : 0 < s)
  (hweight : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1)) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
    2 ^ (k + 2)
    theorem CryptBoolean.maxWalshMagnitude_eq_of_maioranaMcFarland_optimal
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hs : 0 < s)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1)) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.booleanMaioranaMcFarlandGeneral
        φ g) =
    2 ^ (k + 2)
    Equality in the resilient nonlinearity bound fixes the maximum Walsh
magnitude at `2^(k+2)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.leftDimension_eq_succ_or_add_two_of_maioranaMcFarland_optimal
  {r s : ℕ} (k : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hs : 0 < s)
  (hweight : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1)) :
  r = k + 1 ∨ r = k + 2
    theorem CryptBoolean.leftDimension_eq_succ_or_add_two_of_maioranaMcFarland_optimal
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hs : 0 < s)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1)) :
  r = k + 1 ∨ r = k + 2
    Under the strict image-weight hypothesis, optimal nonlinearity forces
the left block dimension to be either `k+1` or `k+2`.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.maxMaioranaMcFarlandFiberCardinality_const {r s : ℕ}
  (a : FABL.F₂Cube r) :
  (CryptBoolean.maxMaioranaMcFarlandFiberCardinality fun x => a) = 2 ^ s
    theorem CryptBoolean.maxMaioranaMcFarlandFiberCardinality_const
  {r s : ℕ} (a : FABL.F₂Cube r) :
  (CryptBoolean.maxMaioranaMcFarlandFiberCardinality
      fun x => a) =
    2 ^ s
    The largest fiber of a constant frequency map is the entire domain.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.exists_eq_twoVariableProduct_add_affine_of_maxWalshMagnitude_eq_two
  (g : CryptBoolean.BooleanFunction 2)
  (hmax : CryptBoolean.maxWalshMagnitude g = 2) :
  ∃ c a, g = CryptBoolean.twoVariableProduct + FABL.affineFunction c a
    theorem CryptBoolean.exists_eq_twoVariableProduct_add_affine_of_maxWalshMagnitude_eq_two
  (g : CryptBoolean.BooleanFunction 2)
  (hmax :
    CryptBoolean.maxWalshMagnitude g =
      2) :
  ∃ c a,
    g =
      CryptBoolean.twoVariableProduct +
        FABL.affineFunction c a
    A two-variable Boolean function with maximum Walsh magnitude two is its
quadratic coordinate product plus an affine function.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.exists_eq_twoVariableProductAt_add_affine_of_maxWalshMagnitude_eq_two
  {s : ℕ} (g : CryptBoolean.BooleanFunction s) (hsTwo : s = 2)
  (hmax : CryptBoolean.maxWalshMagnitude g = 2) :
  ∃ c a,
    g =
      CryptBoolean.twoVariableProductAt hsTwo + FABL.affineFunction c a
    theorem CryptBoolean.exists_eq_twoVariableProductAt_add_affine_of_maxWalshMagnitude_eq_two
  {s : ℕ}
  (g : CryptBoolean.BooleanFunction s)
  (hsTwo : s = 2)
  (hmax :
    CryptBoolean.maxWalshMagnitude g =
      2) :
  ∃ c a,
    g =
      CryptBoolean.twoVariableProductAt
          hsTwo +
        FABL.affineFunction c a
    The same quadratic-affine classification transported along an equality
of the domain dimension with two.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.maioranaMcFarland_optimal_constant_branch {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hr : 0 < r) (hs : 0 < s)
  (hweight : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1))
  (hrank : r = k + 1) :
  (φ = fun x => 1) ∧
    r + s ≤ k + 3 ∧
      (s = 1 ∨
        ∃ (hsTwo : s = 2),
          ∃ c a,
            g =
              CryptBoolean.twoVariableProductAt hsTwo +
                FABL.affineFunction c a)
    theorem CryptBoolean.maioranaMcFarland_optimal_constant_branch
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hr : 0 < r) (hs : 0 < s)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1))
  (hrank : r = k + 1) :
  (φ = fun x => 1) ∧
    r + s ≤ k + 3 ∧
      (s = 1 ∨
        ∃ (hsTwo : s = 2),
          ∃ c a,
            g =
              CryptBoolean.twoVariableProductAt
                  hsTwo +
                FABL.affineFunction c a)
    In the `r=k+1` branch, the frequency map is constant all-one, the right
block has at most two variables, and the binary endpoint is quadratic up to
an affine function.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.injective_of_maioranaMcFarland_optimal_add_two_branch
  {r s : ℕ} (k : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hs : 0 < s)
  (hweight : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1))
  (hrank : r = k + 2) : Function.Injective φ
    theorem CryptBoolean.injective_of_maioranaMcFarland_optimal_add_two_branch
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hs : 0 < s)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1))
  (hrank : r = k + 2) :
  Function.Injective φ
    In the `r=k+2` branch, every frequency-map fiber is a singleton or
empty, so the frequency map is injective.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.card_highWeightCube {r : ℕ} (hr : 2 ≤ r) :
  Fintype.card { a // r - 2 < (FABL.f₂Support a).card } = r + 1
    theorem CryptBoolean.card_highWeightCube {r : ℕ}
  (hr : 2 ≤ r) :
  Fintype.card
      { a //
        r - 2 <
          (FABL.f₂Support a).card } =
    r + 1
    There are exactly `r+1` binary vectors of length `r` and weight strictly
greater than `r-2`.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.two_pow_rightDimension_le_k_add_three_of_add_two_branch
  {r s : ℕ} (k : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (hweight : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card)
  (hinjective : Function.Injective φ) (hrank : r = k + 2) :
  2 ^ s ≤ k + 3
    theorem CryptBoolean.two_pow_rightDimension_le_k_add_three_of_add_two_branch
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card)
  (hinjective : Function.Injective φ)
  (hrank : r = k + 2) : 2 ^ s ≤ k + 3
    Injectivity into the two highest-weight layers gives the sharp finite
dimension inequality `2^s ≤ k+3` in the `r=k+2` branch.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.rightDimension_cast_le_logb_two_k_add_three (k s : ℕ)
  (hpower : 2 ^ s ≤ k + 3) : ↑s ≤ Real.logb 2 ↑(k + 3)
    theorem CryptBoolean.rightDimension_cast_le_logb_two_k_add_three
  (k s : ℕ) (hpower : 2 ^ s ≤ k + 3) :
  ↑s ≤ Real.logb 2 ↑(k + 3)
    The finite power inequality `2^s ≤ k+3` implies Carlet's printed
real-valued logarithmic dimension bound.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.maioranaMcFarland_optimal_injective_branch {r s : ℕ}
  (k : ℕ) (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hs : 0 < s)
  (hweight : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1))
  (hrank : r = k + 2) :
  Function.Injective φ ∧
    ↑(r + s) ≤ ↑(k + 2) + Real.logb 2 ↑(k + 3) ∧
      ↑(FABL.functionAlgebraicDegree
            (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)) ≤
        1 + Real.logb 2 ↑(k + 3)
    theorem CryptBoolean.maioranaMcFarland_optimal_injective_branch
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hs : 0 < s)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1))
  (hrank : r = k + 2) :
  Function.Injective φ ∧
    ↑(r + s) ≤
        ↑(k + 2) + Real.logb 2 ↑(k + 3) ∧
      ↑(FABL.functionAlgebraicDegree
            (CryptBoolean.booleanMaioranaMcFarlandGeneral
              φ g)) ≤
        1 + Real.logb 2 ↑(k + 3)
    In the `r=k+2` branch, the frequency map is injective and both the
dimension and algebraic degree satisfy Carlet's real logarithmic bounds.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/MaioranaMcFarlandOptimal.lean
    complete
    theorem CryptBoolean.maioranaMcFarland_optimal_classification {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s) (hr : 0 < r) (hs : 0 < s)
  (hweight : ∀ (y : FABL.F₂Cube s), k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1)) :
  r = k + 1 ∧
      (φ = fun x => 1) ∧
        r + s ≤ k + 3 ∧
          (s = 1 ∨
            ∃ (hsTwo : s = 2),
              ∃ c a,
                g =
                  CryptBoolean.twoVariableProductAt hsTwo +
                    FABL.affineFunction c a) ∨
    r = k + 2 ∧
      Function.Injective φ ∧
        ↑(r + s) ≤ ↑(k + 2) + Real.logb 2 ↑(k + 3) ∧
          ↑(FABL.functionAlgebraicDegree
                (CryptBoolean.booleanMaioranaMcFarlandGeneral φ g)) ≤
            1 + Real.logb 2 ↑(k + 3)
    theorem CryptBoolean.maioranaMcFarland_optimal_classification
  {r s : ℕ} (k : ℕ)
  (φ : FABL.F₂Cube s → FABL.F₂Cube r)
  (g : CryptBoolean.BooleanFunction s)
  (hr : 0 < r) (hs : 0 < s)
  (hweight :
    ∀ (y : FABL.F₂Cube s),
      k < (FABL.f₂Support (φ y)).card)
  (hnonlinearity :
    CryptBoolean.nonlinearity
        (CryptBoolean.booleanMaioranaMcFarlandGeneral
          φ g) =
      2 ^ (r + s - 1) - 2 ^ (k + 1)) :
  r = k + 1 ∧
      (φ = fun x => 1) ∧
        r + s ≤ k + 3 ∧
          (s = 1 ∨
            ∃ (hsTwo : s = 2),
              ∃ c a,
                g =
                  CryptBoolean.twoVariableProductAt
                      hsTwo +
                    FABL.affineFunction c
                      a) ∨
    r = k + 2 ∧
      Function.Injective φ ∧
        ↑(r + s) ≤
            ↑(k + 2) +
              Real.logb 2 ↑(k + 3) ∧
          ↑(FABL.functionAlgebraicDegree
                (CryptBoolean.booleanMaioranaMcFarlandGeneral
                  φ g)) ≤
            1 + Real.logb 2 ↑(k + 3)
    Carlet's optimal-parameter classification for the general
Maiorana--McFarland construction under the strict image-weight hypothesis.
Theorem6.3.8
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Proposition 1.8.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-7linear-mapresilient-constructionpage-120fidelity-generalized-with-positive-distance

Linear-map construction (Carlet, p. 120). Let k<n, let g:V_k\to\mathbb F_2, let L:V_n\to V_k be a surjective linear map, and let s\in V_n. If C is the row space of a matrix for L and d=\operatorname{dist}(s,C)>0, then f(x)=g(Lx)\oplus s\cdot x is (d-1)-resilient.

Lean code for Theorem6.3.8●7 declarations
  • theoremdefined in CryptBoolean/Carlet/Chapter04/CodeGeneratorResiliency.lean
    complete
    theorem CryptBoolean.vectorFourierCoeff_comp_linearMap_eq_zero_of_not_mem_perpendicular_ker
  {n k : ℕ} (L : FABL.F₂Cube n →ₗ[FABL.𝔽₂] FABL.F₂Cube k)
  (q : FABL.F₂Cube k → ℝ) (u : FABL.F₂Cube n)
  (hu : u ∉ FABL.perpendicularSubspace L.ker) :
  FABL.vectorFourierCoeff (fun x => q (L x)) u = 0
    theorem CryptBoolean.vectorFourierCoeff_comp_linearMap_eq_zero_of_not_mem_perpendicular_ker
  {n k : ℕ}
  (L :
    FABL.F₂Cube n →ₗ[FABL.𝔽₂]
      FABL.F₂Cube k)
  (q : FABL.F₂Cube k → ℝ)
  (u : FABL.F₂Cube n)
  (hu :
    u ∉
      FABL.perpendicularSubspace L.ker) :
  FABL.vectorFourierCoeff
      (fun x => q (L x)) u =
    0
    The Fourier spectrum of a linear pullback is supported on the
perpendicular complement of the kernel of the linear map.
  • defdefined in CryptBoolean/Carlet/Chapter07/LinearPullback.lean
    complete
    def CryptBoolean.binaryCosetMinimumWeight {n : ℕ} (t : FABL.F₂Cube n)
  (C : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) : ℕ
    def CryptBoolean.binaryCosetMinimumWeight
  {n : ℕ} (t : FABL.F₂Cube n)
  (C :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  ℕ
    The minimum Hamming weight in the translate `t + C` of a binary
subspace.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/LinearPullback.lean
    complete
    theorem CryptBoolean.binaryCosetMinimumWeight_le {n : ℕ} (t : FABL.F₂Cube n)
  (C : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (c : FABL.F₂Cube n)
  (hc : c ∈ C) :
  CryptBoolean.binaryCosetMinimumWeight t C ≤
    (FABL.f₂Support (t + c)).card
    theorem CryptBoolean.binaryCosetMinimumWeight_le
  {n : ℕ} (t : FABL.F₂Cube n)
  (C : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (c : FABL.F₂Cube n) (hc : c ∈ C) :
  CryptBoolean.binaryCosetMinimumWeight t
      C ≤
    (FABL.f₂Support (t + c)).card
    The minimum weight of a coset is bounded by the weight of each of its
members.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/LinearPullback.lean
    complete
    theorem CryptBoolean.binaryCosetMinimumWeight_le_dimension {n : ℕ}
  (t : FABL.F₂Cube n) (C : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  CryptBoolean.binaryCosetMinimumWeight t C ≤ n
    theorem CryptBoolean.binaryCosetMinimumWeight_le_dimension
  {n : ℕ} (t : FABL.F₂Cube n)
  (C :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  CryptBoolean.binaryCosetMinimumWeight t
      C ≤
    n
    A binary coset minimum weight never exceeds the ambient dimension.
  • defdefined in CryptBoolean/Carlet/Chapter07/LinearPullback.lean
    complete
    def CryptBoolean.linearPullbackWithFrequency {n k : ℕ}
  (L : FABL.F₂Cube n →ₗ[FABL.𝔽₂] FABL.F₂Cube k)
  (g : CryptBoolean.BooleanFunction k) (t : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.linearPullbackWithFrequency
  {n k : ℕ}
  (L :
    FABL.F₂Cube n →ₗ[FABL.𝔽₂]
      FABL.F₂Cube k)
  (g : CryptBoolean.BooleanFunction k)
  (t : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction n
    Pull a Boolean function back through a linear map and add the parity at
frequency `t`.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/LinearPullback.lean
    complete
    theorem CryptBoolean.walshTransform_linearPullbackWithFrequency {n k : ℕ}
  (L : FABL.F₂Cube n →ₗ[FABL.𝔽₂] FABL.F₂Cube k)
  (g : CryptBoolean.BooleanFunction k) (t u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform
      (CryptBoolean.linearPullbackWithFrequency L g t) u =
    CryptBoolean.walshTransform (fun x => g (L x)) (u + t)
    theorem CryptBoolean.walshTransform_linearPullbackWithFrequency
  {n k : ℕ}
  (L :
    FABL.F₂Cube n →ₗ[FABL.𝔽₂]
      FABL.F₂Cube k)
  (g : CryptBoolean.BooleanFunction k)
  (t u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform
      (CryptBoolean.linearPullbackWithFrequency
        L g t)
      u =
    CryptBoolean.walshTransform
      (fun x => g (L x)) (u + t)
    Adding the outer frequency translates the Walsh spectrum of a linear
pullback.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/LinearPullback.lean
    complete
    theorem CryptBoolean.isResilient_linearPullbackWithFrequency {n k : ℕ}
  (L : FABL.F₂Cube n →ₗ[FABL.𝔽₂] FABL.F₂Cube k)
  (g : CryptBoolean.BooleanFunction k) (t : FABL.F₂Cube n)
  (hd :
    0 <
      CryptBoolean.binaryCosetMinimumWeight t
        (FABL.perpendicularSubspace L.ker)) :
  CryptBoolean.IsResilient
    (CryptBoolean.binaryCosetMinimumWeight t
        (FABL.perpendicularSubspace L.ker) -
      1)
    (CryptBoolean.linearPullbackWithFrequency L g t)
    theorem CryptBoolean.isResilient_linearPullbackWithFrequency
  {n k : ℕ}
  (L :
    FABL.F₂Cube n →ₗ[FABL.𝔽₂]
      FABL.F₂Cube k)
  (g : CryptBoolean.BooleanFunction k)
  (t : FABL.F₂Cube n)
  (hd :
    0 <
      CryptBoolean.binaryCosetMinimumWeight
        t
        (FABL.perpendicularSubspace
          L.ker)) :
  CryptBoolean.IsResilient
    (CryptBoolean.binaryCosetMinimumWeight
        t
        (FABL.perpendicularSubspace
          L.ker) -
      1)
    (CryptBoolean.linearPullbackWithFrequency
      L g t)
    If the frequency translate has positive distance from the Fourier
support subspace of a linear pullback, the resulting function is resilient
to one less than that distance.

The same conclusion holds without surjectivity when C is represented intrinsically as (\ker L)^\perp.

Theorem6.3.9
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.5.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-7relation-63partial-spreadresilient-constructionpages-120-121fidelity-generalized-natural-parameters

Relation (63) (Carlet, pp. 120--121). Put s=n-r and identify V_r with \mathbb F_{2^r}. Let g:\mathbb F_{2^r}\to\mathbb F_2, let \varphi:V_s\to\mathbb F_{2^r} be linear, and let \varphi^*:\mathbb F_{2^r}\to V_s be its adjoint for the trace pairing. Choose a\in\mathbb F_{2^r} and b\in V_s such that a+\varphi(y)\ne0\quad(y\in V_s) and w_H(\varphi^*(z)+b)>k\quad(z\in\mathbb F_{2^r}). Then f(x,y)=g\!\left(\frac{x}{a+\varphi(y)}\right)\oplus b\cdot y is k-resilient.

Lean code for Theorem6.3.9●4 declarations
  • defdefined in CryptBoolean/Carlet/Chapter07/PartialSpreadResilient.lean
    complete
    def CryptBoolean.partialSpreadResilientFunction {r s : ℕ}
  (theta : FABL.F₂Cube r ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField r)
  (g : CryptBoolean.FieldBooleanFunction r)
  (phi : FABL.F₂Cube s →ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField r)
  (a : CryptBoolean.BinaryGaloisField r) (b : FABL.F₂Cube s) :
  CryptBoolean.BooleanFunction (r + s)
    def CryptBoolean.partialSpreadResilientFunction
  {r s : ℕ}
  (theta :
    FABL.F₂Cube r ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField r)
  (g :
    CryptBoolean.FieldBooleanFunction r)
  (phi :
    FABL.F₂Cube s →ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField r)
  (a : CryptBoolean.BinaryGaloisField r)
  (b : FABL.F₂Cube s) :
  CryptBoolean.BooleanFunction (r + s)
    The partial-spread quotient construction in explicit field and cube
coordinates.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/PartialSpreadResilient.lean
    complete
    theorem CryptBoolean.partialSpreadResilientFunction_append {r s : ℕ}
  (theta : FABL.F₂Cube r ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField r)
  (g : CryptBoolean.FieldBooleanFunction r)
  (phi : FABL.F₂Cube s →ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField r)
  (a : CryptBoolean.BinaryGaloisField r) (b : FABL.F₂Cube s)
  (x : FABL.F₂Cube r) (y : FABL.F₂Cube s) :
  CryptBoolean.partialSpreadResilientFunction theta g phi a b
      (Fin.append x y) =
    g (theta x / (a + phi y)) + FABL.f₂DotProduct b y
    theorem CryptBoolean.partialSpreadResilientFunction_append
  {r s : ℕ}
  (theta :
    FABL.F₂Cube r ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField r)
  (g :
    CryptBoolean.FieldBooleanFunction r)
  (phi :
    FABL.F₂Cube s →ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField r)
  (a : CryptBoolean.BinaryGaloisField r)
  (b : FABL.F₂Cube s) (x : FABL.F₂Cube r)
  (y : FABL.F₂Cube s) :
  CryptBoolean.partialSpreadResilientFunction
      theta g phi a b (Fin.append x y) =
    g (theta x / (a + phi y)) +
      FABL.f₂DotProduct b y
  • theoremdefined in CryptBoolean/Carlet/Chapter07/PartialSpreadResilient.lean
    complete
    theorem CryptBoolean.walshTransform_partialSpreadResilientFunction_append
  {r s : ℕ}
  (theta : FABL.F₂Cube r ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField r)
  (g : CryptBoolean.FieldBooleanFunction r)
  (phi : FABL.F₂Cube s →ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField r)
  (phiStar : CryptBoolean.BinaryGaloisField r →ₗ[FABL.𝔽₂] FABL.F₂Cube s)
  (hphiStar :
    ∀ (z : CryptBoolean.BinaryGaloisField r) (y : FABL.F₂Cube s),
      FABL.f₂DotProduct (phiStar z) y =
        (CryptBoolean.absoluteTrace r) (z * phi y))
  (a : CryptBoolean.BinaryGaloisField r) (b : FABL.F₂Cube s)
  (hdenom : ∀ (y : FABL.F₂Cube s), a + phi y ≠ 0) (u : FABL.F₂Cube r)
  (v : FABL.F₂Cube s) (z : CryptBoolean.BinaryGaloisField r)
  (hz :
    ∀ (x : FABL.F₂Cube r),
      FABL.f₂DotProduct u x =
        (CryptBoolean.absoluteTrace r) (z * theta x)) :
  CryptBoolean.walshTransform
      (CryptBoolean.partialSpreadResilientFunction theta g phi a b)
      (Fin.append u v) =
    ∑ t,
      CryptBoolean.bitSignInt
          (g t + (CryptBoolean.absoluteTrace r) (z * a * t)) *
        ∑ y,
          CryptBoolean.bitSignInt
            (FABL.f₂DotProduct (phiStar (z * t) + b + v) y)
    theorem CryptBoolean.walshTransform_partialSpreadResilientFunction_append
  {r s : ℕ}
  (theta :
    FABL.F₂Cube r ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField r)
  (g :
    CryptBoolean.FieldBooleanFunction r)
  (phi :
    FABL.F₂Cube s →ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField r)
  (phiStar :
    CryptBoolean.BinaryGaloisField
        r →ₗ[FABL.𝔽₂]
      FABL.F₂Cube s)
  (hphiStar :
    ∀
      (z :
        CryptBoolean.BinaryGaloisField r)
      (y : FABL.F₂Cube s),
      FABL.f₂DotProduct (phiStar z) y =
        (CryptBoolean.absoluteTrace r)
          (z * phi y))
  (a : CryptBoolean.BinaryGaloisField r)
  (b : FABL.F₂Cube s)
  (hdenom :
    ∀ (y : FABL.F₂Cube s), a + phi y ≠ 0)
  (u : FABL.F₂Cube r) (v : FABL.F₂Cube s)
  (z : CryptBoolean.BinaryGaloisField r)
  (hz :
    ∀ (x : FABL.F₂Cube r),
      FABL.f₂DotProduct u x =
        (CryptBoolean.absoluteTrace r)
          (z * theta x)) :
  CryptBoolean.walshTransform
      (CryptBoolean.partialSpreadResilientFunction
        theta g phi a b)
      (Fin.append u v) =
    ∑ t,
      CryptBoolean.bitSignInt
          (g t +
            (CryptBoolean.absoluteTrace r)
              (z * a * t)) *
        ∑ y,
          CryptBoolean.bitSignInt
            (FABL.f₂DotProduct
              (phiStar (z * t) + b + v) y)
    The Walsh transform of the partial-spread quotient construction is a sum
of cube characters indexed by the quotient variable.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/PartialSpreadResilient.lean
    complete
    theorem CryptBoolean.isResilient_partialSpreadResilientFunction {r s k : ℕ}
  (theta : FABL.F₂Cube r ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField r)
  (g : CryptBoolean.FieldBooleanFunction r)
  (phi : FABL.F₂Cube s →ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField r)
  (phiStar : CryptBoolean.BinaryGaloisField r →ₗ[FABL.𝔽₂] FABL.F₂Cube s)
  (hphiStar :
    ∀ (z : CryptBoolean.BinaryGaloisField r) (y : FABL.F₂Cube s),
      FABL.f₂DotProduct (phiStar z) y =
        (CryptBoolean.absoluteTrace r) (z * phi y))
  (a : CryptBoolean.BinaryGaloisField r) (b : FABL.F₂Cube s)
  (hdenom : ∀ (y : FABL.F₂Cube s), a + phi y ≠ 0)
  (hweight :
    ∀ (z : CryptBoolean.BinaryGaloisField r),
      k < (FABL.f₂Support (phiStar z + b)).card) :
  CryptBoolean.IsResilient k
    (CryptBoolean.partialSpreadResilientFunction theta g phi a b)
    theorem CryptBoolean.isResilient_partialSpreadResilientFunction
  {r s k : ℕ}
  (theta :
    FABL.F₂Cube r ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField r)
  (g :
    CryptBoolean.FieldBooleanFunction r)
  (phi :
    FABL.F₂Cube s →ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField r)
  (phiStar :
    CryptBoolean.BinaryGaloisField
        r →ₗ[FABL.𝔽₂]
      FABL.F₂Cube s)
  (hphiStar :
    ∀
      (z :
        CryptBoolean.BinaryGaloisField r)
      (y : FABL.F₂Cube s),
      FABL.f₂DotProduct (phiStar z) y =
        (CryptBoolean.absoluteTrace r)
          (z * phi y))
  (a : CryptBoolean.BinaryGaloisField r)
  (b : FABL.F₂Cube s)
  (hdenom :
    ∀ (y : FABL.F₂Cube s), a + phi y ≠ 0)
  (hweight :
    ∀
      (z :
        CryptBoolean.BinaryGaloisField r),
      k <
        (FABL.f₂Support
            (phiStar z + b)).card) :
  CryptBoolean.IsResilient k
    (CryptBoolean.partialSpreadResilientFunction
      theta g phi a b)
    Carlet Relation (63): if every adjoint translate lies outside the
weight-`k` ball, the partial-spread quotient construction is `k`-resilient.
The avoidance hypothesis itself implies `k < s`, so separate positivity
hypotheses on the parameters are unnecessary.
Proposition6.3.10
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Theorem 1.7.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 6.3.11
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-7proposition-33dobbertinwalsh-transformpage-121fidelity-exact

Proposition 33 (Carlet, Relation (64), p. 121). Let n>0 be even. Let f:V_{n/2}\times V_{n/2}\to\mathbb F_2 be bent and satisfy f(x,0)=0 for every x. Let g:V_{n/2}\to\mathbb F_2 be balanced and define h(x,y)=f(x,y)\oplus\delta_0(y)g(x). Then W_h(u,v)= \begin{cases} 0,&u=0,\\ W_f(u,v)+W_g(u),&u\ne0. \end{cases} In particular, h is balanced.

Lean code for Proposition6.3.10●9 declarations
  • defdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    def CryptBoolean.dobbertinConstruction {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + m)
    def CryptBoolean.dobbertinConstruction {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + m)
    Dobbertin's modification replaces the zero-second-block restriction of
`f` by `g`.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.dobbertinConstruction_append {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (x y : FABL.F₂Cube m) :
  CryptBoolean.dobbertinConstruction f g (Fin.append x y) =
    f (Fin.append x y) + if y = 0 then g x else 0
    theorem CryptBoolean.dobbertinConstruction_append
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (x y : FABL.F₂Cube m) :
  CryptBoolean.dobbertinConstruction f g
      (Fin.append x y) =
    f (Fin.append x y) +
      if y = 0 then g x else 0
    Evaluation of Dobbertin's construction on the two coordinate blocks.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.walshTransform_dobbertinConstruction_general {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (u v : FABL.F₂Cube m) :
  CryptBoolean.walshTransform (CryptBoolean.dobbertinConstruction f g)
      (Fin.append u v) =
    CryptBoolean.walshTransform f (Fin.append u v) +
        CryptBoolean.walshTransform g u -
      CryptBoolean.walshTransform 0 u
    theorem CryptBoolean.walshTransform_dobbertinConstruction_general
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (u v : FABL.F₂Cube m) :
  CryptBoolean.walshTransform
      (CryptBoolean.dobbertinConstruction
        f g)
      (Fin.append u v) =
    CryptBoolean.walshTransform f
          (Fin.append u v) +
        CryptBoolean.walshTransform g u -
      CryptBoolean.walshTransform 0 u
    Before using bentness and balancedness, the exact spectral correction is
the source Walsh coefficient plus the mask coefficient minus the zero-flat
character sum.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.walshTransform_dobbertinConstruction {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (u v : FABL.F₂Cube m) :
  CryptBoolean.walshTransform (CryptBoolean.dobbertinConstruction f g)
      (Fin.append u v) =
    CryptBoolean.walshTransform f (Fin.append u v) +
        CryptBoolean.walshTransform g u -
      if u = 0 then 2 ^ m else 0
    theorem CryptBoolean.walshTransform_dobbertinConstruction
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (u v : FABL.F₂Cube m) :
  CryptBoolean.walshTransform
      (CryptBoolean.dobbertinConstruction
        f g)
      (Fin.append u v) =
    CryptBoolean.walshTransform f
          (Fin.append u v) +
        CryptBoolean.walshTransform g u -
      if u = 0 then 2 ^ m else 0
    The exact correction formula with the zero-flat character sum evaluated.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.walshTransform_zeroFirstBlock_eq_two_pow_of_isBent {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (v : FABL.F₂Cube m) :
  CryptBoolean.walshTransform f (Fin.append 0 v) = 2 ^ m
    theorem CryptBoolean.walshTransform_zeroFirstBlock_eq_two_pow_of_isBent
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (v : FABL.F₂Cube m) :
  CryptBoolean.walshTransform f
      (Fin.append 0 v) =
    2 ^ m
    A bent function that vanishes on the zero second-block flat has positive
Walsh coefficient `2^m` on every frequency perpendicular to that flat.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.walshTransform_dobbertinConstruction_of_isBent_of_isBalanced
  {m : ℕ} (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) (u v : FABL.F₂Cube m) :
  CryptBoolean.walshTransform (CryptBoolean.dobbertinConstruction f g)
      (Fin.append u v) =
    if u = 0 then 0
    else
      CryptBoolean.walshTransform f (Fin.append u v) +
        CryptBoolean.walshTransform g u
    theorem CryptBoolean.walshTransform_dobbertinConstruction_of_isBent_of_isBalanced
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g)
  (u v : FABL.F₂Cube m) :
  CryptBoolean.walshTransform
      (CryptBoolean.dobbertinConstruction
        f g)
      (Fin.append u v) =
    if u = 0 then 0
    else
      CryptBoolean.walshTransform f
          (Fin.append u v) +
        CryptBoolean.walshTransform g u
    Carlet Proposition 33 and Relation (64): the modified spectrum vanishes
when the first frequency block is zero and otherwise is the sum of the bent
and mask spectra.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.walshTransform_dobbertinConstruction_zeroFirstBlock {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) (v : FABL.F₂Cube m) :
  CryptBoolean.walshTransform (CryptBoolean.dobbertinConstruction f g)
      (Fin.append 0 v) =
    0
    theorem CryptBoolean.walshTransform_dobbertinConstruction_zeroFirstBlock
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g)
  (v : FABL.F₂Cube m) :
  CryptBoolean.walshTransform
      (CryptBoolean.dobbertinConstruction
        f g)
      (Fin.append 0 v) =
    0
    Zero-first-block branch of Dobbertin's Walsh spectrum.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.walshTransform_dobbertinConstruction_ne_zeroFirstBlock
  {m : ℕ} (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) (u v : FABL.F₂Cube m) (hu : u ≠ 0) :
  CryptBoolean.walshTransform (CryptBoolean.dobbertinConstruction f g)
      (Fin.append u v) =
    CryptBoolean.walshTransform f (Fin.append u v) +
      CryptBoolean.walshTransform g u
    theorem CryptBoolean.walshTransform_dobbertinConstruction_ne_zeroFirstBlock
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g)
  (u v : FABL.F₂Cube m) (hu : u ≠ 0) :
  CryptBoolean.walshTransform
      (CryptBoolean.dobbertinConstruction
        f g)
      (Fin.append u v) =
    CryptBoolean.walshTransform f
        (Fin.append u v) +
      CryptBoolean.walshTransform g u
    Nonzero-first-block branch of Dobbertin's Walsh spectrum.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.isBalanced_dobbertinConstruction {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.IsBalanced (CryptBoolean.dobbertinConstruction f g)
    theorem CryptBoolean.isBalanced_dobbertinConstruction
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.IsBalanced
    (CryptBoolean.dobbertinConstruction f
      g)
    Dobbertin's modification is balanced.
Theorem6.3.11
Group: Chapter 6: Resilient functions (38)
Group member previews
Preview
Theorem 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 3.2.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-7dobbertinnonlinearitypages-121-122fidelity-corrected-dimension-range

Dobbertin's nonlinearity bound (Carlet, pp. 121--122). Under the hypotheses of Proposition 33, \operatorname{nl}(h) \ge \operatorname{nl}(f)+\operatorname{nl}(g)-2^{n/2-1} =2^{n-1}-2^{n/2}+\operatorname{nl}(g). If n\ge4, this construction cannot produce a positively resilient function.

Lean code for Theorem6.3.11●6 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.maxWalshMagnitude_dobbertinConstruction_le {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.dobbertinConstruction f g) ≤
    2 ^ m + CryptBoolean.maxWalshMagnitude g
    theorem CryptBoolean.maxWalshMagnitude_dobbertinConstruction_le
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.dobbertinConstruction
        f g) ≤
    2 ^ m +
      CryptBoolean.maxWalshMagnitude g
    The spectral triangle inequality behind Dobbertin's nonlinearity bound.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.nonlinearity_dobbertinConstruction_add_le {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (hm : 0 < m)
  (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.nonlinearity f + CryptBoolean.nonlinearity g ≤
    CryptBoolean.nonlinearity (CryptBoolean.dobbertinConstruction f g) +
      2 ^ (m - 1)
    theorem CryptBoolean.nonlinearity_dobbertinConstruction_add_le
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hm : 0 < m)
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.nonlinearity f +
      CryptBoolean.nonlinearity g ≤
    CryptBoolean.nonlinearity
        (CryptBoolean.dobbertinConstruction
          f g) +
      2 ^ (m - 1)
    Additive form of Dobbertin's nonlinearity bound.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.nonlinearity_dobbertinConstruction_lowerBound {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (hm : 0 < m)
  (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.nonlinearity f + CryptBoolean.nonlinearity g -
      2 ^ (m - 1) ≤
    CryptBoolean.nonlinearity (CryptBoolean.dobbertinConstruction f g)
    theorem CryptBoolean.nonlinearity_dobbertinConstruction_lowerBound
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hm : 0 < m)
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.nonlinearity f +
        CryptBoolean.nonlinearity g -
      2 ^ (m - 1) ≤
    CryptBoolean.nonlinearity
      (CryptBoolean.dobbertinConstruction
        f g)
    Dobbertin's nonlinearity lower bound in Carlet's subtraction form.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.nonlinearity_dobbertinConstruction_boundTerm_eq {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (hm : 0 < m)
  (hf : CryptBoolean.IsBent f) :
  CryptBoolean.nonlinearity f + CryptBoolean.nonlinearity g -
      2 ^ (m - 1) =
    2 ^ (m + m - 1) - 2 ^ m + CryptBoolean.nonlinearity g
    theorem CryptBoolean.nonlinearity_dobbertinConstruction_boundTerm_eq
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hm : 0 < m)
  (hf : CryptBoolean.IsBent f) :
  CryptBoolean.nonlinearity f +
        CryptBoolean.nonlinearity g -
      2 ^ (m - 1) =
    2 ^ (m + m - 1) - 2 ^ m +
      CryptBoolean.nonlinearity g
    For a bent source, Carlet's two forms of the Dobbertin lower-bound term
agree.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.nonlinearity_dobbertinConstruction_lowerBound_source
  {m : ℕ} (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (hm : 0 < m)
  (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) :
  2 ^ (m + m - 1) - 2 ^ m + CryptBoolean.nonlinearity g ≤
    CryptBoolean.nonlinearity (CryptBoolean.dobbertinConstruction f g)
    theorem CryptBoolean.nonlinearity_dobbertinConstruction_lowerBound_source
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hm : 0 < m)
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) :
  2 ^ (m + m - 1) - 2 ^ m +
      CryptBoolean.nonlinearity g ≤
    CryptBoolean.nonlinearity
      (CryptBoolean.dobbertinConstruction
        f g)
    Source-normalized form of Dobbertin's nonlinearity lower bound.
  • theoremdefined in CryptBoolean/Carlet/Chapter07/Dobbertin.lean
    complete
    theorem CryptBoolean.not_isResilient_dobbertinConstruction_of_pos {m k : ℕ}
  (f : CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m) (hm : 2 ≤ m)
  (hf : CryptBoolean.IsBent f)
  (hflat : ∀ (x : FABL.F₂Cube m), f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g) (hk : 0 < k) :
  ¬CryptBoolean.IsResilient k (CryptBoolean.dobbertinConstruction f g)
    theorem CryptBoolean.not_isResilient_dobbertinConstruction_of_pos
  {m k : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + m))
  (g : CryptBoolean.BooleanFunction m)
  (hm : 2 ≤ m)
  (hf : CryptBoolean.IsBent f)
  (hflat :
    ∀ (x : FABL.F₂Cube m),
      f (Fin.append x 0) = 0)
  (hg : CryptBoolean.IsBalanced g)
  (hk : 0 < k) :
  ¬CryptBoolean.IsResilient k
      (CryptBoolean.dobbertinConstruction
        f g)
    In ambient dimension at least four, Dobbertin's construction is not
resilient of any positive order.