Cryptographic Boolean Functions in Lean

5.11. Characterization by second-order covering sequences🔗

Proposition5.11.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 6
Statement dependency previews
Preview
Definition 1.8.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 5.7.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6proposition-24relation-52second-order-covering-sequencesection-6-6-3page-100fidelity-exact

Proposition 24 (Carlet, Relation (52), p. 100). A Boolean function f:V_n\to\mathbb F_2 is bent if and only if, for every x\in V_n, \sum_{a,b\in V_n}(-1)^{D_aD_bf(x)}=2^n. Equivalently, for the sign function f_\chi=(-1)^f, f_\chi\otimes f_\chi\otimes f_\chi=2^nf_\chi, or, at every u\in V_n, W_f(u)^3=2^nW_f(u).

Lean code for Proposition5.11.1●10 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/SecondOrderCharacterization.lean
    complete
    def CryptBoolean.secondDerivativeDoubleSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) : ℝ
    def CryptBoolean.secondDerivativeDoubleSum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) : ℝ
    The double sum of the signs of all second derivatives at a fixed point.
  • defdefined in CryptBoolean/Carlet/Chapter06/SecondOrderCharacterization.lean
    complete
    def CryptBoolean.rawTripleConvolution {n : ℕ} (φ : FABL.F₂Cube n → ℝ) :
  FABL.F₂Cube n → ℝ
    def CryptBoolean.rawTripleConvolution {n : ℕ}
  (φ : FABL.F₂Cube n → ℝ) :
  FABL.F₂Cube n → ℝ
    The unnormalized threefold additive convolution of a real cube function.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondOrderCharacterization.lean
    complete
    theorem CryptBoolean.secondDerivativeDoubleSum_eq_mul_rawTripleConvolution
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) :
  CryptBoolean.secondDerivativeDoubleSum f x =
    CryptBoolean.realSignView f x *
      CryptBoolean.rawTripleConvolution (CryptBoolean.realSignView f) x
    theorem CryptBoolean.secondDerivativeDoubleSum_eq_mul_rawTripleConvolution
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  CryptBoolean.secondDerivativeDoubleSum f
      x =
    CryptBoolean.realSignView f x *
      CryptBoolean.rawTripleConvolution
        (CryptBoolean.realSignView f) x
    The fixed-point second-derivative sum is the sign view times its threefold
raw convolution.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondOrderCharacterization.lean
    complete
    theorem CryptBoolean.rawFourierTransform_rawTripleConvolution {n : ℕ}
  (φ : FABL.F₂Cube n → ℝ) (u : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform (CryptBoolean.rawTripleConvolution φ)
      u =
    CryptBoolean.rawFourierTransform φ u ^ 3
    theorem CryptBoolean.rawFourierTransform_rawTripleConvolution
  {n : ℕ} (φ : FABL.F₂Cube n → ℝ)
  (u : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (CryptBoolean.rawTripleConvolution
        φ)
      u =
    CryptBoolean.rawFourierTransform φ u ^
      3
    The raw Fourier transform sends threefold raw convolution to a cube.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondOrderCharacterization.lean
    complete
    theorem CryptBoolean.rawFourierTransform_const_mul_realSignView {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (c : ℝ) (u : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (fun x => c * CryptBoolean.realSignView f x) u =
    c * ↑(CryptBoolean.walshTransform f u)
    theorem CryptBoolean.rawFourierTransform_const_mul_realSignView
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (c : ℝ) (u : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (fun x =>
        c * CryptBoolean.realSignView f x)
      u =
    c * ↑(CryptBoolean.walshTransform f u)
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondOrderCharacterization.lean
    complete
    theorem CryptBoolean.eq_of_rawFourierTransform_eq {n : ℕ}
  (φ ψ : FABL.F₂Cube n → ℝ)
  (h :
    CryptBoolean.rawFourierTransform φ =
      CryptBoolean.rawFourierTransform ψ) :
  φ = ψ
    theorem CryptBoolean.eq_of_rawFourierTransform_eq
  {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ)
  (h :
    CryptBoolean.rawFourierTransform φ =
      CryptBoolean.rawFourierTransform
        ψ) :
  φ = ψ
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondOrderCharacterization.lean
    complete
    theorem CryptBoolean.isBent_iff_forall_secondDerivativeDoubleSum_eq_two_pow
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    ∀ (x : FABL.F₂Cube n),
      CryptBoolean.secondDerivativeDoubleSum f x = 2 ^ n
    theorem CryptBoolean.isBent_iff_forall_secondDerivativeDoubleSum_eq_two_pow
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    ∀ (x : FABL.F₂Cube n),
      CryptBoolean.secondDerivativeDoubleSum
          f x =
        2 ^ n
    Carlet Proposition 24: bentness is equivalent to the fixed-point double
sum of second-derivative signs being exactly `2^n` at every point.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondOrderCharacterization.lean
    complete
    theorem CryptBoolean.secondDerivativeDoubleSum_eq_two_pow_iff_rawTripleConvolution_eq
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) :
  CryptBoolean.secondDerivativeDoubleSum f x = 2 ^ n ↔
    CryptBoolean.rawTripleConvolution (CryptBoolean.realSignView f) x =
      2 ^ n * CryptBoolean.realSignView f x
    theorem CryptBoolean.secondDerivativeDoubleSum_eq_two_pow_iff_rawTripleConvolution_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  CryptBoolean.secondDerivativeDoubleSum f
        x =
      2 ^ n ↔
    CryptBoolean.rawTripleConvolution
        (CryptBoolean.realSignView f) x =
      2 ^ n *
        CryptBoolean.realSignView f x
    At a fixed point, the second-derivative sum condition is equivalent to
the corresponding value of the threefold raw convolution.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondOrderCharacterization.lean
    complete
    theorem CryptBoolean.isBent_iff_rawTripleConvolution_realSignView_eq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.rawTripleConvolution (CryptBoolean.realSignView f) =
      fun x => 2 ^ n * CryptBoolean.realSignView f x
    theorem CryptBoolean.isBent_iff_rawTripleConvolution_realSignView_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.rawTripleConvolution
        (CryptBoolean.realSignView f) =
      fun x =>
      2 ^ n *
        CryptBoolean.realSignView f x
    Bentness is equivalent to the threefold raw convolution eigenvalue
identity for the sign view.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondOrderCharacterization.lean
    complete
    theorem CryptBoolean.isBent_iff_forall_walshTransform_cube_eq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    ∀ (u : FABL.F₂Cube n),
      CryptBoolean.walshTransform f u ^ 3 =
        2 ^ n * CryptBoolean.walshTransform f u
    theorem CryptBoolean.isBent_iff_forall_walshTransform_cube_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    ∀ (u : FABL.F₂Cube n),
      CryptBoolean.walshTransform f u ^
          3 =
        2 ^ n *
          CryptBoolean.walshTransform f u
    The frequency-domain form of Proposition 24: bentness is equivalent to
the cubic raw Walsh identity at every frequency.