Cryptographic Boolean Functions in Lean

4.3. Indicators of flats🔗

Theorem4.3.1

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.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 1✓L∃∀N

Tagscarletchapter-5affine-flat-indicatorwalsh-spectrumnonlinearitypage-71fidelity-corrected-codimension-one

Affine-flat indicator spectrum (Carlet, Section 5.3, p. 71). Let 1\le r\le n, let a_1,\ldots,a_r\in V_n be linearly independent, and let \epsilon_1,\ldots,\epsilon_r\in\mathbb F_2. For the codimension-r affine flat A=\{x\in V_n:a_i\mathbin\cdot x=\epsilon_i+1\text{ for every }i\}, its indicator is f(x)=\prod_{i=1}^r(a_i\mathbin\cdot x+\epsilon_i), \qquad w_H(f)=2^{n-r}. If u\notin\operatorname{span}\{a_1,\ldots,a_r\}, then W_f(u)=0. If 0\ne u=\sum_i\eta_i a_i, then W_f(u)=-2^{n-r+1}(-1)^{\sum_i\eta_i(\epsilon_i+1)}, while W_f(0)=2^n-2^{n-r+1}. Consequently, \operatorname{nl}(f)= \begin{cases} 0,&r=1,\\ 2^{n-r},&r\ge2. \end{cases}

Lean code for Theorem4.3.1●9 theorems

theoremdefined in CryptBoolean/Carlet/Chapter02/Subspaces.lean

complete

theorem CryptBoolean.rawFourierTransform_setIndicator_binaryAffineSubspace
  {n : ℕ} (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (u a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.setIndicator ↑(FABL.binaryAffineSubspace H u)) a =
    (FABL.vectorWalshCharacter a) u *
      if a ∈ FABL.perpendicularSubspace H then ↑(Nat.card ↥H) else 0

theorem CryptBoolean.rawFourierTransform_setIndicator_binaryAffineSubspace
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (u a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.setIndicator
        ↑(FABL.binaryAffineSubspace H u))
      a =
    (FABL.vectorWalshCharacter a) u *
      if
          a ∈
            FABL.perpendicularSubspace
              H then
        ↑(Nat.card ↥H)
      else 0

The raw transform of an affine-subspace indicator is the direction's
cardinality on its perpendicular, modulated by the translation character.

theoremdefined in CryptBoolean/Carlet/Chapter05/FlatIndicators.lean

complete

theorem CryptBoolean.realSignView_affineFlatIndicator {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a x : FABL.F₂Cube n) :
  CryptBoolean.realSignView (CryptBoolean.affineFlatIndicator H a) x =
    1 - 2 * FABL.setIndicator (↑(FABL.binaryAffineSubspace H a)) x

theorem CryptBoolean.realSignView_affineFlatIndicator
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a x : FABL.F₂Cube n) :
  CryptBoolean.realSignView
      (CryptBoolean.affineFlatIndicator H
        a)
      x =
    1 -
      2 *
        FABL.setIndicator
          (↑(FABL.binaryAffineSubspace H
              a))
          x

The sign view of an affine-flat indicator is one minus twice its real
set indicator.

theoremdefined in CryptBoolean/Carlet/Chapter05/FlatIndicators.lean

complete

theorem CryptBoolean.walshTransform_affineFlatIndicator {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform (CryptBoolean.affineFlatIndicator H a) u =
    if u = 0 then 2 ^ n - 2 * ↑(Nat.card ↥H)
    else
      if u ∈ FABL.perpendicularSubspace H then
        -2 * CryptBoolean.bitSignInt (FABL.f₂DotProduct u a) *
          ↑(Nat.card ↥H)
      else 0

theorem CryptBoolean.walshTransform_affineFlatIndicator
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform
      (CryptBoolean.affineFlatIndicator H
        a)
      u =
    if u = 0 then
      2 ^ n - 2 * ↑(Nat.card ↥H)
    else
      if
          u ∈
            FABL.perpendicularSubspace
              H then
        -2 *
            CryptBoolean.bitSignInt
              (FABL.f₂DotProduct u a) *
          ↑(Nat.card ↥H)
      else 0

Carlet Section 5.3: the affine-flat indicator has a three-case raw Walsh
spectrum, supported on the perpendicular direction.

theoremdefined in CryptBoolean/Carlet/Chapter05/FlatIndicators.lean

complete

theorem CryptBoolean.maxWalshMagnitude_affineFlatIndicator_of_two_le_codimension
  {n : ℕ} (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (hcodim : 2 ≤ FABL.f₂Codimension H) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.affineFlatIndicator H a) =
    2 ^ n - 2 * Nat.card ↥H

theorem CryptBoolean.maxWalshMagnitude_affineFlatIndicator_of_two_le_codimension
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (hcodim : 2 ≤ FABL.f₂Codimension H) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.affineFlatIndicator H
        a) =
    2 ^ n - 2 * Nat.card ↥H

In codimension at least two, the zero-frequency coefficient is the
largest absolute Walsh coefficient of an affine-flat indicator.

theoremdefined in CryptBoolean/Carlet/Chapter05/FlatIndicators.lean

complete

theorem CryptBoolean.nonlinearity_affineFlatIndicator_of_two_le_codimension
  {n : ℕ} (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (hcodim : 2 ≤ FABL.f₂Codimension H) :
  CryptBoolean.nonlinearity (CryptBoolean.affineFlatIndicator H a) =
    Nat.card ↥H

theorem CryptBoolean.nonlinearity_affineFlatIndicator_of_two_le_codimension
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (hcodim : 2 ≤ FABL.f₂Codimension H) :
  CryptBoolean.nonlinearity
      (CryptBoolean.affineFlatIndicator H
        a) =
    Nat.card ↥H

Carlet Section 5.3: an affine-flat indicator of codimension at least two
has nonlinearity equal to the cardinality of its flat.

theoremdefined in CryptBoolean/Carlet/Chapter05/FlatIndicators.lean

complete

theorem CryptBoolean.nonlinearity_affineFlatIndicator_of_codimension_le_one
  {n : ℕ} (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (hcodim : FABL.f₂Codimension H ≤ 1) :
  CryptBoolean.nonlinearity (CryptBoolean.affineFlatIndicator H a) = 0

theorem CryptBoolean.nonlinearity_affineFlatIndicator_of_codimension_le_one
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (hcodim : FABL.f₂Codimension H ≤ 1) :
  CryptBoolean.nonlinearity
      (CryptBoolean.affineFlatIndicator H
        a) =
    0

An affine-flat indicator of codimension at most one is affine and hence
has zero nonlinearity.

theoremdefined in CryptBoolean/Carlet/Chapter05/FlatIndicators.lean

complete

theorem CryptBoolean.nonlinearity_affineFlatIndicator {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  CryptBoolean.nonlinearity (CryptBoolean.affineFlatIndicator H a) =
    if FABL.f₂Codimension H ≤ 1 then 0 else Nat.card ↥H

theorem CryptBoolean.nonlinearity_affineFlatIndicator
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  CryptBoolean.nonlinearity
      (CryptBoolean.affineFlatIndicator H
        a) =
    if FABL.f₂Codimension H ≤ 1 then 0
    else Nat.card ↥H

Carlet Section 5.3 with the codimension-one exception made explicit: an
affine-flat indicator has zero nonlinearity in codimension zero or one and
otherwise has nonlinearity equal to the flat cardinality.

theoremdefined in CryptBoolean/Carlet/Chapter05/FlatIndicators.lean

complete

theorem CryptBoolean.nonlinearity_affineFlatIndicator_of_codimension_one {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (hcodim : FABL.f₂Codimension H = 1) :
  CryptBoolean.nonlinearity (CryptBoolean.affineFlatIndicator H a) = 0

theorem CryptBoolean.nonlinearity_affineFlatIndicator_of_codimension_one
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n)
  (hcodim : FABL.f₂Codimension H = 1) :
  CryptBoolean.nonlinearity
      (CryptBoolean.affineFlatIndicator H
        a) =
    0

The codimension-one case printed implicitly in Carlet's spectrum formula
has zero nonlinearity.

theoremdefined in CryptBoolean/Carlet/Chapter05/FlatIndicators.lean

complete

theorem CryptBoolean.nonlinearity_affineFlatIndicator_of_finrank_eq {n : ℕ}
  (r : ℕ) (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n)
  (hrn : r ≤ n) (hfinrank : Module.finrank FABL.𝔽₂ ↥H = n - r) :
  CryptBoolean.nonlinearity (CryptBoolean.affineFlatIndicator H a) =
    if r ≤ 1 then 0 else 2 ^ (n - r)

theorem CryptBoolean.nonlinearity_affineFlatIndicator_of_finrank_eq
  {n : ℕ} (r : ℕ)
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) (hrn : r ≤ n)
  (hfinrank :
    Module.finrank FABL.𝔽₂ ↥H = n - r) :
  CryptBoolean.nonlinearity
      (CryptBoolean.affineFlatIndicator H
        a) =
    if r ≤ 1 then 0 else 2 ^ (n - r)

Dimension form of the complete affine-flat-indicator nonlinearity
formula.

For r=1 the indicator is affine and has nonlinearity zero. Thus the printed value \operatorname{nl}(f)=2^{n-r} follows from the stated Walsh formula precisely when r\ge2.