5.13. Superclasses of bent functions🔗

Proposition5.13.1

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 4

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-6proposition-26relation-53pages-103-104fidelity-exact

Proposition 26 (Carlet, Relation (53), pp. 103--104). For a Boolean function f:V_n\to\mathbb F_2, let N_{\Delta_f}=|\{b:\Delta_f(b)\ne0\}|, \qquad N_{W_f}=|\{u:W_f(u)\ne0\}|. Then N_{\Delta_f}N_{W_f}\ge2^n. Equality holds if and only if every derivative D_bf is balanced or constant. Equivalently, there are complementary subspaces E,E' and functions g,h, with g bent on E and h affine on E', such that f(x+y)=g(x)+h(y) \qquad(x\in E,\ y\in E'). Such functions are called partially bent. Every quadratic function is partially bent, and every partially bent function is plateaued.

Lean code for Proposition5.13.1●23 declarations

defdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

def CryptBoolean.autocorrelationSupport {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Finset (FABL.F₂Cube n)

def CryptBoolean.autocorrelationSupport
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Finset (FABL.F₂Cube n)

The directions with nonzero autocorrelation.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.mem_autocorrelationSupport {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) :
  b ∈ CryptBoolean.autocorrelationSupport f ↔
    CryptBoolean.autocorrelation f b ≠ 0

theorem CryptBoolean.mem_autocorrelationSupport
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.F₂Cube n) :
  b ∈
      CryptBoolean.autocorrelationSupport
        f ↔
    CryptBoolean.autocorrelation f b ≠ 0

defdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

def CryptBoolean.nonzeroAutocorrelationCount {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℕ

def CryptBoolean.nonzeroAutocorrelationCount
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℕ

Carlet's quantity `N_Δf`, the number of nonzero autocorrelation
coefficients.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.rawFourierSupport_autocorrelation {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.rawFourierSupport (CryptBoolean.autocorrelation f) =
    CryptBoolean.walshSupport f

theorem CryptBoolean.rawFourierSupport_autocorrelation
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.rawFourierSupport
      (CryptBoolean.autocorrelation f) =
    CryptBoolean.walshSupport f

Wiener--Khintchine identifies the Fourier support of the autocorrelation
with the raw Walsh support.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.two_pow_le_nonzeroAutocorrelationCount_mul_card_walshSupport
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  2 ^ n ≤
    CryptBoolean.nonzeroAutocorrelationCount f *
      (CryptBoolean.walshSupport f).card

theorem CryptBoolean.two_pow_le_nonzeroAutocorrelationCount_mul_card_walshSupport
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  2 ^ n ≤
    CryptBoolean.nonzeroAutocorrelationCount
        f *
      (CryptBoolean.walshSupport f).card

Carlet Proposition 26, inequality (53).

defdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

def CryptBoolean.IsPartiallyBent {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop

def CryptBoolean.IsPartiallyBent {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop

A Boolean function is partially bent when every directional derivative
is balanced or constant.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.isPartiallyBent_of_functionAlgebraicDegree_le_two {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree : FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.IsPartiallyBent f

theorem CryptBoolean.isPartiallyBent_of_functionAlgebraicDegree_le_two
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.IsPartiallyBent f

Every quadratic Boolean function is partially bent.

defdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

def CryptBoolean.HasBentAffineComplementDecomposition {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (m k : ℕ) : Prop

def CryptBoolean.HasBentAffineComplementDecomposition
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (m k : ℕ) : Prop

A coordinate-free form of Carlet's complementary-subspace
decomposition. The second summand is affine with its constant absorbed into
the bent summand.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.HasBentAffineComplementDecomposition.isPartiallyBent
  {n : ℕ} {f : CryptBoolean.BooleanFunction n} {m k : ℕ}
  (hf : CryptBoolean.HasBentAffineComplementDecomposition f m k) :
  CryptBoolean.IsPartiallyBent f

theorem CryptBoolean.HasBentAffineComplementDecomposition.isPartiallyBent
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {m k : ℕ}
  (hf :
    CryptBoolean.HasBentAffineComplementDecomposition
      f m k) :
  CryptBoolean.IsPartiallyBent f

Every bent-plus-affine complementary decomposition is partially bent.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.HasBentAffineComplementDecomposition.linearKernel_eq_affineSubspace
  {n : ℕ} {f : CryptBoolean.BooleanFunction n} {m k : ℕ}
  (hf : CryptBoolean.HasBentAffineComplementDecomposition f m k) :
  ∃ E E',
    ∃ (_ : IsCompl E E'),
      ∃ eE eE' g ε,
        CryptBoolean.IsBent g ∧
          CryptBoolean.linearKernel f = E' ∧
            ∀ (x : FABL.F₂Cube m) (y : FABL.F₂Cube k),
              f (↑(eE x) + ↑(eE' y)) = g x + FABL.f₂DotProduct ε y

theorem CryptBoolean.HasBentAffineComplementDecomposition.linearKernel_eq_affineSubspace
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {m k : ℕ}
  (hf :
    CryptBoolean.HasBentAffineComplementDecomposition
      f m k) :
  ∃ E E',
    ∃ (_ : IsCompl E E'),
      ∃ eE eE' g ε,
        CryptBoolean.IsBent g ∧
          CryptBoolean.linearKernel f =
              E' ∧
            ∀ (x : FABL.F₂Cube m)
              (y : FABL.F₂Cube k),
              f (↑(eE x) + ↑(eE' y)) =
                g x +
                  FABL.f₂DotProduct ε y

In a bent-plus-affine complementary decomposition, the affine summand is
exactly the linear kernel.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.HasBentAffineComplementDecomposition.dimensions_add {n : ℕ}
  {f : CryptBoolean.BooleanFunction n} {m k : ℕ}
  (hf : CryptBoolean.HasBentAffineComplementDecomposition f m k) :
  m + k = n

theorem CryptBoolean.HasBentAffineComplementDecomposition.dimensions_add
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {m k : ℕ}
  (hf :
    CryptBoolean.HasBentAffineComplementDecomposition
      f m k) :
  m + k = n

Complementary coordinate dimensions add to the ambient dimension.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.HasBentAffineComplementDecomposition.even_bentDimension
  {n : ℕ} {f : CryptBoolean.BooleanFunction n} {m k : ℕ}
  (hf : CryptBoolean.HasBentAffineComplementDecomposition f m k) :
  Even m

theorem CryptBoolean.HasBentAffineComplementDecomposition.even_bentDimension
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {m k : ℕ}
  (hf :
    CryptBoolean.HasBentAffineComplementDecomposition
      f m k) :
  Even m

The bent summand has even dimension.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.exists_hasBentAffineComplementDecomposition_of_isPartiallyBent
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsPartiallyBent f) :
  ∃ m k, CryptBoolean.HasBentAffineComplementDecomposition f m k

theorem CryptBoolean.exists_hasBentAffineComplementDecomposition_of_isPartiallyBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsPartiallyBent f) :
  ∃ m k,
    CryptBoolean.HasBentAffineComplementDecomposition
      f m k

Every partially bent function decomposes over complementary subspaces as
a bent function plus an affine function.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.isPartiallyBent_iff_exists_bentAffineComplementDecomposition
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsPartiallyBent f ↔
    ∃ m k, CryptBoolean.HasBentAffineComplementDecomposition f m k

theorem CryptBoolean.isPartiallyBent_iff_exists_bentAffineComplementDecomposition
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsPartiallyBent f ↔
    ∃ m k,
      CryptBoolean.HasBentAffineComplementDecomposition
        f m k

Carlet Proposition 26's structural characterization.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.isLinearStructure_iff_abs_autocorrelation_eq_two_pow
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) :
  CryptBoolean.IsLinearStructure f b ↔
    |CryptBoolean.autocorrelation f b| = 2 ^ n

theorem CryptBoolean.isLinearStructure_iff_abs_autocorrelation_eq_two_pow
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.F₂Cube n) :
  CryptBoolean.IsLinearStructure f b ↔
    |CryptBoolean.autocorrelation f b| =
      2 ^ n

A direction is a linear structure exactly when its autocorrelation has
maximal absolute value.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.isPartiallyBent_of_nonzeroAutocorrelationCount_mul_card_walshSupport_eq
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hproduct :
    CryptBoolean.nonzeroAutocorrelationCount f *
        (CryptBoolean.walshSupport f).card =
      2 ^ n) :
  CryptBoolean.IsPartiallyBent f

theorem CryptBoolean.isPartiallyBent_of_nonzeroAutocorrelationCount_mul_card_walshSupport_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hproduct :
    CryptBoolean.nonzeroAutocorrelationCount
          f *
        (CryptBoolean.walshSupport
            f).card =
      2 ^ n) :
  CryptBoolean.IsPartiallyBent f

Equality in Carlet's support inequality forces every derivative to be
balanced or constant.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.nonzeroAutocorrelationCount_mul_card_walshSupport_eq_of_isPartiallyBent
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsPartiallyBent f) :
  CryptBoolean.nonzeroAutocorrelationCount f *
      (CryptBoolean.walshSupport f).card =
    2 ^ n

theorem CryptBoolean.nonzeroAutocorrelationCount_mul_card_walshSupport_eq_of_isPartiallyBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsPartiallyBent f) :
  CryptBoolean.nonzeroAutocorrelationCount
        f *
      (CryptBoolean.walshSupport f).card =
    2 ^ n

If every derivative is balanced or constant, equality holds in Carlet's
support inequality.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.nonzeroAutocorrelationCount_mul_card_walshSupport_eq_two_pow_iff
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.nonzeroAutocorrelationCount f *
        (CryptBoolean.walshSupport f).card =
      2 ^ n ↔
    CryptBoolean.IsPartiallyBent f

theorem CryptBoolean.nonzeroAutocorrelationCount_mul_card_walshSupport_eq_two_pow_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.nonzeroAutocorrelationCount
          f *
        (CryptBoolean.walshSupport
            f).card =
      2 ^ n ↔
    CryptBoolean.IsPartiallyBent f

Carlet Proposition 26: equality in (53) is equivalent to partial
bentness.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.HasBentAffineComplementDecomposition.nonzeroAutocorrelationCount_eq
  {n : ℕ} {f : CryptBoolean.BooleanFunction n} {m k : ℕ}
  (hf : CryptBoolean.HasBentAffineComplementDecomposition f m k) :
  CryptBoolean.nonzeroAutocorrelationCount f = 2 ^ k

theorem CryptBoolean.HasBentAffineComplementDecomposition.nonzeroAutocorrelationCount_eq
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {m k : ℕ}
  (hf :
    CryptBoolean.HasBentAffineComplementDecomposition
      f m k) :
  CryptBoolean.nonzeroAutocorrelationCount
      f =
    2 ^ k

The autocorrelation support has the cardinality of the affine summand.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.hasPlateauedWalshSpectrum_of_isPartiallyBent {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsPartiallyBent f) :
  CryptBoolean.HasPlateauedWalshSpectrum f

theorem CryptBoolean.hasPlateauedWalshSpectrum_of_isPartiallyBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsPartiallyBent f) :
  CryptBoolean.HasPlateauedWalshSpectrum f

Every partially bent function has a flat nonzero Walsh spectrum.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.IsPartiallyBent.isPlateaued {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsPartiallyBent f) : CryptBoolean.IsPlateaued f

theorem CryptBoolean.IsPartiallyBent.isPlateaued
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsPartiallyBent f) :
  CryptBoolean.IsPlateaued f

Every partially bent function is plateaued.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.isPlateaued_of_functionAlgebraicDegree_le_two {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree : FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.IsPlateaued f

theorem CryptBoolean.isPlateaued_of_functionAlgebraicDegree_le_two
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.IsPlateaued f

In particular, every quadratic Boolean function is plateaued.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartiallyBent.lean

complete

theorem CryptBoolean.HasBentAffineComplementDecomposition.hasPlateauedWalshAmplitude
  {n : ℕ} {f : CryptBoolean.BooleanFunction n} {m k : ℕ}
  (hf : CryptBoolean.HasBentAffineComplementDecomposition f m k) :
  CryptBoolean.HasPlateauedWalshAmplitude f (2 ^ (k + m / 2))

theorem CryptBoolean.HasBentAffineComplementDecomposition.hasPlateauedWalshAmplitude
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {m k : ℕ}
  (hf :
    CryptBoolean.HasBentAffineComplementDecomposition
      f m k) :
  CryptBoolean.HasPlateauedWalshAmplitude
    f (2 ^ (k + m / 2))

In a decomposition with bent dimension `m` and affine dimension `k`,
every nonzero Walsh coefficient has magnitude `2^(k + m/2)`.

Proposition5.13.2

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 1.8.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-6proposition-27pages-104-105fidelity-exact-nonzero-modulation

Proposition 27 (Carlet, pp. 104--105). Let \varphi:V_n\to\mathbb R be nonzero, and write N_\varphi=|\{x:\varphi(x)\ne0\}|, \qquad N_{\widehat\varphi}=|\{u:\widehat\varphi(u)\ne0\}|. Then N_\varphi N_{\widehat\varphi}\ge2^n. Equality holds if and only if there are a nonzero real number \lambda, a frequency u, and an affine flat F such that \varphi(x)= \begin{cases} \lambda(-1)^{u\mathbin\cdot x},&x\in F,\\ 0,&x\notin F. \end{cases}

Lean code for Proposition5.13.2●7 declarations

defdefined in CryptBoolean/Carlet/Chapter06/FourierUncertainty.lean

complete

def CryptBoolean.pseudoBooleanSupport {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) : Finset (FABL.F₂Cube n)

def CryptBoolean.pseudoBooleanSupport {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  Finset (FABL.F₂Cube n)

The finite support of a pseudo-Boolean function.

theoremdefined in CryptBoolean/Carlet/Chapter06/FourierUncertainty.lean

complete

theorem CryptBoolean.mem_pseudoBooleanSupport {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) (x : FABL.F₂Cube n) :
  x ∈ CryptBoolean.pseudoBooleanSupport φ ↔ φ x ≠ 0

theorem CryptBoolean.mem_pseudoBooleanSupport
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (x : FABL.F₂Cube n) :
  x ∈
      CryptBoolean.pseudoBooleanSupport
        φ ↔
    φ x ≠ 0

theoremdefined in CryptBoolean/Carlet/Chapter06/FourierUncertainty.lean

complete

theorem CryptBoolean.two_pow_le_card_pseudoBooleanSupport_mul_card_rawFourierSupport
  {n : ℕ} (φ : FABL.PseudoBooleanFunction n) (hφ : φ ≠ 0) :
  2 ^ n ≤
    (CryptBoolean.pseudoBooleanSupport φ).card *
      (CryptBoolean.rawFourierSupport φ).card

theorem CryptBoolean.two_pow_le_card_pseudoBooleanSupport_mul_card_rawFourierSupport
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (hφ : φ ≠ 0) :
  2 ^ n ≤
    (CryptBoolean.pseudoBooleanSupport
          φ).card *
      (CryptBoolean.rawFourierSupport
          φ).card

Carlet Proposition 27's uncertainty inequality: for every nonzero
pseudo-Boolean function, the product of its value-support size and raw
Fourier-support size is at least the size of the binary cube.

defdefined in CryptBoolean/Carlet/Chapter06/FourierUncertainty.lean

complete

def CryptBoolean.IsModulatedAffineFlatIndicator {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) : Prop

def CryptBoolean.IsModulatedAffineFlatIndicator
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  Prop

A pseudo-Boolean function is a modulated affine-flat indicator when it is
a nonzero real multiple of one Walsh character on an affine flat and vanishes
off that flat.

theoremdefined in CryptBoolean/Carlet/Chapter06/FourierUncertainty.lean

complete

theorem CryptBoolean.IsModulatedAffineFlatIndicator.card_support_mul_card_rawFourierSupport_eq
  {n : ℕ} {φ : FABL.PseudoBooleanFunction n}
  (hφ : CryptBoolean.IsModulatedAffineFlatIndicator φ) :
  (CryptBoolean.pseudoBooleanSupport φ).card *
      (CryptBoolean.rawFourierSupport φ).card =
    2 ^ n

theorem CryptBoolean.IsModulatedAffineFlatIndicator.card_support_mul_card_rawFourierSupport_eq
  {n : ℕ}
  {φ : FABL.PseudoBooleanFunction n}
  (hφ :
    CryptBoolean.IsModulatedAffineFlatIndicator
      φ) :
  (CryptBoolean.pseudoBooleanSupport
          φ).card *
      (CryptBoolean.rawFourierSupport
          φ).card =
    2 ^ n

Every nonzero modulated affine-flat indicator attains equality in the
Fourier uncertainty bound.

theoremdefined in CryptBoolean/Carlet/Chapter06/FourierUncertainty.lean

complete

theorem CryptBoolean.isModulatedAffineFlatIndicator_of_card_support_mul_card_rawFourierSupport_eq
  {n : ℕ} (φ : FABL.PseudoBooleanFunction n) (hφ : φ ≠ 0)
  (hproduct :
    (CryptBoolean.pseudoBooleanSupport φ).card *
        (CryptBoolean.rawFourierSupport φ).card =
      2 ^ n) :
  CryptBoolean.IsModulatedAffineFlatIndicator φ

theorem CryptBoolean.isModulatedAffineFlatIndicator_of_card_support_mul_card_rawFourierSupport_eq
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (hφ : φ ≠ 0)
  (hproduct :
    (CryptBoolean.pseudoBooleanSupport
            φ).card *
        (CryptBoolean.rawFourierSupport
            φ).card =
      2 ^ n) :
  CryptBoolean.IsModulatedAffineFlatIndicator
    φ

Equality in the Fourier uncertainty bound forces the value support to be
an affine flat and the function to be a nonzero scalar multiple of one Walsh
character on that flat.

theoremdefined in CryptBoolean/Carlet/Chapter06/FourierUncertainty.lean

complete

theorem CryptBoolean.card_support_mul_card_rawFourierSupport_eq_two_pow_iff
  {n : ℕ} (φ : FABL.PseudoBooleanFunction n) (hφ : φ ≠ 0) :
  (CryptBoolean.pseudoBooleanSupport φ).card *
        (CryptBoolean.rawFourierSupport φ).card =
      2 ^ n ↔
    CryptBoolean.IsModulatedAffineFlatIndicator φ

theorem CryptBoolean.card_support_mul_card_rawFourierSupport_eq_two_pow_iff
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (hφ : φ ≠ 0) :
  (CryptBoolean.pseudoBooleanSupport
            φ).card *
        (CryptBoolean.rawFourierSupport
            φ).card =
      2 ^ n ↔
    CryptBoolean.IsModulatedAffineFlatIndicator
      φ

Carlet Proposition 27's equality classification. The coefficient is
explicitly nonzero, as forced by the theorem's nonzero-function hypothesis.

Definition5.13.3

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.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 5.13.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagscarletchapter-6partial-bentpage-105fidelity-exact

Partial bent functions (Carlet, p. 105). Let n be even. A Boolean function f:V_n\to\mathbb F_2 is partial bent if there is an integer \lambda such that, on V_n\setminus\{0\}, its raw Fourier transform as a \{0,1\}-valued function takes exactly the two values \lambda and \lambda+2^{n/2}.

Lean code for Definition5.13.3●4 declarations

defdefined in CryptBoolean/Carlet/Chapter06/PartialBent.lean

complete

def CryptBoolean.HasPartialBentFourierLevels {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (level : ℤ) : Prop

def CryptBoolean.HasPartialBentFourierLevels
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (level : ℤ) : Prop

The raw Fourier transform of the zero-one embedding takes exactly the
levels `level` and `level + 2^(n/2)` on the punctured cube.

defdefined in CryptBoolean/Carlet/Chapter06/PartialBent.lean

complete

def CryptBoolean.IsPartialBent {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop

def CryptBoolean.IsPartialBent {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop

A partial bent function has even dimension and exactly two raw Fourier
levels, separated by `2^(n/2)`, on the punctured cube.

defdefined in CryptBoolean/Carlet/Chapter06/PartialBentDual.lean

complete

def CryptBoolean.partialBentIntegerFourier {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (u : FABL.F₂Cube n) : ℤ

def CryptBoolean.partialBentIntegerFourier
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube n) : ℤ

The integral raw Fourier transform of a Boolean function's zero-one embedding.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialBentDual.lean

complete

theorem CryptBoolean.partialBentIntegerFourier_cast {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (u : FABL.F₂Cube n) :
  ↑(CryptBoolean.partialBentIntegerFourier f u) =
    CryptBoolean.rawFourierTransform (FABL.booleanRealEmbedding f) u

theorem CryptBoolean.partialBentIntegerFourier_cast
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube n) :
  ↑(CryptBoolean.partialBentIntegerFourier
        f u) =
    CryptBoolean.rawFourierTransform
      (FABL.booleanRealEmbedding f) u

The integral partial-bent transform casts to the raw real Fourier transform.

Theorem5.13.4

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 1.8.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-6partial-bentdualitypage-105fidelity-formal-zero-frequency-convention

Duality for partial bent functions (Carlet, p. 105). Let f be partial bent with Fourier levels \lambda and \lambda+2^{n/2}. Define its dual at zero by \widetilde f(0)=f(0) and, for every nonzero u, by \widetilde f(u)= \begin{cases} 0,&\widehat f(u)=\lambda,\\ 1,&\widehat f(u)=\lambda+2^{n/2}. \end{cases} Then \widetilde f is partial bent and \widetilde{\widetilde f}=f.

Lean code for Theorem5.13.4●5 declarations

defdefined in CryptBoolean/Carlet/Chapter06/PartialBentDual.lean

complete

def CryptBoolean.partialBentDual {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (level : ℤ) :
  CryptBoolean.BooleanFunction n

def CryptBoolean.partialBentDual {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (level : ℤ) :
  CryptBoolean.BooleanFunction n

The dual of a partial bent function, with the source's punctured-spectrum
convention completed at zero by `f(0)`.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialBentDual.lean

complete

theorem CryptBoolean.partialBentDual_zero {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (level : ℤ) :
  CryptBoolean.partialBentDual f level 0 = f 0

theorem CryptBoolean.partialBentDual_zero {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (level : ℤ) :
  CryptBoolean.partialBentDual f level 0 =
    f 0

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialBentDual.lean

complete

theorem CryptBoolean.exists_partialBentDual_fourierLevels {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (level : ℤ) (hn : Even n)
  (hlevels : CryptBoolean.HasPartialBentFourierLevels f level) :
  ∃ dualLevel,
    CryptBoolean.HasPartialBentFourierLevels
        (CryptBoolean.partialBentDual f level) dualLevel ∧
      ∀ (x : FABL.F₂Cube n),
        x ≠ 0 →
          CryptBoolean.partialBentIntegerFourier
              (CryptBoolean.partialBentDual f level) x =
            dualLevel + 2 ^ (n / 2) * CryptBoolean.bitValueInt (f x)

theorem CryptBoolean.exists_partialBentDual_fourierLevels
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (level : ℤ) (hn : Even n)
  (hlevels :
    CryptBoolean.HasPartialBentFourierLevels
      f level) :
  ∃ dualLevel,
    CryptBoolean.HasPartialBentFourierLevels
        (CryptBoolean.partialBentDual f
          level)
        dualLevel ∧
      ∀ (x : FABL.F₂Cube n),
        x ≠ 0 →
          CryptBoolean.partialBentIntegerFourier
              (CryptBoolean.partialBentDual
                f level)
              x =
            dualLevel +
              2 ^ (n / 2) *
                CryptBoolean.bitValueInt
                  (f x)

The punctured Fourier transform of the partial-bent dual again has two
levels, and its level choice records the values of the original function.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialBentDual.lean

complete

theorem CryptBoolean.partialBentDual_involution {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (level dualLevel : ℤ)
  (hdual :
    ∀ (x : FABL.F₂Cube n),
      x ≠ 0 →
        CryptBoolean.partialBentIntegerFourier
            (CryptBoolean.partialBentDual f level) x =
          dualLevel + 2 ^ (n / 2) * CryptBoolean.bitValueInt (f x)) :
  CryptBoolean.partialBentDual (CryptBoolean.partialBentDual f level)
      dualLevel =
    f

theorem CryptBoolean.partialBentDual_involution
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (level dualLevel : ℤ)
  (hdual :
    ∀ (x : FABL.F₂Cube n),
      x ≠ 0 →
        CryptBoolean.partialBentIntegerFourier
            (CryptBoolean.partialBentDual
              f level)
            x =
          dualLevel +
            2 ^ (n / 2) *
              CryptBoolean.bitValueInt
                (f x)) :
  CryptBoolean.partialBentDual
      (CryptBoolean.partialBentDual f
        level)
      dualLevel =
    f

Taking the partial-bent dual twice, with the Fourier levels supplied by
the first duality theorem, returns the original function.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialBentDual.lean

complete

theorem CryptBoolean.exists_isPartialBent_partialBentDual_and_involution {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (level : ℤ) (hn : Even n)
  (hlevels : CryptBoolean.HasPartialBentFourierLevels f level) :
  ∃ dualLevel,
    CryptBoolean.IsPartialBent (CryptBoolean.partialBentDual f level) ∧
      CryptBoolean.HasPartialBentFourierLevels
          (CryptBoolean.partialBentDual f level) dualLevel ∧
        CryptBoolean.partialBentDual
            (CryptBoolean.partialBentDual f level) dualLevel =
          f

theorem CryptBoolean.exists_isPartialBent_partialBentDual_and_involution
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (level : ℤ) (hn : Even n)
  (hlevels :
    CryptBoolean.HasPartialBentFourierLevels
      f level) :
  ∃ dualLevel,
    CryptBoolean.IsPartialBent
        (CryptBoolean.partialBentDual f
          level) ∧
      CryptBoolean.HasPartialBentFourierLevels
          (CryptBoolean.partialBentDual f
            level)
          dualLevel ∧
        CryptBoolean.partialBentDual
            (CryptBoolean.partialBentDual
              f level)
            dualLevel =
          f

A partial-bent dual is partial bent, and its dual is the original function.

Theorem5.13.5

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Proposition 5.4.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-6partial-bentalgebraic-degreerothaus-boundcounterexamplepage-105fidelity-source-error-exact-two-level-counterexample

Counterexample to the printed partial-bent degree bound (Carlet, p. 105). On V_2, let f be the indicator of the point (1,0). Then f is partial bent, but \deg_{\mathrm{alg}}(f)=2>2/2. Thus the printed half-dimension bound requires additional regularity hypotheses beyond the exact punctured two-level definition.

Lean code for Theorem5.13.5●2 declarations

defdefined in CryptBoolean/Carlet/Chapter06/PartialBentCounterexamples.lean

complete

def CryptBoolean.partialBentDegreeCounterexample :
  CryptBoolean.BooleanFunction 2

def CryptBoolean.partialBentDegreeCounterexample :
  CryptBoolean.BooleanFunction 2

The indicator of the singleton binary point `![1, 0]`.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialBentCounterexamples.lean

complete

theorem CryptBoolean.partialBentDegreeCounterexample_refutes_bound :
  CryptBoolean.IsPartialBent
      CryptBoolean.partialBentDegreeCounterexample ∧
    FABL.functionAlgebraicDegree
          CryptBoolean.partialBentDegreeCounterexample =
        2 ∧
      2 / 2 <
        FABL.functionAlgebraicDegree
          CryptBoolean.partialBentDegreeCounterexample

theorem CryptBoolean.partialBentDegreeCounterexample_refutes_bound :
  CryptBoolean.IsPartialBent
      CryptBoolean.partialBentDegreeCounterexample ∧
    FABL.functionAlgebraicDegree
          CryptBoolean.partialBentDegreeCounterexample =
        2 ∧
      2 / 2 <
        FABL.functionAlgebraicDegree
          CryptBoolean.partialBentDegreeCounterexample

The exact punctured two-level definition permits algebraic degree
strictly greater than half the dimension.

Theorem5.13.6

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

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-6partial-benttypesparsevalpage-105fidelity-source-correction-type-formula

The two types of partial bent functions (Carlet, p. 105; corrected). Let n>0 be even, put q=2^{n/2} and e=f(0), and let f be partial bent with Fourier levels \lambda and \lambda+q. Exactly one of the two identities \widehat f(0)-e=-(\lambda-e)(q-1) and \widehat f(0)-e=(q+\lambda-e)(q+1) holds; these alternatives define the two types.

Lean code for Theorem5.13.6●1 theorem

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialBentDual.lean

complete

theorem CryptBoolean.partialBent_fourier_level_types {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (level : ℤ) (hnEven : Even n)
  (hn : 0 < n)
  (hlevels : CryptBoolean.HasPartialBentFourierLevels f level) :
  Xor
    (CryptBoolean.partialBentIntegerFourier f 0 -
        CryptBoolean.bitValueInt (f 0) =
      -(level - CryptBoolean.bitValueInt (f 0)) * (2 ^ (n / 2) - 1))
    (CryptBoolean.partialBentIntegerFourier f 0 -
        CryptBoolean.bitValueInt (f 0) =
      (2 ^ (n / 2) + level - CryptBoolean.bitValueInt (f 0)) *
        (2 ^ (n / 2) + 1))

theorem CryptBoolean.partialBent_fourier_level_types
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (level : ℤ) (hnEven : Even n)
  (hn : 0 < n)
  (hlevels :
    CryptBoolean.HasPartialBentFourierLevels
      f level) :
  Xor
    (CryptBoolean.partialBentIntegerFourier
          f 0 -
        CryptBoolean.bitValueInt (f 0) =
      -(level -
            CryptBoolean.bitValueInt
              (f 0)) *
        (2 ^ (n / 2) - 1))
    (CryptBoolean.partialBentIntegerFourier
          f 0 -
        CryptBoolean.bitValueInt (f 0) =
      (2 ^ (n / 2) + level -
          CryptBoolean.bitValueInt
            (f 0)) *
        (2 ^ (n / 2) + 1))

Parseval gives the two mutually exclusive partial-bent Fourier types.
The second factor has the corrected sign, and both factors retain the origin
value required by the punctured-spectrum convention.

Theorem5.13.7

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 1.8.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-6partial-bentsumsupportscounterexamplepage-105fidelity-source-error-exact-two-level-counterexample

Counterexample to the printed partial-bent sum assertion (Carlet, p. 105). On V_2, let f be the indicator of \{(1,0)\} and let g(x)=x_2, the indicator of \{(0,1),(1,1)\}. Their punctured Fourier levels are \{-1,1\} and \{-2,0\}, respectively. Both functions are partial bent of the corrected first type, and \operatorname{supp}(f)\cap\operatorname{supp}(g)\subseteq\{0\}. Nevertheless, f+g is not partial bent. Hence the printed closure assertion also requires an additional regularity convention.

Lean code for Theorem5.13.7●2 declarations

defdefined in CryptBoolean/Carlet/Chapter06/PartialBentCounterexamples.lean

complete

def CryptBoolean.partialBentSumCounterexampleCompanion :
  CryptBoolean.BooleanFunction 2

def CryptBoolean.partialBentSumCounterexampleCompanion :
  CryptBoolean.BooleanFunction 2

The indicator of the two points whose second coordinate is one.

theoremdefined in CryptBoolean/Carlet/Chapter06/PartialBentCounterexamples.lean

complete

theorem CryptBoolean.partialBentCounterexamples_refute_disjoint_support_sum :
  CryptBoolean.HasPartialBentFourierLevels
      CryptBoolean.partialBentDegreeCounterexample (-1) ∧
    CryptBoolean.HasPartialBentFourierLevels
        CryptBoolean.partialBentSumCounterexampleCompanion (-2) ∧
      CryptBoolean.IsPartialBent
          CryptBoolean.partialBentDegreeCounterexample ∧
        CryptBoolean.IsPartialBent
            CryptBoolean.partialBentSumCounterexampleCompanion ∧
          CryptBoolean.partialBentIntegerFourier
                  CryptBoolean.partialBentDegreeCounterexample 0 -
                CryptBoolean.bitValueInt
                  (CryptBoolean.partialBentDegreeCounterexample 0) =
              -(-1 -
                    CryptBoolean.bitValueInt
                      (CryptBoolean.partialBentDegreeCounterexample
                        0)) *
                (2 ^ (2 / 2) - 1) ∧
            CryptBoolean.partialBentIntegerFourier
                    CryptBoolean.partialBentSumCounterexampleCompanion
                    0 -
                  CryptBoolean.bitValueInt
                    (CryptBoolean.partialBentSumCounterexampleCompanion
                      0) =
                -(-2 -
                      CryptBoolean.bitValueInt
                        (CryptBoolean.partialBentSumCounterexampleCompanion
                          0)) *
                  (2 ^ (2 / 2) - 1) ∧
              CryptBoolean.support
                      CryptBoolean.partialBentDegreeCounterexample ∩
                    CryptBoolean.support
                      CryptBoolean.partialBentSumCounterexampleCompanion ⊆
                  {0} ∧
                ¬CryptBoolean.IsPartialBent
                    (CryptBoolean.partialBentDegreeCounterexample +
                      CryptBoolean.partialBentSumCounterexampleCompanion)

theorem CryptBoolean.partialBentCounterexamples_refute_disjoint_support_sum :
  CryptBoolean.HasPartialBentFourierLevels
      CryptBoolean.partialBentDegreeCounterexample
      (-1) ∧
    CryptBoolean.HasPartialBentFourierLevels
        CryptBoolean.partialBentSumCounterexampleCompanion
        (-2) ∧
      CryptBoolean.IsPartialBent
          CryptBoolean.partialBentDegreeCounterexample ∧
        CryptBoolean.IsPartialBent
            CryptBoolean.partialBentSumCounterexampleCompanion ∧
          CryptBoolean.partialBentIntegerFourier
                  CryptBoolean.partialBentDegreeCounterexample
                  0 -
                CryptBoolean.bitValueInt
                  (CryptBoolean.partialBentDegreeCounterexample
                    0) =
              -(-1 -
                    CryptBoolean.bitValueInt
                      (CryptBoolean.partialBentDegreeCounterexample
                        0)) *
                (2 ^ (2 / 2) - 1) ∧
            CryptBoolean.partialBentIntegerFourier
                    CryptBoolean.partialBentSumCounterexampleCompanion
                    0 -
                  CryptBoolean.bitValueInt
                    (CryptBoolean.partialBentSumCounterexampleCompanion
                      0) =
                -(-2 -
                      CryptBoolean.bitValueInt
                        (CryptBoolean.partialBentSumCounterexampleCompanion
                          0)) *
                  (2 ^ (2 / 2) - 1) ∧
              CryptBoolean.support
                      CryptBoolean.partialBentDegreeCounterexample ∩
                    CryptBoolean.support
                      CryptBoolean.partialBentSumCounterexampleCompanion ⊆
                  {0} ∧
                ¬CryptBoolean.IsPartialBent
                    (CryptBoolean.partialBentDegreeCounterexample +
                      CryptBoolean.partialBentSumCounterexampleCompanion)

Two partial bent functions of the corrected first Fourier type can
have disjoint supports while their sum fails to be partial bent.

Definition5.13.8

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.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 6

Reverse dependency previews

Preview

Corollary 5.7.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagscarletchapter-6plateauedpages-105-106fidelity-exact

Plateaued functions (Carlet, pp. 105--106). A Boolean function is plateaued with amplitude \lambda>0 when every Walsh coefficient belongs to \{0,\lambda,-\lambda\}. A plateaued function is bent exactly when its Walsh transform has full support. Parseval's identity forces \lambda=2^r with 2r\ge n; consequently every Walsh coefficient is divisible by 2^{\lceil n/2\rceil}.

Lean code for Definition5.13.8●7 declarations

defdefined in CryptBoolean/Carlet/Chapter06/Plateaued.lean

complete

def CryptBoolean.HasPlateauedWalshAmplitude {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (amplitude : ℕ) : Prop

def CryptBoolean.HasPlateauedWalshAmplitude
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (amplitude : ℕ) : Prop

A Boolean function has Walsh amplitude `amplitude` when every raw Walsh
coefficient is zero or has that positive integral magnitude.

defdefined in CryptBoolean/Carlet/Chapter06/Plateaued.lean

complete

def CryptBoolean.IsPlateaued {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  Prop

def CryptBoolean.IsPlateaued {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop

A Boolean function is plateaued when it has some positive integral Walsh amplitude.

theoremdefined in CryptBoolean/Carlet/Chapter06/Plateaued.lean

complete

theorem CryptBoolean.isPlateaued_iff_hasPlateauedWalshSpectrum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsPlateaued f ↔ CryptBoolean.HasPlateauedWalshSpectrum f

theorem CryptBoolean.isPlateaued_iff_hasPlateauedWalshSpectrum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsPlateaued f ↔
    CryptBoolean.HasPlateauedWalshSpectrum
      f

Carlet's integral-amplitude definition agrees with the existing real
flat-on-support predicate.

theoremdefined in CryptBoolean/Carlet/Chapter06/Plateaued.lean

complete

theorem CryptBoolean.isBent_iff_isPlateaued_and_forall_walshTransform_ne_zero
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.IsPlateaued f ∧
      ∀ (a : FABL.F₂Cube n), CryptBoolean.walshTransform f a ≠ 0

theorem CryptBoolean.isBent_iff_isPlateaued_and_forall_walshTransform_ne_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.IsPlateaued f ∧
      ∀ (a : FABL.F₂Cube n),
        CryptBoolean.walshTransform f a ≠
          0

A bent function is exactly a plateaued function with full Walsh support.

theoremdefined in CryptBoolean/Carlet/Chapter06/Plateaued.lean

complete

theorem CryptBoolean.card_walshSupport_mul_amplitude_sq_eq_two_pow_two_mul
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (amplitude : ℕ)
  (hf : CryptBoolean.HasPlateauedWalshAmplitude f amplitude) :
  (CryptBoolean.walshSupport f).card * amplitude ^ 2 = 2 ^ (2 * n)

theorem CryptBoolean.card_walshSupport_mul_amplitude_sq_eq_two_pow_two_mul
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (amplitude : ℕ)
  (hf :
    CryptBoolean.HasPlateauedWalshAmplitude
      f amplitude) :
  (CryptBoolean.walshSupport f).card *
      amplitude ^ 2 =
    2 ^ (2 * n)

Parseval determines the product of Walsh-support size and squared plateaued amplitude.

theoremdefined in CryptBoolean/Carlet/Chapter06/Plateaued.lean

complete

theorem CryptBoolean.exists_plateauedAmplitudeExponent {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (amplitude : ℕ)
  (hf : CryptBoolean.HasPlateauedWalshAmplitude f amplitude) :
  ∃ r, amplitude = 2 ^ r ∧ n ≤ 2 * r

theorem CryptBoolean.exists_plateauedAmplitudeExponent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (amplitude : ℕ)
  (hf :
    CryptBoolean.HasPlateauedWalshAmplitude
      f amplitude) :
  ∃ r, amplitude = 2 ^ r ∧ n ≤ 2 * r

The amplitude of a plateaued Boolean function is a power of two, and its
exponent is at least half the dimension.

theoremdefined in CryptBoolean/Carlet/Chapter06/Plateaued.lean

complete

theorem CryptBoolean.two_pow_add_one_div_two_dvd_walshTransform_of_hasPlateauedWalshAmplitude
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (amplitude : ℕ)
  (hf : CryptBoolean.HasPlateauedWalshAmplitude f amplitude)
  (a : FABL.F₂Cube n) :
  ↑(2 ^ ((n + 1) / 2)) ∣ CryptBoolean.walshTransform f a

theorem CryptBoolean.two_pow_add_one_div_two_dvd_walshTransform_of_hasPlateauedWalshAmplitude
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (amplitude : ℕ)
  (hf :
    CryptBoolean.HasPlateauedWalshAmplitude
      f amplitude)
  (a : FABL.F₂Cube n) :
  ↑(2 ^ ((n + 1) / 2)) ∣
    CryptBoolean.walshTransform f a

Every Walsh coefficient of a plateaued Boolean function is divisible by
`2^⌈n/2⌉`; this is `2^(n/2)` in even dimension and `2^((n+1)/2)` in odd dimension.

Theorem5.13.9

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.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-6plateauedpage-106fidelity-exact

Walsh-support bound (Carlet, p. 106). If N_{W_f} is the cardinality of the Walsh support of f:V_n\to\mathbb F_2, then \operatorname{nl}(f) \le 2^{n-1}\left(1-\frac1{\sqrt{N_{W_f}}}\right). Equality holds if and only if f is plateaued.

Lean code for Theorem5.13.9●6 theorems

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedSupport.lean

complete

theorem CryptBoolean.maxWalshMagnitude_eq_of_hasPlateauedWalshAmplitude {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (amplitude : ℕ)
  (hf : CryptBoolean.HasPlateauedWalshAmplitude f amplitude) :
  CryptBoolean.maxWalshMagnitude f = amplitude

theorem CryptBoolean.maxWalshMagnitude_eq_of_hasPlateauedWalshAmplitude
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (amplitude : ℕ)
  (hf :
    CryptBoolean.HasPlateauedWalshAmplitude
      f amplitude) :
  CryptBoolean.maxWalshMagnitude f =
    amplitude

The maximum Walsh magnitude is the amplitude supplied by a plateaued spectrum.

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedSupport.lean

complete

theorem CryptBoolean.sum_walshTransform_sq_walshSupport {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ a ∈ CryptBoolean.walshSupport f,
      ↑(CryptBoolean.walshTransform f a) ^ 2 =
    (2 ^ n) ^ 2

theorem CryptBoolean.sum_walshTransform_sq_walshSupport
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∑ a ∈ CryptBoolean.walshSupport f,
      ↑(CryptBoolean.walshTransform f a) ^
        2 =
    (2 ^ n) ^ 2

Parseval restricted to the nonzero Walsh support.

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedSupport.lean

complete

theorem CryptBoolean.two_pow_sq_le_card_walshSupport_mul_maxWalshMagnitude_sq
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  (2 ^ n) ^ 2 ≤
    ↑(CryptBoolean.walshSupport f).card *
      ↑(CryptBoolean.maxWalshMagnitude f) ^ 2

theorem CryptBoolean.two_pow_sq_le_card_walshSupport_mul_maxWalshMagnitude_sq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  (2 ^ n) ^ 2 ≤
    ↑(CryptBoolean.walshSupport f).card *
      ↑(CryptBoolean.maxWalshMagnitude
            f) ^
        2

Walsh support size times squared maximum magnitude dominates the Parseval mass.

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedSupport.lean

complete

theorem CryptBoolean.two_pow_sq_eq_card_walshSupport_mul_maxWalshMagnitude_sq_iff_plateaued
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  (2 ^ n) ^ 2 =
      ↑(CryptBoolean.walshSupport f).card *
        ↑(CryptBoolean.maxWalshMagnitude f) ^ 2 ↔
    CryptBoolean.IsPlateaued f

theorem CryptBoolean.two_pow_sq_eq_card_walshSupport_mul_maxWalshMagnitude_sq_iff_plateaued
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  (2 ^ n) ^ 2 =
      ↑(CryptBoolean.walshSupport
              f).card *
        ↑(CryptBoolean.maxWalshMagnitude
              f) ^
          2 ↔
    CryptBoolean.IsPlateaued f

Equality in the Walsh-support product bound characterizes plateaued functions.

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedSupport.lean

complete

theorem CryptBoolean.nonlinearity_cast_le_walshSupport_bound {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ n / 2 * (1 - (√↑(CryptBoolean.walshSupport f).card)⁻¹)

theorem CryptBoolean.nonlinearity_cast_le_walshSupport_bound
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ n / 2 *
      (1 -
        (√↑(CryptBoolean.walshSupport
                  f).card)⁻¹)

Carlet's support-size upper bound on nonlinearity.

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedSupport.lean

complete

theorem CryptBoolean.nonlinearity_cast_eq_walshSupport_bound_iff_plateaued
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
      2 ^ n / 2 * (1 - (√↑(CryptBoolean.walshSupport f).card)⁻¹) ↔
    CryptBoolean.IsPlateaued f

theorem CryptBoolean.nonlinearity_cast_eq_walshSupport_bound_iff_plateaued
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.nonlinearity f) =
      2 ^ n / 2 *
        (1 -
          (√↑(CryptBoolean.walshSupport
                    f).card)⁻¹) ↔
    CryptBoolean.IsPlateaued f

Equality in the Walsh-support nonlinearity bound holds exactly for plateaued functions.

Proposition5.13.10

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Proposition 5.11.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-6proposition-28relation-55page-106fidelity-exact

Proposition 28 (Carlet, Relation (55), p. 106). A Boolean function f:V_n\to\mathbb F_2 is plateaued if and only if there is a positive integer \lambda such that, for every x\in V_n, \sum_{a,b\in V_n}(-1)^{D_aD_bf(x)}=\lambda^2. The integer \lambda is the Walsh amplitude.

Lean code for Proposition5.13.10●2 theorems

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedSecondOrder.lean

complete

theorem CryptBoolean.hasPlateauedWalshAmplitude_iff_forall_walshTransform_cube_eq
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (amplitude : ℕ) :
  CryptBoolean.HasPlateauedWalshAmplitude f amplitude ↔
    0 < amplitude ∧
      ∀ (u : FABL.F₂Cube n),
        ↑(CryptBoolean.walshTransform f u) ^ 3 =
          ↑amplitude ^ 2 * ↑(CryptBoolean.walshTransform f u)

theorem CryptBoolean.hasPlateauedWalshAmplitude_iff_forall_walshTransform_cube_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (amplitude : ℕ) :
  CryptBoolean.HasPlateauedWalshAmplitude
      f amplitude ↔
    0 < amplitude ∧
      ∀ (u : FABL.F₂Cube n),
        ↑(CryptBoolean.walshTransform f
                u) ^
            3 =
          ↑amplitude ^ 2 *
            ↑(CryptBoolean.walshTransform
                f u)

A positive integer is the Walsh amplitude exactly when the raw Walsh
transform satisfies its corresponding cubic equation.

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedSecondOrder.lean

complete

theorem CryptBoolean.isPlateaued_iff_exists_forall_secondDerivativeDoubleSum_eq_sq
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsPlateaued f ↔
    ∃ amplitude,
      0 < amplitude ∧
        ∀ (x : FABL.F₂Cube n),
          CryptBoolean.secondDerivativeDoubleSum f x = ↑amplitude ^ 2

theorem CryptBoolean.isPlateaued_iff_exists_forall_secondDerivativeDoubleSum_eq_sq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsPlateaued f ↔
    ∃ amplitude,
      0 < amplitude ∧
        ∀ (x : FABL.F₂Cube n),
          CryptBoolean.secondDerivativeDoubleSum
              f x =
            ↑amplitude ^ 2

Carlet Proposition 28, Relation (55): a Boolean function is plateaued
exactly when all fixed-point double sums of second-derivative signs are the
same positive square.

Theorem5.13.11

Group: Chapter 5: Bent functions (69)

Group member previews

Preview

Definition 5.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 5

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-6plateauedorphanpage-106fidelity-source-correction-non-affine-hypothesis

Langevin's orphan theorem (Carlet, p. 106). Order the cosets of R(1,n) as follows: g+R(1,n) is below f+R(1,n) when there are minimum-weight representatives g_1 and f_1 of the respective cosets such that \operatorname{supp}(g_1)\subseteq\operatorname{supp}(f_1). A maximal coset for this order is called an orphan. If f is plateaued and f\notin R(1,n), then f+R(1,n) is an orphan. The non-affine hypothesis is necessary: affine functions are plateaued, while R(1,n) is the least coset in this order.

Lean code for Theorem5.13.11●6 declarations

defdefined in CryptBoolean/Carlet/Chapter06/PlateauedOrphan.lean

complete

def CryptBoolean.IsFirstOrderCosetLeader {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop

def CryptBoolean.IsFirstOrderCosetLeader
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop

A first-order coset leader is a representative whose weight realizes its
nonlinearity.

defdefined in CryptBoolean/Carlet/Chapter06/PlateauedOrphan.lean

complete

def CryptBoolean.FirstOrderCosetBelow {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) : Prop

def CryptBoolean.FirstOrderCosetBelow {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  Prop

The support order on first-order Reed--Muller cosets.

defdefined in CryptBoolean/Carlet/Chapter06/PlateauedOrphan.lean

complete

def CryptBoolean.IsFirstOrderOrphan {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop

def CryptBoolean.IsFirstOrderOrphan {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop

A first-order Reed--Muller coset is an orphan when it is maximal in the
coset-leader support order.

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedOrphan.lean

complete

theorem CryptBoolean.IsPlateaued.add_affineFunction {n : ℕ}
  {f : CryptBoolean.BooleanFunction n} (hf : CryptBoolean.IsPlateaued f)
  (b : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  CryptBoolean.IsPlateaued (f + FABL.affineFunction b a)

theorem CryptBoolean.IsPlateaued.add_affineFunction
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf : CryptBoolean.IsPlateaued f)
  (b : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  CryptBoolean.IsPlateaued
    (f + FABL.affineFunction b a)

Adding an affine function preserves plateauedness.

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedOrphan.lean

complete

theorem CryptBoolean.eq_of_plateaued_cosetLeaders_of_support_subset {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsPlateaued f)
  (hnonlinearity : 0 < CryptBoolean.nonlinearity f)
  (hleaderF : CryptBoolean.IsFirstOrderCosetLeader f)
  (hleaderG : CryptBoolean.IsFirstOrderCosetLeader g)
  (hsubset : CryptBoolean.support f ⊆ CryptBoolean.support g) : g = f

theorem CryptBoolean.eq_of_plateaued_cosetLeaders_of_support_subset
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsPlateaued f)
  (hnonlinearity :
    0 < CryptBoolean.nonlinearity f)
  (hleaderF :
    CryptBoolean.IsFirstOrderCosetLeader
      f)
  (hleaderG :
    CryptBoolean.IsFirstOrderCosetLeader
      g)
  (hsubset :
    CryptBoolean.support f ⊆
      CryptBoolean.support g) :
  g = f

A non-affine plateaued coset leader cannot have its support properly
contained in the support of another first-order coset leader.

theoremdefined in CryptBoolean/Carlet/Chapter06/PlateauedOrphan.lean

complete

theorem CryptBoolean.isFirstOrderOrphan_of_isPlateaued {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsPlateaued f)
  (hnonaffine : f ∉ CryptBoolean.reedMuller 1 n) :
  CryptBoolean.IsFirstOrderOrphan f

theorem CryptBoolean.isFirstOrderOrphan_of_isPlateaued
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsPlateaued f)
  (hnonaffine :
    f ∉ CryptBoolean.reedMuller 1 n) :
  CryptBoolean.IsFirstOrderOrphan f

Langevin's corrected orphan theorem: every non-affine plateaued function
represents a maximal first-order Reed--Muller coset.