Cryptographic Boolean Functions in Lean

7.1. Propagation criteria and Walsh analysis🔗

Theorem7.1.1
Group: Chapter 7: Strict avalanche and propagation criteria (13)
Group member previews
Preview
Theorem 7.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 3.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-8propagation-criterionbent-functionseven-dimensionpage-131fidelity-explicit-valid-dimension-range

Extremal propagation in even dimension (Carlet, p. 131). Let n\ge4 be even and let f:V_n\to\mathbb F_2. Then f\text{ satisfies }\mathrm{PC}(n-2) \quad\Longleftrightarrow\quad f\text{ is bent}. Equivalently, \mathrm{PC}(n-2) already implies \mathrm{PC}(n). Consequently, no balanced n-variable function satisfies \mathrm{PC}(n-2).

Lean code for Theorem7.1.1●4 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.isBent_of_satisfiesPropagationCriterion_pred_two_of_even
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : 4 ≤ n)
  (heven : Even n)
  (hpc : CryptBoolean.SatisfiesPropagationCriterion (n - 2) f) :
  CryptBoolean.IsBent f
    theorem CryptBoolean.isBent_of_satisfiesPropagationCriterion_pred_two_of_even
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 4 ≤ n) (heven : Even n)
  (hpc :
    CryptBoolean.SatisfiesPropagationCriterion
      (n - 2) f) :
  CryptBoolean.IsBent f
    In even dimension at least four, `PC(n-2)` already forces bentness.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.satisfiesPropagationCriterion_pred_two_iff_isBent_of_even
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : 4 ≤ n)
  (heven : Even n) :
  CryptBoolean.SatisfiesPropagationCriterion (n - 2) f ↔
    CryptBoolean.IsBent f
    theorem CryptBoolean.satisfiesPropagationCriterion_pred_two_iff_isBent_of_even
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 4 ≤ n) (heven : Even n) :
  CryptBoolean.SatisfiesPropagationCriterion
      (n - 2) f ↔
    CryptBoolean.IsBent f
    In even dimension at least four, `PC(n-2)` is equivalent to bentness.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.satisfiesPropagationCriterion_dimension_of_pred_two_of_even
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : 4 ≤ n)
  (heven : Even n)
  (hf : CryptBoolean.SatisfiesPropagationCriterion (n - 2) f) :
  CryptBoolean.SatisfiesPropagationCriterion n f
    theorem CryptBoolean.satisfiesPropagationCriterion_dimension_of_pred_two_of_even
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 4 ≤ n) (heven : Even n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterion
      (n - 2) f) :
  CryptBoolean.SatisfiesPropagationCriterion
    n f
    In even dimension at least four, `PC(n-2)` upgrades to `PC(n)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.not_satisfiesPropagationCriterion_pred_two_of_even_of_isBalanced
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : 4 ≤ n)
  (heven : Even n) (hf : CryptBoolean.IsBalanced f) :
  ¬CryptBoolean.SatisfiesPropagationCriterion (n - 2) f
    theorem CryptBoolean.not_satisfiesPropagationCriterion_pred_two_of_even_of_isBalanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 4 ≤ n) (heven : Even n)
  (hf : CryptBoolean.IsBalanced f) :
  ¬CryptBoolean.SatisfiesPropagationCriterion
      (n - 2) f
    No balanced Boolean function in even dimension at least four satisfies `PC(n-2)`.
Theorem7.1.2
Group: Chapter 7: Strict avalanche and propagation criteria (13)
Group member previews
Preview
Theorem 7.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.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-8propagation-criterionclassificationodd-dimensionpage-131fidelity-reviewed-endpoint

Extremal propagation in odd dimension (Carlet, p. 131). Let n\ge3 be odd and let f:V_n\to\mathbb F_2. Then f satisfies \mathrm{PC}(n-1) if and only if there exist a bent function g:V_{n-1}\to\mathbb F_2 and an affine function h:V_n\to\mathbb F_2 such that f(x_1,\ldots,x_n)= g(x_1\oplus x_n,\ldots,x_{n-1}\oplus x_n)\oplus h(x_1,\ldots,x_n).

Lean code for Theorem7.1.2●4 declarations
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.oddDiagonalProjection (m : ℕ) :
  FABL.F₂Cube (m + 1) →ₗ[FABL.𝔽₂] FABL.F₂Cube m
    def CryptBoolean.oddDiagonalProjection
  (m : ℕ) :
  FABL.F₂Cube (m + 1) →ₗ[FABL.𝔽₂]
    FABL.F₂Cube m
    The diagonal quotient map
`(x₁,…,xₘ,xₘ₊₁) ↦ (x₁+xₘ₊₁,…,xₘ+xₘ₊₁)`.
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.oddDiagonalBentLift {m : ℕ}
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + 1)
    def CryptBoolean.oddDiagonalBentLift {m : ℕ}
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + 1)
    Pulling a Boolean function back along the odd diagonal quotient.
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.HasOddDiagonalBentNormalForm {m : ℕ}
  (f : CryptBoolean.BooleanFunction (m + 1)) : Prop
    def CryptBoolean.HasOddDiagonalBentNormalForm
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction
      (m + 1)) :
  Prop
    The source-facing diagonal bent normal form in odd dimension.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.satisfiesPropagationCriterion_pred_one_iff_hasOddDiagonalBentNormalForm
  (k : ℕ) (hk : 1 ≤ k) (f : CryptBoolean.BooleanFunction (2 * k + 1)) :
  CryptBoolean.SatisfiesPropagationCriterion (2 * k) f ↔
    CryptBoolean.HasOddDiagonalBentNormalForm f
    theorem CryptBoolean.satisfiesPropagationCriterion_pred_one_iff_hasOddDiagonalBentNormalForm
  (k : ℕ) (hk : 1 ≤ k)
  (f :
    CryptBoolean.BooleanFunction
      (2 * k + 1)) :
  CryptBoolean.SatisfiesPropagationCriterion
      (2 * k) f ↔
    CryptBoolean.HasOddDiagonalBentNormalForm
      f
    In odd dimension at least three, `PC(n-1)` is exactly the diagonal
pullback of a bent function, up to an arbitrary affine summand.
Theorem7.1.3
Group: Chapter 7: Strict avalanche and propagation criteria (13)
Group member previews
Preview
Theorem 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 3.6.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-8propagation-criterionclassificationlinear-structuresodd-dimensionpage-131fidelity-primary-coordinate-forms-restored

The \mathrm{PC}(n-2) classification in odd dimension (Carlet, p. 131). Let n\ge3 be odd. A function f:V_n\to\mathbb F_2 satisfies \mathrm{PC}(n-2) if and only if it is an affine function plus a bent function on one of the following three quotient-coordinate systems:

  • y_j=x_j\oplus x_n for every 1\le j\le n-1;

  • for one i, y_i=x_i and y_j=x_j\oplus x_n for j\ne i;

  • y_j=x_j\oplus x_{n-1} for 1\le j\le n-2, and y_{n-1}=x_n.

Equivalently, there exists a nonzero a\in V_n with w_H(a)\ge n-1 such that D_af is constant, while D_bf is balanced for every nonzero b\ne a. Thus f has exactly one nonzero linear structure, of weight n-1 or n.

Lean code for Theorem7.1.3●24 declarations
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.coordinateDirection {n : ℕ} (i : Fin n) : FABL.F₂Cube n
    def CryptBoolean.coordinateDirection {n : ℕ}
  (i : Fin n) : FABL.F₂Cube n
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.HasUniqueHighWeightLinearStructure {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.HasUniqueHighWeightLinearStructure
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    A Boolean function has one distinguished nonzero linear structure of
weight at least `n-1`, and every other nonzero derivative is balanced.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.satisfiesPropagationCriterion_pred_two_iff_hasUniqueHighWeightLinearStructure
  (k : ℕ) (hk : 1 ≤ k) (f : CryptBoolean.BooleanFunction (2 * k + 1)) :
  CryptBoolean.SatisfiesPropagationCriterion (2 * k - 1) f ↔
    CryptBoolean.HasUniqueHighWeightLinearStructure f
    theorem CryptBoolean.satisfiesPropagationCriterion_pred_two_iff_hasUniqueHighWeightLinearStructure
  (k : ℕ) (hk : 1 ≤ k)
  (f :
    CryptBoolean.BooleanFunction
      (2 * k + 1)) :
  CryptBoolean.SatisfiesPropagationCriterion
      (2 * k - 1) f ↔
    CryptBoolean.HasUniqueHighWeightLinearStructure
      f
    In odd dimension at least three, `PC(n-2)` is equivalent to having one
high-weight nonzero linear structure and balanced derivatives in every other
nonzero direction.
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.puncturedDiagonalShearLinearMap (m : ℕ) (i : Fin m) :
  FABL.F₂Cube (m + 1) →ₗ[FABL.𝔽₂] FABL.F₂Cube (m + 1)
    def CryptBoolean.puncturedDiagonalShearLinearMap
  (m : ℕ) (i : Fin m) :
  FABL.F₂Cube (m + 1) →ₗ[FABL.𝔽₂]
    FABL.F₂Cube (m + 1)
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.puncturedDiagonalShearLinearMap_involutive (m : ℕ)
  (i : Fin m) :
  Function.Involutive
    ⇑(CryptBoolean.puncturedDiagonalShearLinearMap m i)
    theorem CryptBoolean.puncturedDiagonalShearLinearMap_involutive
  (m : ℕ) (i : Fin m) :
  Function.Involutive
    ⇑(CryptBoolean.puncturedDiagonalShearLinearMap
        m i)
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.puncturedDiagonalShearLinearEquiv (m : ℕ) (i : Fin m) :
  FABL.F₂Cube (m + 1) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube (m + 1)
    def CryptBoolean.puncturedDiagonalShearLinearEquiv
  (m : ℕ) (i : Fin m) :
  FABL.F₂Cube (m + 1) ≃ₗ[FABL.𝔽₂]
    FABL.F₂Cube (m + 1)
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.oddPuncturedDiagonalProjection (m : ℕ) (i : Fin m) :
  FABL.F₂Cube (m + 1) →ₗ[FABL.𝔽₂] FABL.F₂Cube m
    def CryptBoolean.oddPuncturedDiagonalProjection
  (m : ℕ) (i : Fin m) :
  FABL.F₂Cube (m + 1) →ₗ[FABL.𝔽₂]
    FABL.F₂Cube m
    The second odd-dimensional quotient family: one of the first coordinates
is retained and every other first coordinate is added to the last one.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.oddPuncturedDiagonalProjection_apply_same (m : ℕ)
  (i : Fin m) (x : FABL.F₂Cube (m + 1)) :
  (CryptBoolean.oddPuncturedDiagonalProjection m i) x i = x i.castSucc
    theorem CryptBoolean.oddPuncturedDiagonalProjection_apply_same
  (m : ℕ) (i : Fin m)
  (x : FABL.F₂Cube (m + 1)) :
  (CryptBoolean.oddPuncturedDiagonalProjection
        m i)
      x i =
    x i.castSucc
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.oddPuncturedDiagonalProjection_apply_of_ne (m : ℕ)
  (i j : Fin m) (hji : j ≠ i) (x : FABL.F₂Cube (m + 1)) :
  (CryptBoolean.oddPuncturedDiagonalProjection m i) x j =
    x j.castSucc + x (Fin.last m)
    theorem CryptBoolean.oddPuncturedDiagonalProjection_apply_of_ne
  (m : ℕ) (i j : Fin m) (hji : j ≠ i)
  (x : FABL.F₂Cube (m + 1)) :
  (CryptBoolean.oddPuncturedDiagonalProjection
        m i)
      x j =
    x j.castSucc + x (Fin.last m)
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.coordinateSwapLinearEquiv {n : ℕ} (i j : Fin n) :
  FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] FABL.F₂Cube n
    def CryptBoolean.coordinateSwapLinearEquiv
  {n : ℕ} (i j : Fin n) :
  FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] FABL.F₂Cube n
    Reindexing binary-cube coordinates by a transposition.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.coordinateSwapLinearEquiv_apply {n : ℕ} (i j : Fin n)
  (x : FABL.F₂Cube n) (t : Fin n) :
  (CryptBoolean.coordinateSwapLinearEquiv i j) x t =
    x ((Equiv.swap i j) t)
    theorem CryptBoolean.coordinateSwapLinearEquiv_apply
  {n : ℕ} (i j : Fin n)
  (x : FABL.F₂Cube n) (t : Fin n) :
  (CryptBoolean.coordinateSwapLinearEquiv
        i j)
      x t =
    x ((Equiv.swap i j) t)
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.oddTerminalDiagonalProjectionAt (m : ℕ) (i : Fin m) :
  FABL.F₂Cube (m + 1) →ₗ[FABL.𝔽₂] FABL.F₂Cube m
    def CryptBoolean.oddTerminalDiagonalProjectionAt
  (m : ℕ) (i : Fin m) :
  FABL.F₂Cube (m + 1) →ₗ[FABL.𝔽₂]
    FABL.F₂Cube m
    A terminal-coordinate quotient with a designated retained output
coordinate.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.oddTerminalDiagonalProjectionAt_apply_same (m : ℕ)
  (i : Fin m) (x : FABL.F₂Cube (m + 1)) :
  (CryptBoolean.oddTerminalDiagonalProjectionAt m i) x i =
    x (Fin.last m)
    theorem CryptBoolean.oddTerminalDiagonalProjectionAt_apply_same
  (m : ℕ) (i : Fin m)
  (x : FABL.F₂Cube (m + 1)) :
  (CryptBoolean.oddTerminalDiagonalProjectionAt
        m i)
      x i =
    x (Fin.last m)
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.oddTerminalDiagonalProjectionAt_apply_of_ne (m : ℕ)
  (i j : Fin m) (hji : j ≠ i) (x : FABL.F₂Cube (m + 1)) :
  (CryptBoolean.oddTerminalDiagonalProjectionAt m i) x j =
    x j.castSucc + x i.castSucc
    theorem CryptBoolean.oddTerminalDiagonalProjectionAt_apply_of_ne
  (m : ℕ) (i j : Fin m) (hji : j ≠ i)
  (x : FABL.F₂Cube (m + 1)) :
  (CryptBoolean.oddTerminalDiagonalProjectionAt
        m i)
      x j =
    x j.castSucc + x i.castSucc
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.oddTerminalDiagonalProjection (r : ℕ) :
  FABL.F₂Cube (r + 2) →ₗ[FABL.𝔽₂] FABL.F₂Cube (r + 1)
    def CryptBoolean.oddTerminalDiagonalProjection
  (r : ℕ) :
  FABL.F₂Cube (r + 2) →ₗ[FABL.𝔽₂]
    FABL.F₂Cube (r + 1)
    The third odd-dimensional quotient family: the first `r` coordinates
are added to the next coordinate, while the final coordinate is retained.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.oddTerminalDiagonalProjection_apply_castSucc (r : ℕ)
  (x : FABL.F₂Cube (r + 2)) (j : Fin r) :
  (CryptBoolean.oddTerminalDiagonalProjection r) x j.castSucc =
    x j.castSucc.castSucc + x (Fin.last r).castSucc
    theorem CryptBoolean.oddTerminalDiagonalProjection_apply_castSucc
  (r : ℕ) (x : FABL.F₂Cube (r + 2))
  (j : Fin r) :
  (CryptBoolean.oddTerminalDiagonalProjection
        r)
      x j.castSucc =
    x j.castSucc.castSucc +
      x (Fin.last r).castSucc
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.oddTerminalDiagonalProjection_apply_last (r : ℕ)
  (x : FABL.F₂Cube (r + 2)) :
  (CryptBoolean.oddTerminalDiagonalProjection r) x (Fin.last r) =
    x (Fin.last (r + 1))
    theorem CryptBoolean.oddTerminalDiagonalProjection_apply_last
  (r : ℕ) (x : FABL.F₂Cube (r + 2)) :
  (CryptBoolean.oddTerminalDiagonalProjection
        r)
      x (Fin.last r) =
    x (Fin.last (r + 1))
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.oddPuncturedDiagonalBentLift {m : ℕ} (i : Fin m)
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + 1)
    def CryptBoolean.oddPuncturedDiagonalBentLift
  {m : ℕ} (i : Fin m)
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + 1)
    Pullback along the second explicit odd-dimensional quotient.
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.oddTerminalDiagonalBentLiftAt {m : ℕ} (i : Fin m)
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + 1)
    def CryptBoolean.oddTerminalDiagonalBentLiftAt
  {m : ℕ} (i : Fin m)
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + 1)
    Pullback along a terminal-coordinate quotient.
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.oddPenultimateIndex (k : ℕ) (hk : 1 ≤ k) : Fin (2 * k)
    def CryptBoolean.oddPenultimateIndex (k : ℕ)
  (hk : 1 ≤ k) : Fin (2 * k)
    The penultimate coordinate among `2k+1` input coordinates.
  • defdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    def CryptBoolean.HasOddPredTwoBentNormalForm (k : ℕ) (hk : 1 ≤ k)
  (f : CryptBoolean.BooleanFunction (2 * k + 1)) : Prop
    def CryptBoolean.HasOddPredTwoBentNormalForm
  (k : ℕ) (hk : 1 ≤ k)
  (f :
    CryptBoolean.BooleanFunction
      (2 * k + 1)) :
  Prop
    The three source-facing bent quotient normal forms for odd-dimensional
`PC(n-2)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.hasOddPredTwoBentNormalForm_of_satisfiesPropagationCriterion
  (k : ℕ) (hk : 1 ≤ k) (f : CryptBoolean.BooleanFunction (2 * k + 1))
  (hpc : CryptBoolean.SatisfiesPropagationCriterion (2 * k - 1) f) :
  CryptBoolean.HasOddPredTwoBentNormalForm k hk f
    theorem CryptBoolean.hasOddPredTwoBentNormalForm_of_satisfiesPropagationCriterion
  (k : ℕ) (hk : 1 ≤ k)
  (f :
    CryptBoolean.BooleanFunction
      (2 * k + 1))
  (hpc :
    CryptBoolean.SatisfiesPropagationCriterion
      (2 * k - 1) f) :
  CryptBoolean.HasOddPredTwoBentNormalForm
    k hk f
    Every odd-dimensional `PC(n-2)` function has one of the three explicit
bent quotient normal forms.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.satisfiesPropagationCriterion_of_hasOddPredTwoBentNormalForm
  (k : ℕ) (hk : 1 ≤ k) (f : CryptBoolean.BooleanFunction (2 * k + 1))
  (hform : CryptBoolean.HasOddPredTwoBentNormalForm k hk f) :
  CryptBoolean.SatisfiesPropagationCriterion (2 * k - 1) f
    theorem CryptBoolean.satisfiesPropagationCriterion_of_hasOddPredTwoBentNormalForm
  (k : ℕ) (hk : 1 ≤ k)
  (f :
    CryptBoolean.BooleanFunction
      (2 * k + 1))
  (hform :
    CryptBoolean.HasOddPredTwoBentNormalForm
      k hk f) :
  CryptBoolean.SatisfiesPropagationCriterion
    (2 * k - 1) f
    Each of the three explicit bent quotient normal forms satisfies
odd-dimensional `PC(n-2)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean
    complete
    theorem CryptBoolean.satisfiesPropagationCriterion_pred_two_iff_hasOddPredTwoBentNormalForm
  (k : ℕ) (hk : 1 ≤ k) (f : CryptBoolean.BooleanFunction (2 * k + 1)) :
  CryptBoolean.SatisfiesPropagationCriterion (2 * k - 1) f ↔
    CryptBoolean.HasOddPredTwoBentNormalForm k hk f
    theorem CryptBoolean.satisfiesPropagationCriterion_pred_two_iff_hasOddPredTwoBentNormalForm
  (k : ℕ) (hk : 1 ≤ k)
  (f :
    CryptBoolean.BooleanFunction
      (2 * k + 1)) :
  CryptBoolean.SatisfiesPropagationCriterion
      (2 * k - 1) f ↔
    CryptBoolean.HasOddPredTwoBentNormalForm
      k hk f
    The three explicit bent quotient normal forms classify
odd-dimensional `PC(n-2)`.
Theorem7.1.4
Group: Chapter 7: Strict avalanche and propagation criteria (13)
Group member previews
Preview
Theorem 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-8propagation-criterionalgebraic-degreepage-131fidelity-explicit-valid-dimension-range

Algebraic degree under a propagation criterion (Carlet, p. 131). Let n\ge3, 1\le \ell<n, and f:V_n\to\mathbb F_2. If f satisfies \mathrm{PC}(\ell), then \deg(f)\le n-1.

Lean code for Theorem7.1.4●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter08/AlgebraicDegree.lean
    complete
    theorem CryptBoolean.differenceMultiplicity_even {n : ℕ}
  (D : Finset (FABL.F₂Cube n)) (a : FABL.F₂Cube n) (ha : a ≠ 0) :
  Even (CryptBoolean.differenceMultiplicity D a)
    theorem CryptBoolean.differenceMultiplicity_even
  {n : ℕ} (D : Finset (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) (ha : a ≠ 0) :
  Even
    (CryptBoolean.differenceMultiplicity D
      a)
    Every nonzero difference occurs an even number of times inside a subset of
the binary cube.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/AlgebraicDegree.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_le_pred_of_satisfiesPropagationCriterion
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ) (hn : 3 ≤ n)
  (hl : 1 ≤ l) (_hlt : l < n)
  (hpc : CryptBoolean.SatisfiesPropagationCriterion l f) :
  FABL.functionAlgebraicDegree f ≤ n - 1
    theorem CryptBoolean.functionAlgebraicDegree_le_pred_of_satisfiesPropagationCriterion
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ) (hn : 3 ≤ n) (hl : 1 ≤ l)
  (_hlt : l < n)
  (hpc :
    CryptBoolean.SatisfiesPropagationCriterion
      l f) :
  FABL.functionAlgebraicDegree f ≤ n - 1
    Carlet Section 8.1: a Boolean function satisfying a nontrivial `PC(l)`
in dimension at least three has algebraic degree at most `n-1`.
Theorem7.1.5
Group: Chapter 7: Strict avalanche and propagation criteria (13)
Group member previews
Preview
Theorem 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Corollary 1.8.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-8propagation-criterionnonlinearitywalsh-transformpage-131fidelity-exact

Nonlinearity from a propagating subspace (Carlet, p. 131). Let F\le V_n have dimension \ell, and assume that D_af is balanced for every nonzero a\in F. Then, for every u\in V_n, W_f(u)^2\le 2^{2n-\ell} and \operatorname{nl}(f)\ge 2^{n-1}-2^{n-\ell/2-1}. Consequently, the same bounds hold whenever 0\le\ell\le n and f satisfies \mathrm{PC}(\ell).

Lean code for Theorem7.1.5●4 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter08/PropagationNonlinearity.lean
    complete
    theorem CryptBoolean.walshTransform_sq_le_of_balanced_derivatives_on_subspace
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (l : ℕ)
  (hfinrank : Module.finrank FABL.𝔽₂ ↥F = l)
  (hbalanced :
    ∀ (a : ↥F),
      a ≠ 0 → CryptBoolean.IsBalanced (FABL.booleanDerivative f ↑a))
  (u : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f u) ^ 2 ≤ 2 ^ (2 * n - l)
    theorem CryptBoolean.walshTransform_sq_le_of_balanced_derivatives_on_subspace
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (l : ℕ)
  (hfinrank :
    Module.finrank FABL.𝔽₂ ↥F = l)
  (hbalanced :
    ∀ (a : ↥F),
      a ≠ 0 →
        CryptBoolean.IsBalanced
          (FABL.booleanDerivative f ↑a))
  (u : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f u) ^ 2 ≤
    2 ^ (2 * n - l)
    A propagating `l`-dimensional subspace bounds every squared raw Walsh
coefficient by `2^(2n-l)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/PropagationNonlinearity.lean
    complete
    theorem CryptBoolean.nonlinearity_lowerBound_of_balanced_derivatives_on_subspace
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (l : ℕ)
  (hfinrank : Module.finrank FABL.𝔽₂ ↥F = l)
  (hbalanced :
    ∀ (a : ↥F),
      a ≠ 0 → CryptBoolean.IsBalanced (FABL.booleanDerivative f ↑a)) :
  2 ^ (↑n - 1) - 2 ^ (↑n - ↑l / 2 - 1) ≤ ↑(CryptBoolean.nonlinearity f)
    theorem CryptBoolean.nonlinearity_lowerBound_of_balanced_derivatives_on_subspace
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (l : ℕ)
  (hfinrank :
    Module.finrank FABL.𝔽₂ ↥F = l)
  (hbalanced :
    ∀ (a : ↥F),
      a ≠ 0 →
        CryptBoolean.IsBalanced
          (FABL.booleanDerivative f ↑a)) :
  2 ^ (↑n - 1) - 2 ^ (↑n - ↑l / 2 - 1) ≤
    ↑(CryptBoolean.nonlinearity f)
    A propagating `l`-dimensional subspace gives Carlet's real-exponent
nonlinearity lower bound.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/PropagationNonlinearity.lean
    complete
    theorem CryptBoolean.walshTransform_sq_le_of_satisfiesPropagationCriterion
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ) (hln : l ≤ n)
  (hpc : CryptBoolean.SatisfiesPropagationCriterion l f)
  (u : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f u) ^ 2 ≤ 2 ^ (2 * n - l)
    theorem CryptBoolean.walshTransform_sq_le_of_satisfiesPropagationCriterion
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ) (hln : l ≤ n)
  (hpc :
    CryptBoolean.SatisfiesPropagationCriterion
      l f)
  (u : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f u) ^ 2 ≤
    2 ^ (2 * n - l)
    `PC(l)` bounds every squared raw Walsh coefficient by `2^(2n-l)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/PropagationNonlinearity.lean
    complete
    theorem CryptBoolean.nonlinearity_lowerBound_of_satisfiesPropagationCriterion
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ) (hln : l ≤ n)
  (hpc : CryptBoolean.SatisfiesPropagationCriterion l f) :
  2 ^ (↑n - 1) - 2 ^ (↑n - ↑l / 2 - 1) ≤ ↑(CryptBoolean.nonlinearity f)
    theorem CryptBoolean.nonlinearity_lowerBound_of_satisfiesPropagationCriterion
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ) (hln : l ≤ n)
  (hpc :
    CryptBoolean.SatisfiesPropagationCriterion
      l f) :
  2 ^ (↑n - 1) - 2 ^ (↑n - ↑l / 2 - 1) ≤
    ↑(CryptBoolean.nonlinearity f)
    Carlet's nonlinearity lower bound for a function satisfying `PC(l)`.
Theorem7.1.6
Group: Chapter 7: Strict avalanche and propagation criteria (13)
Group member previews
Preview
Theorem 7.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 0✓L∃∀N
Tagscarletchapter-8propagation-criterionnonlinearityequalitypage-131fidelity-exact

Parameters for equality in the propagation bound (Carlet, p. 131). Let 1\le\ell\le n, and let f:V_n\to\mathbb F_2 satisfy \mathrm{PC}(\ell). If \operatorname{nl}(f)=2^{n-1}-2^{n-\ell/2-1}, then either n is odd and \ell=n-1, or n is even and \ell=n.

Lean code for Theorem7.1.6●1 theorem
  • theoremdefined in CryptBoolean/Carlet/Chapter08/PropagationNonlinearity.lean
    complete
    theorem CryptBoolean.propagationCriterion_nonlinearity_equality_parameters
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ) (hl : 1 ≤ l)
  (hln : l ≤ n) (hpc : CryptBoolean.SatisfiesPropagationCriterion l f)
  (hequality :
    ↑(CryptBoolean.nonlinearity f) =
      2 ^ (↑n - 1) - 2 ^ (↑n - ↑l / 2 - 1)) :
  Odd n ∧ l = n - 1 ∨ Even n ∧ l = n
    theorem CryptBoolean.propagationCriterion_nonlinearity_equality_parameters
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ) (hl : 1 ≤ l) (hln : l ≤ n)
  (hpc :
    CryptBoolean.SatisfiesPropagationCriterion
      l f)
  (hequality :
    ↑(CryptBoolean.nonlinearity f) =
      2 ^ (↑n - 1) -
        2 ^ (↑n - ↑l / 2 - 1)) :
  Odd n ∧ l = n - 1 ∨ Even n ∧ l = n
    Equality in the propagation nonlinearity bound is possible only at the
odd-dimensional `PC(n-1)` endpoint or the even-dimensional bent endpoint.
Theorem7.1.7
Group: Chapter 7: Strict avalanche and propagation criteria (13)
Group member previews
Preview
Theorem 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.7.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-8propagation-criterionwalsh-transformcharacterizationpage-131fidelity-exact

Wiener--Khintchine characterization (Carlet, p. 131). Let 0\le\ell\le n and f:V_n\to\mathbb F_2. Then f satisfies \mathrm{PC}(\ell) if and only if, for every nonzero a\in V_n with w_H(a)\le\ell, \sum_{u\in V_n}(-1)^{a\cdot u}W_f(u)^2=0.

Lean code for Theorem7.1.7●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter08/WalshCharacterization.lean
    complete
    theorem CryptBoolean.sum_vectorWalshCharacter_mul_walshTransform_sq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  ∑ u,
      (FABL.vectorWalshCharacter a) u *
        ↑(CryptBoolean.walshTransform f u) ^ 2 =
    2 ^ n * CryptBoolean.autocorrelation f a
    theorem CryptBoolean.sum_vectorWalshCharacter_mul_walshTransform_sq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  ∑ u,
      (FABL.vectorWalshCharacter a) u *
        ↑(CryptBoolean.walshTransform f
              u) ^
          2 =
    2 ^ n *
      CryptBoolean.autocorrelation f a
    Fourier inversion expresses autocorrelation as the character-weighted sum of
squared raw Walsh coefficients.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/WalshCharacterization.lean
    complete
    theorem CryptBoolean.satisfiesPropagationCriterion_iff_sum_vectorWalshCharacter_mul_walshTransform_sq_eq_zero
  {n : ℕ} (l : ℕ) (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesPropagationCriterion l f ↔
    ∀ (a : FABL.F₂Cube n),
      a ≠ 0 →
        (FABL.f₂Support a).card ≤ l →
          ∑ u,
              (FABL.vectorWalshCharacter a) u *
                ↑(CryptBoolean.walshTransform f u) ^ 2 =
            0
    theorem CryptBoolean.satisfiesPropagationCriterion_iff_sum_vectorWalshCharacter_mul_walshTransform_sq_eq_zero
  {n : ℕ} (l : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesPropagationCriterion
      l f ↔
    ∀ (a : FABL.F₂Cube n),
      a ≠ 0 →
        (FABL.f₂Support a).card ≤ l →
          ∑ u,
              (FABL.vectorWalshCharacter
                    a)
                  u *
                ↑(CryptBoolean.walshTransform
                      f u) ^
                  2 =
            0
    Carlet Chapter 8.1.1: `PC(l)` is equivalent to vanishing of every
low-weight nontrivial character sum of the squared raw Walsh spectrum.
Theorem7.1.8
Group: Chapter 7: Strict avalanche and propagation criteria (13)
Group member previews
Preview
Theorem 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Corollary 1.8.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-8proposition-35propagation-criterionwalsh-transformaffine-flatpage-131page-132fidelity-exact

Proposition 35 (Carlet, pp. 131--132). Let 0\le\ell\le n and f:V_n\to\mathbb F_2. Write w\preceq u when \operatorname{supp}(w)\subseteq\operatorname{supp}(u). Then f satisfies \mathrm{PC}(\ell) if and only if, for every u,v\in V_n with w_H(u)\ge n-\ell, \sum_{w\preceq u}W_f(w\oplus v)^2=2^{n+w_H(u)}.

Lean code for Theorem7.1.8●3 declarations
  • defdefined in CryptBoolean/Carlet/Chapter08/AffineFlatWalshCharacterization.lean
    complete
    def CryptBoolean.predecessorWalshSquareSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (u v : FABL.F₂Cube n) : ℝ
    def CryptBoolean.predecessorWalshSquareSum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u v : FABL.F₂Cube n) : ℝ
    The squared raw Walsh mass on the affine coordinate flat whose directions
precede `u`.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/AffineFlatWalshCharacterization.lean
    complete
    theorem CryptBoolean.predecessorWalshSquareSum_eq_autocorrelationSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (u v : FABL.F₂Cube n) :
  CryptBoolean.predecessorWalshSquareSum f u v =
    2 ^ (FABL.f₂Support u).card *
      ∑ x,
        (FABL.vectorWalshCharacter v) ↑x *
          CryptBoolean.autocorrelation f ↑x
    theorem CryptBoolean.predecessorWalshSquareSum_eq_autocorrelationSum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u v : FABL.F₂Cube n) :
  CryptBoolean.predecessorWalshSquareSum f
      u v =
    2 ^ (FABL.f₂Support u).card *
      ∑ x,
        (FABL.vectorWalshCharacter v) ↑x *
          CryptBoolean.autocorrelation f
            ↑x
    Raw Poisson summation for the affine coordinate flat of predecessors of
`u`.
  • theoremdefined in CryptBoolean/Carlet/Chapter08/AffineFlatWalshCharacterization.lean
    complete
    theorem CryptBoolean.satisfiesPropagationCriterion_iff_predecessorWalshSquareSum
  {n : ℕ} (l : ℕ) (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesPropagationCriterion l f ↔
    ∀ (u v : FABL.F₂Cube n),
      n - l ≤ (FABL.f₂Support u).card →
        CryptBoolean.predecessorWalshSquareSum f u v =
          2 ^ (n + (FABL.f₂Support u).card)
    theorem CryptBoolean.satisfiesPropagationCriterion_iff_predecessorWalshSquareSum
  {n : ℕ} (l : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesPropagationCriterion
      l f ↔
    ∀ (u v : FABL.F₂Cube n),
      n - l ≤ (FABL.f₂Support u).card →
        CryptBoolean.predecessorWalshSquareSum
            f u v =
          2 ^
            (n + (FABL.f₂Support u).card)
    Carlet Proposition 35: `PC(l)` is equivalent to a constant squared-Walsh
mass on every affine coordinate flat of dimension at least `n-l`.