Cryptographic Boolean Functions in Lean

5.7. Decompositions of bent functions🔗

Theorem5.7.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 2
Statement dependency previews
Preview
Proposition 1.10.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Corollary 5.7.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6theorem-11pages-95-96fidelity-exact

Theorem 11 (Carlet, pp. 95--96). Let n\ge4 be even and let f:V_n\to\mathbb F_2. For a linear hyperplane E, identify E and its complementary coset with V_{n-1} and denote the two restrictions by h_0,h_1. The following are equivalent:

  1. f is bent;

  2. for every linear hyperplane, and equivalently for at least one linear hyperplane, the transforms W_{h_0} and W_{h_1} take values in \{0,\pm2^{n/2}\}, and at every frequency exactly one is nonzero.

Lean code for Theorem5.7.1●14 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    def CryptBoolean.singletonF₂Cube (b : FABL.𝔽₂) : FABL.F₂Cube 1
    def CryptBoolean.singletonF₂Cube
  (b : FABL.𝔽₂) : FABL.F₂Cube 1
    The one-dimensional binary cube point with prescribed coordinate.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.singletonF₂Cube_apply (b : FABL.𝔽₂) (i : Fin 1) :
  CryptBoolean.singletonF₂Cube b i = b
    theorem CryptBoolean.singletonF₂Cube_apply
  (b : FABL.𝔽₂) (i : Fin 1) :
  CryptBoolean.singletonF₂Cube b i = b
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    def CryptBoolean.singletonF₂CubeLinearEquiv :
  FABL.𝔽₂ ≃ₗ[FABL.𝔽₂] FABL.F₂Cube 1
    def CryptBoolean.singletonF₂CubeLinearEquiv :
  FABL.𝔽₂ ≃ₗ[FABL.𝔽₂] FABL.F₂Cube 1
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.sum_singletonF₂Cube.{u_1} {R : Type u_1} [AddCommMonoid R]
  (g : FABL.F₂Cube 1 → R) :
  ∑ y, g y =
    g (CryptBoolean.singletonF₂Cube 0) +
      g (CryptBoolean.singletonF₂Cube 1)
    theorem CryptBoolean.sum_singletonF₂Cube.{u_1}
  {R : Type u_1} [AddCommMonoid R]
  (g : FABL.F₂Cube 1 → R) :
  ∑ y, g y =
    g (CryptBoolean.singletonF₂Cube 0) +
      g (CryptBoolean.singletonF₂Cube 1)
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.walshTransform_append_singletonF₂Cube {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + 1)) (a : FABL.F₂Cube n)
  (b : FABL.𝔽₂) :
  CryptBoolean.walshTransform f
      (Fin.append a (CryptBoolean.singletonF₂Cube b)) =
    CryptBoolean.walshTransform
        (CryptBoolean.firstBlockSlice f
          (CryptBoolean.singletonF₂Cube 0))
        a +
      CryptBoolean.bitSignInt b *
        CryptBoolean.walshTransform
          (CryptBoolean.firstBlockSlice f
            (CryptBoolean.singletonF₂Cube 1))
          a
    theorem CryptBoolean.walshTransform_append_singletonF₂Cube
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (a : FABL.F₂Cube n) (b : FABL.𝔽₂) :
  CryptBoolean.walshTransform f
      (Fin.append a
        (CryptBoolean.singletonF₂Cube
          b)) =
    CryptBoolean.walshTransform
        (CryptBoolean.firstBlockSlice f
          (CryptBoolean.singletonF₂Cube
            0))
        a +
      CryptBoolean.bitSignInt b *
        CryptBoolean.walshTransform
          (CryptBoolean.firstBlockSlice f
            (CryptBoolean.singletonF₂Cube
              1))
          a
    Splitting the last coordinate expresses an ambient Walsh coefficient as
the signed sum of the Walsh coefficients of the two hyperplane restrictions.
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    def CryptBoolean.linearHyperplaneRestriction {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + 1))
  (L : FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube (n + 1))
  (b : FABL.𝔽₂) : CryptBoolean.BooleanFunction n
    def CryptBoolean.linearHyperplaneRestriction
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (L :
    FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube (n + 1))
  (b : FABL.𝔽₂) :
  CryptBoolean.BooleanFunction n
    The two coordinate restrictions determined by a linear change of
variables represent a linear hyperplane and its complementary affine coset.
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    def CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + 1))
  (L : FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube (n + 1)) : Prop
    def CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (L :
    FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube (n + 1)) :
  Prop
    The two hyperplane restrictions have complementary spectra of amplitude
`2^((n+1)/2)` when at every frequency exactly one coefficient is nonzero and
that coefficient has this magnitude.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.isBent_iff_hasComplementaryHyperplaneRestrictionSpectra
  {n : ℕ} (f : CryptBoolean.BooleanFunction (n + 1))
  (L : FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube (n + 1))
  (_hnEven : Even (n + 1)) (_hnFour : 4 ≤ n + 1) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra f L
    theorem CryptBoolean.isBent_iff_hasComplementaryHyperplaneRestrictionSpectra
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (L :
    FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube (n + 1))
  (_hnEven : Even (n + 1))
  (_hnFour : 4 ≤ n + 1) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra
      f L
    Carlet Theorem 11 for a fixed linear hyperplane: in even ambient
dimension at least four, bentness is equivalent to complementary restriction
spectra with values `0` and `±2^((n+1)/2)`.
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    def CryptBoolean.hyperplaneExtension {n : ℕ}
  (h₀ h₁ : CryptBoolean.BooleanFunction n) :
  CryptBoolean.BooleanFunction (n + 1)
    def CryptBoolean.hyperplaneExtension {n : ℕ}
  (h₀ h₁ :
    CryptBoolean.BooleanFunction n) :
  CryptBoolean.BooleanFunction (n + 1)
    The Boolean function obtained by placing `h₀` and `h₁` on the two
cosets of the standard coordinate hyperplane.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.hyperplaneExtension_append_singletonF₂Cube {n : ℕ}
  (h₀ h₁ : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n)
  (b : FABL.𝔽₂) :
  CryptBoolean.hyperplaneExtension h₀ h₁
      (Fin.append x (CryptBoolean.singletonF₂Cube b)) =
    if b = 0 then h₀ x else h₁ x
    theorem CryptBoolean.hyperplaneExtension_append_singletonF₂Cube
  {n : ℕ}
  (h₀ h₁ : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) (b : FABL.𝔽₂) :
  CryptBoolean.hyperplaneExtension h₀ h₁
      (Fin.append x
        (CryptBoolean.singletonF₂Cube
          b)) =
    if b = 0 then h₀ x else h₁ x
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.linearHyperplaneRestriction_hyperplaneExtension_refl
  {n : ℕ} (h₀ h₁ : CryptBoolean.BooleanFunction n) (b : FABL.𝔽₂) :
  CryptBoolean.linearHyperplaneRestriction
      (CryptBoolean.hyperplaneExtension h₀ h₁)
      (LinearEquiv.refl FABL.𝔽₂ (FABL.F₂Cube (n + 1))) b =
    if b = 0 then h₀ else h₁
    theorem CryptBoolean.linearHyperplaneRestriction_hyperplaneExtension_refl
  {n : ℕ}
  (h₀ h₁ : CryptBoolean.BooleanFunction n)
  (b : FABL.𝔽₂) :
  CryptBoolean.linearHyperplaneRestriction
      (CryptBoolean.hyperplaneExtension h₀
        h₁)
      (LinearEquiv.refl FABL.𝔽₂
        (FABL.F₂Cube (n + 1)))
      b =
    if b = 0 then h₀ else h₁
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.isBent_hyperplaneExtension_of_complementaryWalshSpectra
  {n : ℕ} (h₀ h₁ : CryptBoolean.BooleanFunction n)
  (hnEven : Even (n + 1)) (hnFour : 4 ≤ n + 1)
  (hspectra :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform h₀ a = 0 ∧
          (CryptBoolean.walshTransform h₁ a).natAbs =
            2 ^ ((n + 1) / 2) ∨
        (CryptBoolean.walshTransform h₀ a).natAbs = 2 ^ ((n + 1) / 2) ∧
          CryptBoolean.walshTransform h₁ a = 0) :
  CryptBoolean.IsBent (CryptBoolean.hyperplaneExtension h₀ h₁)
    theorem CryptBoolean.isBent_hyperplaneExtension_of_complementaryWalshSpectra
  {n : ℕ}
  (h₀ h₁ : CryptBoolean.BooleanFunction n)
  (hnEven : Even (n + 1))
  (hnFour : 4 ≤ n + 1)
  (hspectra :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform h₀ a =
            0 ∧
          (CryptBoolean.walshTransform h₁
                a).natAbs =
            2 ^ ((n + 1) / 2) ∨
        (CryptBoolean.walshTransform h₀
                a).natAbs =
            2 ^ ((n + 1) / 2) ∧
          CryptBoolean.walshTransform h₁
              a =
            0) :
  CryptBoolean.IsBent
    (CryptBoolean.hyperplaneExtension h₀
      h₁)
    Complementary Walsh spectra of amplitude `2^((n+1)/2)` give a bent
extension across the standard hyperplane.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.isBent_iff_forall_hasComplementaryHyperplaneRestrictionSpectra
  {n : ℕ} (f : CryptBoolean.BooleanFunction (n + 1))
  (hnEven : Even (n + 1)) (hnFour : 4 ≤ n + 1) :
  CryptBoolean.IsBent f ↔
    ∀ (L : FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube (n + 1)),
      CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra f L
    theorem CryptBoolean.isBent_iff_forall_hasComplementaryHyperplaneRestrictionSpectra
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (hnEven : Even (n + 1))
  (hnFour : 4 ≤ n + 1) :
  CryptBoolean.IsBent f ↔
    ∀
      (L :
        FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂]
          FABL.F₂Cube (n + 1)),
      CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra
        f L
    In Theorem 11, a bent function has the complementary restriction property
for every linear hyperplane coordinate system.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.isBent_iff_exists_hasComplementaryHyperplaneRestrictionSpectra
  {n : ℕ} (f : CryptBoolean.BooleanFunction (n + 1))
  (hnEven : Even (n + 1)) (hnFour : 4 ≤ n + 1) :
  CryptBoolean.IsBent f ↔
    ∃ L, CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra f L
    theorem CryptBoolean.isBent_iff_exists_hasComplementaryHyperplaneRestrictionSpectra
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (hnEven : Even (n + 1))
  (hnFour : 4 ≤ n + 1) :
  CryptBoolean.IsBent f ↔
    ∃ L,
      CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra
        f L
    In Theorem 11, it is enough that one linear hyperplane coordinate system
has complementary restriction spectra.
Corollary5.7.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
Theorem 3.2.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6hyperplane-restrictionpage-96fidelity-exact

Hyperplane-restriction consequence (Carlet, p. 96). Every restriction of an n-variable bent function to an affine hyperplane, with n\ge4 even, is plateaued on V_{n-1} with amplitude 2^{n/2} and has the optimal odd-dimensional nonlinearity 2^{n-2}-2^{(n-2)/2}.

Lean code for Corollary5.7.2●3 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.hasPlateauedWalshAmplitude_linearHyperplaneRestriction_of_isBent
  {n : ℕ} (f : CryptBoolean.BooleanFunction (n + 1))
  (L : FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube (n + 1))
  (hf : CryptBoolean.IsBent f) (hnEven : Even (n + 1))
  (hnFour : 4 ≤ n + 1) (b : FABL.𝔽₂) :
  CryptBoolean.HasPlateauedWalshAmplitude
    (CryptBoolean.linearHyperplaneRestriction f L b) (2 ^ ((n + 1) / 2))
    theorem CryptBoolean.hasPlateauedWalshAmplitude_linearHyperplaneRestriction_of_isBent
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (L :
    FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube (n + 1))
  (hf : CryptBoolean.IsBent f)
  (hnEven : Even (n + 1))
  (hnFour : 4 ≤ n + 1) (b : FABL.𝔽₂) :
  CryptBoolean.HasPlateauedWalshAmplitude
    (CryptBoolean.linearHyperplaneRestriction
      f L b)
    (2 ^ ((n + 1) / 2))
    Each affine-hyperplane restriction of a bent function in even ambient
dimension at least four is plateaued with the optimal odd-dimensional
amplitude.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.isPlateaued_linearHyperplaneRestriction_of_isBent {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + 1))
  (L : FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube (n + 1))
  (hf : CryptBoolean.IsBent f) (hnEven : Even (n + 1))
  (hnFour : 4 ≤ n + 1) (b : FABL.𝔽₂) :
  CryptBoolean.IsPlateaued
    (CryptBoolean.linearHyperplaneRestriction f L b)
    theorem CryptBoolean.isPlateaued_linearHyperplaneRestriction_of_isBent
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (L :
    FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube (n + 1))
  (hf : CryptBoolean.IsBent f)
  (hnEven : Even (n + 1))
  (hnFour : 4 ≤ n + 1) (b : FABL.𝔽₂) :
  CryptBoolean.IsPlateaued
    (CryptBoolean.linearHyperplaneRestriction
      f L b)
    Every affine-hyperplane restriction of a bent function is plateaued.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean
    complete
    theorem CryptBoolean.nonlinearity_linearHyperplaneRestriction_of_isBent {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + 1))
  (L : FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube (n + 1))
  (hf : CryptBoolean.IsBent f) (hnEven : Even (n + 1))
  (hnFour : 4 ≤ n + 1) (b : FABL.𝔽₂) :
  CryptBoolean.nonlinearity
      (CryptBoolean.linearHyperplaneRestriction f L b) =
    2 ^ (n - 1) - 2 ^ ((n - 1) / 2)
    theorem CryptBoolean.nonlinearity_linearHyperplaneRestriction_of_isBent
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (L :
    FABL.F₂Cube (n + 1) ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube (n + 1))
  (hf : CryptBoolean.IsBent f)
  (hnEven : Even (n + 1))
  (hnFour : 4 ≤ n + 1) (b : FABL.𝔽₂) :
  CryptBoolean.nonlinearity
      (CryptBoolean.linearHyperplaneRestriction
        f L b) =
    2 ^ (n - 1) - 2 ^ ((n - 1) / 2)
    The affine-hyperplane restrictions of an even-dimensional bent function
have optimal odd-dimensional nonlinearity.
Theorem5.7.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.
Statement uses 2
Statement dependency previews
Preview
Theorem 5.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6decompositionpage-97fidelity-exact-coordinate-identification

Balanced derivatives along a hyperplane (Carlet, p. 97). Let f:V_{2k+1}\to\mathbb F_2, and let E be a linear hyperplane. If D_u f is balanced for every nonzero u\in E, then the restrictions of f to E and to its complementary coset are bent.

Lean code for Theorem5.7.3●1 theorem
  • theoremdefined in CryptBoolean/Carlet/Chapter06/AdditionalDecompositions.lean
    complete
    theorem CryptBoolean.isBent_linearHyperplaneRestriction_of_balanced_derivatives
  (k : ℕ) (f : CryptBoolean.BooleanFunction (2 * k + 1))
  (L : FABL.F₂Cube (2 * k + 1) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube (2 * k + 1))
  (hbalanced :
    ∀ (u : FABL.F₂Cube (2 * k)),
      u ≠ 0 →
        CryptBoolean.IsBalanced
          (FABL.booleanDerivative f
            (L (Fin.append u (CryptBoolean.singletonF₂Cube 0)))))
  (b : FABL.𝔽₂) :
  CryptBoolean.IsBent (CryptBoolean.linearHyperplaneRestriction f L b)
    theorem CryptBoolean.isBent_linearHyperplaneRestriction_of_balanced_derivatives
  (k : ℕ)
  (f :
    CryptBoolean.BooleanFunction
      (2 * k + 1))
  (L :
    FABL.F₂Cube (2 * k + 1) ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube (2 * k + 1))
  (hbalanced :
    ∀ (u : FABL.F₂Cube (2 * k)),
      u ≠ 0 →
        CryptBoolean.IsBalanced
          (FABL.booleanDerivative f
            (L
              (Fin.append u
                (CryptBoolean.singletonF₂Cube
                  0)))))
  (b : FABL.𝔽₂) :
  CryptBoolean.IsBent
    (CryptBoolean.linearHyperplaneRestriction
      f L b)
    If every nonzero derivative in a hyperplane is balanced, both coset
restrictions are bent.
Theorem5.7.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 4
Statement dependency previews
Preview
Definition 5.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6decompositionpage-97fidelity-exact-coordinate-identification

Restrictions to four codimension-two cosets (Carlet, p. 97). Let f be bent on V_N, with N even, and let E\le V_N have codimension two. The four restrictions of f to the cosets of E, viewed in any fixed linear coordinate identification with V_{N-2}, have the same set of Walsh magnitudes. If E^\perp=\langle a,b\rangle, then all four restrictions are bent if and only if D_aD_b\widetilde f=1.

Lean code for Theorem5.7.4●4 declarations
  • theoremdefined in CryptBoolean/Carlet/Chapter06/AdditionalDecompositions.lean
    complete
    theorem CryptBoolean.four_mul_walshTransform_firstBlockSlice_eq {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + 2))
  (hf : CryptBoolean.IsBent f) (a : FABL.F₂Cube n) (y : FABL.F₂Cube 2) :
  4 *
      ↑(CryptBoolean.walshTransform (CryptBoolean.firstBlockSlice f y)
          a) =
    2 ^ ((n + 2) / 2) *
      ↑(CryptBoolean.walshTransform
          (CryptBoolean.secondBlockSlice (CryptBoolean.bentDual f) a) y)
    theorem CryptBoolean.four_mul_walshTransform_firstBlockSlice_eq
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 2))
  (hf : CryptBoolean.IsBent f)
  (a : FABL.F₂Cube n)
  (y : FABL.F₂Cube 2) :
  4 *
      ↑(CryptBoolean.walshTransform
          (CryptBoolean.firstBlockSlice f
            y)
          a) =
    2 ^ ((n + 2) / 2) *
      ↑(CryptBoolean.walshTransform
          (CryptBoolean.secondBlockSlice
            (CryptBoolean.bentDual f) a)
          y)
    The Walsh coefficient of a codimension-two restriction is the two-bit
Walsh coefficient of the corresponding dual slice, with exact raw scaling.
  • defdefined in CryptBoolean/Carlet/Chapter06/AdditionalDecompositions.lean
    complete
    def CryptBoolean.walshMagnitudeSet {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Finset ℕ
    def CryptBoolean.walshMagnitudeSet {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Finset ℕ
    The set of magnitudes occurring in the raw Walsh spectrum.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/AdditionalDecompositions.lean
    complete
    theorem CryptBoolean.walshMagnitudeSet_firstBlockSlice_eq {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + 2))
  (hf : CryptBoolean.IsBent f) (hn : Even n) (y z : FABL.F₂Cube 2) :
  CryptBoolean.walshMagnitudeSet (CryptBoolean.firstBlockSlice f y) =
    CryptBoolean.walshMagnitudeSet (CryptBoolean.firstBlockSlice f z)
    theorem CryptBoolean.walshMagnitudeSet_firstBlockSlice_eq
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 2))
  (hf : CryptBoolean.IsBent f)
  (hn : Even n) (y z : FABL.F₂Cube 2) :
  CryptBoolean.walshMagnitudeSet
      (CryptBoolean.firstBlockSlice f y) =
    CryptBoolean.walshMagnitudeSet
      (CryptBoolean.firstBlockSlice f z)
    The four codimension-two coordinate restrictions of a bent function have
the same set of raw Walsh magnitudes.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/AdditionalDecompositions.lean
    complete
    theorem CryptBoolean.isBent_firstBlockSlices_iff_bentDual_secondDerivative_eq_one
  {n : ℕ} (f : CryptBoolean.BooleanFunction (n + 2))
  (hf : CryptBoolean.IsBent f) (hn : Even n) :
  (∀ (y : FABL.F₂Cube 2),
      CryptBoolean.IsBent (CryptBoolean.firstBlockSlice f y)) ↔
    CryptBoolean.secondBooleanDerivative (CryptBoolean.bentDual f)
        (Fin.append 0 (Pi.single 0 1)) (Fin.append 0 (Pi.single 1 1)) =
      1
    theorem CryptBoolean.isBent_firstBlockSlices_iff_bentDual_secondDerivative_eq_one
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 2))
  (hf : CryptBoolean.IsBent f)
  (hn : Even n) :
  (∀ (y : FABL.F₂Cube 2),
      CryptBoolean.IsBent
        (CryptBoolean.firstBlockSlice f
          y)) ↔
    CryptBoolean.secondBooleanDerivative
        (CryptBoolean.bentDual f)
        (Fin.append 0 (Pi.single 0 1))
        (Fin.append 0 (Pi.single 1 1)) =
      1
    The four codimension-two coordinate restrictions of a bent function are
bent exactly when the dual has constant second derivative one in the two
orthogonal coordinate directions.