Cryptographic Boolean Functions in Lean

5.6. Secondary constructions of bent functions🔗

Theorem5.6.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
Definition 5.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Proposition 5.14.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6direct-sumpages-88-89fidelity-exact

Direct sum (Carlet, pp. 88--89). If f:V_n\to\mathbb F_2 and g:V_m\to\mathbb F_2 are bent, then h(x,y)=f(x)+g(y) is bent on V_{n+m}. Its spectrum and dual factor as W_h(a,b)=W_f(a)W_g(b) and \widetilde h(a,b)=\widetilde f(a)+\widetilde g(b).

Lean code for Theorem5.6.1●5 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/DirectSum.lean
    complete
    def CryptBoolean.IsDecomposable {n m : ℕ}
  (h : CryptBoolean.BooleanFunction (n + m)) : Prop
    def CryptBoolean.IsDecomposable {n m : ℕ}
  (h :
    CryptBoolean.BooleanFunction
      (n + m)) :
  Prop
    A function is decomposable with block sizes `n` and `m` when an affine
change of variables turns it into a sum of functions on the two disjoint
blocks.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DirectSum.lean
    complete
    theorem CryptBoolean.isDecomposable_booleanDirectSum {n m : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.IsDecomposable (CryptBoolean.booleanDirectSum f g)
    theorem CryptBoolean.isDecomposable_booleanDirectSum
  {n m : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.IsDecomposable
    (CryptBoolean.booleanDirectSum f g)
    Every direct sum is decomposable.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DirectSum.lean
    complete
    theorem CryptBoolean.walshTransform_directSum {n m : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (g : CryptBoolean.BooleanFunction m) (a : FABL.F₂Cube n)
  (b : FABL.F₂Cube m) :
  CryptBoolean.walshTransform (CryptBoolean.booleanDirectSum f g)
      (Fin.append a b) =
    CryptBoolean.walshTransform f a * CryptBoolean.walshTransform g b
    theorem CryptBoolean.walshTransform_directSum
  {n m : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (g : CryptBoolean.BooleanFunction m)
  (a : FABL.F₂Cube n)
  (b : FABL.F₂Cube m) :
  CryptBoolean.walshTransform
      (CryptBoolean.booleanDirectSum f g)
      (Fin.append a b) =
    CryptBoolean.walshTransform f a *
      CryptBoolean.walshTransform g b
    Carlet's direct-sum Walsh identity.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DirectSum.lean
    complete
    theorem CryptBoolean.isBent_booleanDirectSum {n m : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {g : CryptBoolean.BooleanFunction m} (hf : CryptBoolean.IsBent f)
  (hg : CryptBoolean.IsBent g) :
  CryptBoolean.IsBent (CryptBoolean.booleanDirectSum f g)
    theorem CryptBoolean.isBent_booleanDirectSum
  {n m : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {g : CryptBoolean.BooleanFunction m}
  (hf : CryptBoolean.IsBent f)
  (hg : CryptBoolean.IsBent g) :
  CryptBoolean.IsBent
    (CryptBoolean.booleanDirectSum f g)
    The Boolean direct sum of two bent functions is bent.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/DirectSum.lean
    complete
    theorem CryptBoolean.bentDual_booleanDirectSum_append {n m : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {g : CryptBoolean.BooleanFunction m} (hf : CryptBoolean.IsBent f)
  (hg : CryptBoolean.IsBent g) (a : FABL.F₂Cube n) (b : FABL.F₂Cube m) :
  CryptBoolean.bentDual (CryptBoolean.booleanDirectSum f g)
      (Fin.append a b) =
    CryptBoolean.bentDual f a + CryptBoolean.bentDual g b
    theorem CryptBoolean.bentDual_booleanDirectSum_append
  {n m : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {g : CryptBoolean.BooleanFunction m}
  (hf : CryptBoolean.IsBent f)
  (hg : CryptBoolean.IsBent g)
  (a : FABL.F₂Cube n)
  (b : FABL.F₂Cube m) :
  CryptBoolean.bentDual
      (CryptBoolean.booleanDirectSum f g)
      (Fin.append a b) =
    CryptBoolean.bentDual f a +
      CryptBoolean.bentDual g b
    The dual of a direct sum is the direct sum of the two duals.
Theorem5.6.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 2
Statement dependency previews
Preview
Theorem 5.6.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6rothauspage-89fidelity-exact

Dillon--Rothaus construction (Carlet, p. 89). Let g,h,k, and g+h+k be bent functions on V_n. Then the function on \mathbb F_2^2\times V_n given by gh+gk+hk+(g+h)x_1+(g+k)x_2+x_1x_2 is bent.

Lean code for Theorem5.6.2●3 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/Rothaus.lean
    complete
    def CryptBoolean.rothausConstruction {n : ℕ}
  (g h k : CryptBoolean.BooleanFunction n) :
  CryptBoolean.BooleanFunction (2 + n)
    def CryptBoolean.rothausConstruction {n : ℕ}
  (g h k :
    CryptBoolean.BooleanFunction n) :
  CryptBoolean.BooleanFunction (2 + n)
    The Dillon--Rothaus function, with the two new coordinates forming the
first block.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Rothaus.lean
    complete
    theorem CryptBoolean.rothausConstruction_append {n : ℕ}
  (g h k : CryptBoolean.BooleanFunction n) (u : FABL.F₂Cube 2)
  (x : FABL.F₂Cube n) :
  CryptBoolean.rothausConstruction g h k (Fin.append u x) =
    g x * h x + g x * k x + h x * k x + (g x + h x) * u 0 +
        (g x + k x) * u 1 +
      u 0 * u 1
    theorem CryptBoolean.rothausConstruction_append
  {n : ℕ}
  (g h k : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube 2)
  (x : FABL.F₂Cube n) :
  CryptBoolean.rothausConstruction g h k
      (Fin.append u x) =
    g x * h x + g x * k x + h x * k x +
          (g x + h x) * u 0 +
        (g x + k x) * u 1 +
      u 0 * u 1
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Rothaus.lean
    complete
    theorem CryptBoolean.isBent_rothausConstruction {n : ℕ}
  (g h k : CryptBoolean.BooleanFunction n) (hnEven : Even n)
  (_hnTwo : 2 ≤ n) (hg : CryptBoolean.IsBent g)
  (hh : CryptBoolean.IsBent h) (hk : CryptBoolean.IsBent k)
  (hsum : CryptBoolean.IsBent (CryptBoolean.threeFunctionSum g h k)) :
  CryptBoolean.IsBent (CryptBoolean.rothausConstruction g h k)
    theorem CryptBoolean.isBent_rothausConstruction
  {n : ℕ}
  (g h k : CryptBoolean.BooleanFunction n)
  (hnEven : Even n) (_hnTwo : 2 ≤ n)
  (hg : CryptBoolean.IsBent g)
  (hh : CryptBoolean.IsBent h)
  (hk : CryptBoolean.IsBent k)
  (hsum :
    CryptBoolean.IsBent
      (CryptBoolean.threeFunctionSum g h
        k)) :
  CryptBoolean.IsBent
    (CryptBoolean.rothausConstruction g h
      k)
    The Dillon--Rothaus secondary construction is bent when `g`, `h`, `k`,
and `g + h + k` are bent.
Theorem5.6.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 4
Statement dependency previews
Preview
Proposition 1.11.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 5.6.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6theorem-9pages-90-91fidelity-exact

Theorem 9 (Carlet, pp. 90--91). Let f be bent on V_n, let b+E be an affine flat, and put f^*=f+\mathbf1_{b+E}. Then f^* is bent if and only if either of the following equivalent conditions holds:

  1. for every a\notin E, the derivative D_af is balanced on b+E;

  2. on every coset of E^\perp, the restriction of \widetilde f(x)+b\mathbin\cdot x is constant or balanced.

If both f and f^* are bent, then \dim E\ge n/2 and the restriction of f to b+E has algebraic degree at most \dim E-n/2+1. Conversely, if \dim E=n/2 and that restriction is affine, then f^* is bent.

Lean code for Theorem5.6.3●18 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    def CryptBoolean.flatSwitch {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (b : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.flatSwitch {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction n
    The Boolean function obtained by complementing `f` on the affine flat
`b + E`.
  • defdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    def CryptBoolean.IsBalancedOnAffineFlat {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (b : FABL.F₂Cube n) : Prop
    def CryptBoolean.IsBalancedOnAffineFlat
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) : Prop
    Balancedness of the restriction of a Boolean function to an affine flat,
expressed without choosing coordinates on its direction subspace.
  • defdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    def CryptBoolean.IsConstantOrBalancedOnAffineFlat {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (b : FABL.F₂Cube n) : Prop
    def CryptBoolean.IsConstantOrBalancedOnAffineFlat
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) : Prop
    A Boolean function is constant or balanced on an affine flat exactly
when its signed restriction sum is extremal or zero.
  • defdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    def CryptBoolean.affineFlatWalshSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (b a : FABL.F₂Cube n) : ℤ
    def CryptBoolean.affineFlatWalshSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b a : FABL.F₂Cube n) : ℤ
    The signed Walsh sum of `f` over the affine flat `b + E`.
  • defdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    def CryptBoolean.affineFlatSubtypeEquiv {n : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (b : FABL.F₂Cube n) :
  ↥E ≃ ↥(FABL.binaryAffineSubspace E b)
    def CryptBoolean.affineFlatSubtypeEquiv
  {n : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) :
  ↥E ≃ ↥(FABL.binaryAffineSubspace E b)
    Translation identifies a subspace with each of its affine cosets.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.walshTransform_sub_flatSwitch {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (b a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f a -
      CryptBoolean.walshTransform (CryptBoolean.flatSwitch f E b) a =
    2 * CryptBoolean.affineFlatWalshSum f E b a
    theorem CryptBoolean.walshTransform_sub_flatSwitch
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f a -
      CryptBoolean.walshTransform
        (CryptBoolean.flatSwitch f E b)
        a =
    2 *
      CryptBoolean.affineFlatWalshSum f E
        b a
    Complementing on an affine flat changes a Walsh coefficient by twice
the signed Walsh sum over that flat.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.affineFlatWalshSum_eq_bitSignInt_mul_walshTransform_restriction
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (b a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) (c : FABL.F₂Cube k)
  (ha :
    ∀ (y : FABL.F₂Cube k),
      FABL.f₂DotProduct a ↑(e y) = FABL.f₂DotProduct c y) :
  CryptBoolean.affineFlatWalshSum f E b a =
    CryptBoolean.bitSignInt (FABL.f₂DotProduct a b) *
      CryptBoolean.walshTransform
        (CryptBoolean.coordinateAffineSubspaceRestriction f E b e) c
    theorem CryptBoolean.affineFlatWalshSum_eq_bitSignInt_mul_walshTransform_restriction
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b a : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (c : FABL.F₂Cube k)
  (ha :
    ∀ (y : FABL.F₂Cube k),
      FABL.f₂DotProduct a ↑(e y) =
        FABL.f₂DotProduct c y) :
  CryptBoolean.affineFlatWalshSum f E b
      a =
    CryptBoolean.bitSignInt
        (FABL.f₂DotProduct a b) *
      CryptBoolean.walshTransform
        (CryptBoolean.coordinateAffineSubspaceRestriction
          f E b e)
        c
    In coordinates on `E`, the signed Walsh sum on `b + E` is the local
Walsh coefficient, up to the sign contributed by the translate.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.affineSubspaceRestrictionImbalance_bentDual_add_linear
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a b : FABL.F₂Cube n) :
  CryptBoolean.affineSubspaceRestrictionImbalance
      (CryptBoolean.bentDual f + FABL.affineFunction 0 b)
      (FABL.perpendicularSubspace E) a =
    (2 ^ (n / 2))⁻¹ * ↑(Nat.card ↥(FABL.perpendicularSubspace E)) *
        (FABL.vectorWalshCharacter b) a *
      ↑(CryptBoolean.affineFlatWalshSum f E b a)
    theorem CryptBoolean.affineSubspaceRestrictionImbalance_bentDual_add_linear
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a b : FABL.F₂Cube n) :
  CryptBoolean.affineSubspaceRestrictionImbalance
      (CryptBoolean.bentDual f +
        FABL.affineFunction 0 b)
      (FABL.perpendicularSubspace E) a =
    (2 ^ (n / 2))⁻¹ *
          ↑(Nat.card
              ↥(FABL.perpendicularSubspace
                  E)) *
        (FABL.vectorWalshCharacter b) a *
      ↑(CryptBoolean.affineFlatWalshSum f
          E b a)
    Poisson summation identifies the imbalance of the dual-plus-linear
restriction on `a + Eᵖ` with the signed Walsh sum of `f` on `b + E`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.abs_affineSubspaceRestrictionImbalance_bentDual_add_linear
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a b : FABL.F₂Cube n) :
  |CryptBoolean.affineSubspaceRestrictionImbalance
        (CryptBoolean.bentDual f + FABL.affineFunction 0 b)
        (FABL.perpendicularSubspace E) a| =
    (2 ^ (n / 2))⁻¹ * ↑(Nat.card ↥(FABL.perpendicularSubspace E)) *
      |↑(CryptBoolean.affineFlatWalshSum f E b a)|
    theorem CryptBoolean.abs_affineSubspaceRestrictionImbalance_bentDual_add_linear
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a b : FABL.F₂Cube n) :
  |CryptBoolean.affineSubspaceRestrictionImbalance
        (CryptBoolean.bentDual f +
          FABL.affineFunction 0 b)
        (FABL.perpendicularSubspace E)
        a| =
    (2 ^ (n / 2))⁻¹ *
        ↑(Nat.card
            ↥(FABL.perpendicularSubspace
                E)) *
      |↑(CryptBoolean.affineFlatWalshSum f
            E b a)|
    Absolute-value form of the dual Poisson identity used in Carlet
Theorem 9, Condition 2.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.autocorrelation_flatSwitch {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (b a : FABL.F₂Cube n) :
  CryptBoolean.autocorrelation (CryptBoolean.flatSwitch f E b) a =
    if a ∈ E then CryptBoolean.autocorrelation f a
    else
      CryptBoolean.autocorrelation f a -
        4 *
          CryptBoolean.affineSubspaceRestrictionImbalance
            (FABL.booleanDerivative f a) E b
    theorem CryptBoolean.autocorrelation_flatSwitch
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b a : FABL.F₂Cube n) :
  CryptBoolean.autocorrelation
      (CryptBoolean.flatSwitch f E b) a =
    if a ∈ E then
      CryptBoolean.autocorrelation f a
    else
      CryptBoolean.autocorrelation f a -
        4 *
          CryptBoolean.affineSubspaceRestrictionImbalance
            (FABL.booleanDerivative f a) E
            b
    The autocorrelation change under affine-flat switching. In directions
outside `E`, the correction is four times the imbalance of the restricted
derivative.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.isBent_flatSwitch_iff_derivative_balanced_on_affineFlat
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) :
  CryptBoolean.IsBent (CryptBoolean.flatSwitch f E b) ↔
    ∀ a ∉ E,
      CryptBoolean.IsBalancedOnAffineFlat (FABL.booleanDerivative f a) E
        b
    theorem CryptBoolean.isBent_flatSwitch_iff_derivative_balanced_on_affineFlat
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) :
  CryptBoolean.IsBent
      (CryptBoolean.flatSwitch f E b) ↔
    ∀ a ∉ E,
      CryptBoolean.IsBalancedOnAffineFlat
        (FABL.booleanDerivative f a) E b
    Carlet Theorem 9, Condition 1: switching a bent function on `b + E`
is bent exactly when every derivative in a direction outside `E` is balanced
on that flat.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.isBent_flatSwitch_iff_bentDual_add_linear_constant_or_balanced
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) :
  CryptBoolean.IsBent (CryptBoolean.flatSwitch f E b) ↔
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.IsConstantOrBalancedOnAffineFlat
        (CryptBoolean.bentDual f + FABL.affineFunction 0 b)
        (FABL.perpendicularSubspace E) a
    theorem CryptBoolean.isBent_flatSwitch_iff_bentDual_add_linear_constant_or_balanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) :
  CryptBoolean.IsBent
      (CryptBoolean.flatSwitch f E b) ↔
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.IsConstantOrBalancedOnAffineFlat
        (CryptBoolean.bentDual f +
          FABL.affineFunction 0 b)
        (FABL.perpendicularSubspace E) a
    Carlet Theorem 9, Condition 2: switching a bent function on `b + E`
is bent exactly when `bentDual f + b · x` is constant or balanced on every
coset of `Eᵖ`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.derivative_balanced_on_affineFlat_iff_bentDual_add_linear_constant_or_balanced
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) :
  (∀ a ∉ E,
      CryptBoolean.IsBalancedOnAffineFlat (FABL.booleanDerivative f a) E
        b) ↔
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.IsConstantOrBalancedOnAffineFlat
        (CryptBoolean.bentDual f + FABL.affineFunction 0 b)
        (FABL.perpendicularSubspace E) a
    theorem CryptBoolean.derivative_balanced_on_affineFlat_iff_bentDual_add_linear_constant_or_balanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) :
  (∀ a ∉ E,
      CryptBoolean.IsBalancedOnAffineFlat
        (FABL.booleanDerivative f a) E
        b) ↔
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.IsConstantOrBalancedOnAffineFlat
        (CryptBoolean.bentDual f +
          FABL.affineFunction 0 b)
        (FABL.perpendicularSubspace E) a
    The two criteria in Carlet Theorem 9 are equivalent.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.bitSignInt_mul_self (b : FABL.𝔽₂) :
  CryptBoolean.bitSignInt b * CryptBoolean.bitSignInt b = 1
    theorem CryptBoolean.bitSignInt_mul_self
  (b : FABL.𝔽₂) :
  CryptBoolean.bitSignInt b *
      CryptBoolean.bitSignInt b =
    1
    A binary sign squares to one.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.two_pow_half_dvd_walshTransform_affineFlatRestriction
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n)
  (hswitch : CryptBoolean.IsBent (CryptBoolean.flatSwitch f E b))
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) (c : FABL.F₂Cube k) :
  2 ^ (n / 2) ∣
    CryptBoolean.walshTransform
      (CryptBoolean.coordinateAffineSubspaceRestriction f E b e) c
    theorem CryptBoolean.two_pow_half_dvd_walshTransform_affineFlatRestriction
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n)
  (hswitch :
    CryptBoolean.IsBent
      (CryptBoolean.flatSwitch f E b))
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (c : FABL.F₂Cube k) :
  2 ^ (n / 2) ∣
    CryptBoolean.walshTransform
      (CryptBoolean.coordinateAffineSubspaceRestriction
        f E b e)
      c
    If both the original function and its affine-flat switch are bent, every
Walsh coefficient of the restriction to the switched flat is divisible by
`2^(n/2)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.half_dimension_le_finrank_of_isBent_flatSwitch {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (b : FABL.F₂Cube n)
  (hswitch : CryptBoolean.IsBent (CryptBoolean.flatSwitch f E b)) :
  n / 2 ≤ Module.finrank FABL.𝔽₂ ↥E
    theorem CryptBoolean.half_dimension_le_finrank_of_isBent_flatSwitch
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n)
  (hswitch :
    CryptBoolean.IsBent
      (CryptBoolean.flatSwitch f E b)) :
  n / 2 ≤ Module.finrank FABL.𝔽₂ ↥E
    Carlet Theorem 9: if a bent function remains bent after switching on
`b + E`, then `E` has dimension at least `n/2`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_affineFlatRestriction_le_of_isBent_flatSwitch
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n)
  (hswitch : CryptBoolean.IsBent (CryptBoolean.flatSwitch f E b))
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.coordinateAffineSubspaceRestriction f E b e) ≤
    k - n / 2 + 1
    theorem CryptBoolean.functionAlgebraicDegree_affineFlatRestriction_le_of_isBent_flatSwitch
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n)
  (hswitch :
    CryptBoolean.IsBent
      (CryptBoolean.flatSwitch f E b))
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.coordinateAffineSubspaceRestriction
        f E b e) ≤
    k - n / 2 + 1
    Carlet Theorem 9: when the switch is bent, the algebraic degree of the
restriction to `b + E` is at most `dim(E) - n/2 + 1`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/FlatSwitching.lean
    complete
    theorem CryptBoolean.isBent_flatSwitch_of_half_dimension_of_restriction_degree_le_one
  {n k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (hk : k = n / 2)
  (hdegree :
    FABL.functionAlgebraicDegree
        (CryptBoolean.coordinateAffineSubspaceRestriction f E b e) ≤
      1) :
  CryptBoolean.IsBent (CryptBoolean.flatSwitch f E b)
    theorem CryptBoolean.isBent_flatSwitch_of_half_dimension_of_restriction_degree_le_one
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (b : FABL.F₂Cube n)
  (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E)
  (hk : k = n / 2)
  (hdegree :
    FABL.functionAlgebraicDegree
        (CryptBoolean.coordinateAffineSubspaceRestriction
          f E b e) ≤
      1) :
  CryptBoolean.IsBent
    (CryptBoolean.flatSwitch f E b)
    Carlet Theorem 9, converse: if `E` has dimension `n/2` and the
restriction of a bent function to `b + E` is affine, switching on that flat
is bent.
Theorem5.6.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 5.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6class-d-zeropages-90-91fidelity-exact

Class D_0 (Carlet, pp. 90--91). Let \pi be a permutation of V_m. The function f(x,y)=x\mathbin\cdot\pi(y)+\delta_0(x) is bent on V_m\times V_m, and its dual is \widetilde f(a,b)=b\mathbin\cdot\pi^{-1}(a)+\delta_0(b).

Lean code for Theorem5.6.4●5 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    def CryptBoolean.classDZero {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m)) :
  CryptBoolean.BooleanFunction (m + m)
    def CryptBoolean.classDZero {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m)) :
  CryptBoolean.BooleanFunction (m + m)
    Carlet's class `D₀`, obtained by switching the zero first-block flat
of the permutation Maiorana--McFarland construction.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    theorem CryptBoolean.classDZero_append {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (x y : FABL.F₂Cube m) :
  CryptBoolean.classDZero π (Fin.append x y) =
    FABL.f₂DotProduct x (π y) + FABL.f₂PointIndicator 0 x
    theorem CryptBoolean.classDZero_append {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (x y : FABL.F₂Cube m) :
  CryptBoolean.classDZero π
      (Fin.append x y) =
    FABL.f₂DotProduct x (π y) +
      FABL.f₂PointIndicator 0 x
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    theorem CryptBoolean.walshTransform_classDZero {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m)) (a b : FABL.F₂Cube m) :
  CryptBoolean.walshTransform (CryptBoolean.classDZero π)
      (Fin.append a b) =
    CryptBoolean.bitSignInt
        (FABL.f₂DotProduct b ((Equiv.symm π) a) +
          FABL.f₂PointIndicator 0 b) *
      2 ^ m
    theorem CryptBoolean.walshTransform_classDZero
  {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (a b : FABL.F₂Cube m) :
  CryptBoolean.walshTransform
      (CryptBoolean.classDZero π)
      (Fin.append a b) =
    CryptBoolean.bitSignInt
        (FABL.f₂DotProduct b
            ((Equiv.symm π) a) +
          FABL.f₂PointIndicator 0 b) *
      2 ^ m
    The exact Walsh spectrum of Carlet's class `D₀`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    theorem CryptBoolean.isBent_classDZero {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m)) :
  CryptBoolean.IsBent (CryptBoolean.classDZero π)
    theorem CryptBoolean.isBent_classDZero {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m)) :
  CryptBoolean.IsBent
    (CryptBoolean.classDZero π)
    Every class-`D₀` function is bent.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    theorem CryptBoolean.bentDual_classDZero_append {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m)) (a b : FABL.F₂Cube m) :
  CryptBoolean.bentDual (CryptBoolean.classDZero π) (Fin.append a b) =
    FABL.f₂DotProduct b ((Equiv.symm π) a) + FABL.f₂PointIndicator 0 b
    theorem CryptBoolean.bentDual_classDZero_append
  {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (a b : FABL.F₂Cube m) :
  CryptBoolean.bentDual
      (CryptBoolean.classDZero π)
      (Fin.append a b) =
    FABL.f₂DotProduct b
        ((Equiv.symm π) a) +
      FABL.f₂PointIndicator 0 b
    The dual of a class-`D₀` function has the inverse-permutation formula
recorded by Carlet.
Theorem5.6.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
Theorem 5.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6class-dpages-90-91fidelity-exact

Class D (Carlet, pp. 90--91). Let E_1,E_2 be subspaces of V_m and let \pi be a permutation such that \pi(E_2)=E_1^\perp. Then f(x,y)=x\mathbin\cdot\pi(y)+\mathbf 1_{E_1}(x)\mathbf 1_{E_2}(y) is bent on V_m\times V_m.

Lean code for Theorem5.6.5●3 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    def CryptBoolean.classD {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) :
  CryptBoolean.BooleanFunction (m + m)
    def CryptBoolean.classD {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (E₁ E₂ :
    Submodule FABL.𝔽₂ (FABL.F₂Cube m)) :
  CryptBoolean.BooleanFunction (m + m)
    Carlet's class `D`, obtained by switching a permutation
Maiorana--McFarland function on a product of subspaces.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    theorem CryptBoolean.classD_append {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) (x y : FABL.F₂Cube m) :
  CryptBoolean.classD π E₁ E₂ (Fin.append x y) =
    FABL.f₂DotProduct x (π y) +
      CryptBoolean.affineFlatIndicator E₁ 0 x *
        CryptBoolean.affineFlatIndicator E₂ 0 y
    theorem CryptBoolean.classD_append {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (E₁ E₂ :
    Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (x y : FABL.F₂Cube m) :
  CryptBoolean.classD π E₁ E₂
      (Fin.append x y) =
    FABL.f₂DotProduct x (π y) +
      CryptBoolean.affineFlatIndicator E₁
          0 x *
        CryptBoolean.affineFlatIndicator
          E₂ 0 y
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    theorem CryptBoolean.isBent_classD {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (hπ :
    ∀ (y : FABL.F₂Cube m),
      y ∈ E₂ ↔ π y ∈ FABL.perpendicularSubspace E₁) :
  CryptBoolean.IsBent (CryptBoolean.classD π E₁ E₂)
    theorem CryptBoolean.isBent_classD {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (E₁ E₂ :
    Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (hπ :
    ∀ (y : FABL.F₂Cube m),
      y ∈ E₂ ↔
        π y ∈
          FABL.perpendicularSubspace E₁) :
  CryptBoolean.IsBent
    (CryptBoolean.classD π E₁ E₂)
    Carlet's class `D` is bent when the permutation sends the second
switching subspace onto the perpendicular of the first.
Theorem5.6.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 5.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6class-cpages-90-91fidelity-exact

Class C (Carlet, pp. 90--91). Let L be a subspace of V_m and let \pi be a permutation such that every set \pi^{-1}(a+L^\perp) is an affine flat. Then f(x,y)=x\mathbin\cdot\pi(y)+\mathbf 1_L(x) is bent. More generally, f_g(x,y)=x\mathbin\cdot\pi(y)+\mathbf 1_L(x)+g(y) is bent whenever the restriction of g to every \pi^{-1}(a+L^\perp) is affine.

Lean code for Theorem5.6.6●7 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    def CryptBoolean.HasAffinePerpendicularCosetPreimages {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : Prop
    def CryptBoolean.HasAffinePerpendicularCosetPreimages
  {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (L :
    Submodule FABL.𝔽₂ (FABL.F₂Cube m)) :
  Prop
    Every inverse image under `π` of a coset of `Lᵖ` is an affine flat.
  • defdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    def CryptBoolean.IsAffineOnPerpendicularCosetPreimages {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m) : Prop
    def CryptBoolean.IsAffineOnPerpendicularCosetPreimages
  {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m) :
  Prop
    The offset function restricts affinely to every inverse image under
`π` of a coset of `Lᵖ`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    theorem CryptBoolean.isAffineOnPerpendicularCosetPreimages_zero {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) :
  CryptBoolean.IsAffineOnPerpendicularCosetPreimages π L 0
    theorem CryptBoolean.isAffineOnPerpendicularCosetPreimages_zero
  {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (L :
    Submodule FABL.𝔽₂ (FABL.F₂Cube m)) :
  CryptBoolean.IsAffineOnPerpendicularCosetPreimages
    π L 0
    The zero offset is affine on every perpendicular-coset preimage.
  • defdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    def CryptBoolean.classC {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + m)
    def CryptBoolean.classC {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (m + m)
    Carlet's class `C`, obtained by switching a permutation
Maiorana--McFarland function on `L × V_m`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    theorem CryptBoolean.classC_append {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m) (x y : FABL.F₂Cube m) :
  CryptBoolean.classC π L g (Fin.append x y) =
    FABL.f₂DotProduct x (π y) + g y +
      CryptBoolean.affineFlatIndicator L 0 x
    theorem CryptBoolean.classC_append {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m)
  (x y : FABL.F₂Cube m) :
  CryptBoolean.classC π L g
      (Fin.append x y) =
    FABL.f₂DotProduct x (π y) + g y +
      CryptBoolean.affineFlatIndicator L 0
        x
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    theorem CryptBoolean.isBent_classC {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m)
  (hpreimages : CryptBoolean.HasAffinePerpendicularCosetPreimages π L)
  (hoffset : CryptBoolean.IsAffineOnPerpendicularCosetPreimages π L g) :
  CryptBoolean.IsBent (CryptBoolean.classC π L g)
    theorem CryptBoolean.isBent_classC {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m)
  (hpreimages :
    CryptBoolean.HasAffinePerpendicularCosetPreimages
      π L)
  (hoffset :
    CryptBoolean.IsAffineOnPerpendicularCosetPreimages
      π L g) :
  CryptBoolean.IsBent
    (CryptBoolean.classC π L g)
    Carlet's class `C` is bent when perpendicular-coset preimages are
affine flats and the offset restricts affinely to each of them.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean
    complete
    theorem CryptBoolean.isBent_classC_zero {m : ℕ} (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (hpreimages : CryptBoolean.HasAffinePerpendicularCosetPreimages π L) :
  CryptBoolean.IsBent (CryptBoolean.classC π L 0)
    theorem CryptBoolean.isBent_classC_zero {m : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m))
  (hpreimages :
    CryptBoolean.HasAffinePerpendicularCosetPreimages
      π L) :
  CryptBoolean.IsBent
    (CryptBoolean.classC π L 0)
    The basic class-`C` construction with zero offset.
Theorem5.6.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 2
Statement dependency previews
Preview
Definition 5.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 5
Reverse dependency previews
Preview
Theorem 5.6.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6theorem-10pages-91-92fidelity-exact

Theorem 10 (Carlet, pp. 91--92). Let n,m be even and let f:V_n\times V_m\to\mathbb F_2. Suppose every slice f_y(x)=f(x,y) is bent, and define \varphi_s(y)=\widetilde{f_y}(s). Then f is bent if and only if every \varphi_s is bent. In that case \widetilde f(s,t)=\widetilde{\varphi_s}(t).

Lean code for Theorem5.6.7●8 declarations
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NestedBent.lean
    complete
    theorem CryptBoolean.finAppend_add {n m : ℕ} (u₁ u₂ : FABL.F₂Cube n)
  (v₁ v₂ : FABL.F₂Cube m) :
  Fin.append (u₁ + u₂) (v₁ + v₂) = Fin.append u₁ v₁ + Fin.append u₂ v₂
    theorem CryptBoolean.finAppend_add {n m : ℕ}
  (u₁ u₂ : FABL.F₂Cube n)
  (v₁ v₂ : FABL.F₂Cube m) :
  Fin.append (u₁ + u₂) (v₁ + v₂) =
    Fin.append u₁ v₁ + Fin.append u₂ v₂
    Appending binary-cube blocks commutes with addition.
  • defdefined in CryptBoolean/Carlet/Chapter06/NestedBent.lean
    complete
    def CryptBoolean.firstBlockSlice {n m : ℕ}
  (f : CryptBoolean.BooleanFunction (n + m)) (y : FABL.F₂Cube m) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.firstBlockSlice {n m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + m))
  (y : FABL.F₂Cube m) :
  CryptBoolean.BooleanFunction n
    The restriction of a block Boolean function at a fixed second-block input.
  • defdefined in CryptBoolean/Carlet/Chapter06/NestedBent.lean
    complete
    def CryptBoolean.secondBlockSlice {n m : ℕ}
  (f : CryptBoolean.BooleanFunction (n + m)) (x : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction m
    def CryptBoolean.secondBlockSlice {n m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + m))
  (x : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction m
    The restriction of a block Boolean function at a fixed first-block input.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NestedBent.lean
    complete
    theorem CryptBoolean.walshTransform_append_cast_eq_rawFourierTransform_sliceWalsh
  {n m : ℕ} (f : CryptBoolean.BooleanFunction (n + m))
  (s : FABL.F₂Cube n) (t : FABL.F₂Cube m) :
  ↑(CryptBoolean.walshTransform f (Fin.append s t)) =
    CryptBoolean.rawFourierTransform
      (fun y =>
        ↑(CryptBoolean.walshTransform (CryptBoolean.firstBlockSlice f y)
            s))
      t
    theorem CryptBoolean.walshTransform_append_cast_eq_rawFourierTransform_sliceWalsh
  {n m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + m))
  (s : FABL.F₂Cube n)
  (t : FABL.F₂Cube m) :
  ↑(CryptBoolean.walshTransform f
        (Fin.append s t)) =
    CryptBoolean.rawFourierTransform
      (fun y =>
        ↑(CryptBoolean.walshTransform
            (CryptBoolean.firstBlockSlice
              f y)
            s))
      t
    At fixed first-block frequency, the ambient Walsh transform is the raw
Fourier transform of the Walsh coefficients of the first-block slices.
  • defdefined in CryptBoolean/Carlet/Chapter06/NestedBent.lean
    complete
    def CryptBoolean.dualSliceFunction {n m : ℕ}
  (f : CryptBoolean.BooleanFunction (n + m)) (s : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction m
    def CryptBoolean.dualSliceFunction {n m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + m))
  (s : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction m
    At a first-block frequency, collect the dual values of all bent first-block slices.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NestedBent.lean
    complete
    theorem CryptBoolean.walshTransform_eq_two_pow_half_mul_walshTransform_dualSliceFunction
  {n m : ℕ} (f : CryptBoolean.BooleanFunction (n + m))
  (hslices :
    ∀ (y : FABL.F₂Cube m),
      CryptBoolean.IsBent (CryptBoolean.firstBlockSlice f y))
  (s : FABL.F₂Cube n) (t : FABL.F₂Cube m) :
  CryptBoolean.walshTransform f (Fin.append s t) =
    2 ^ (n / 2) *
      CryptBoolean.walshTransform (CryptBoolean.dualSliceFunction f s) t
    theorem CryptBoolean.walshTransform_eq_two_pow_half_mul_walshTransform_dualSliceFunction
  {n m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + m))
  (hslices :
    ∀ (y : FABL.F₂Cube m),
      CryptBoolean.IsBent
        (CryptBoolean.firstBlockSlice f
          y))
  (s : FABL.F₂Cube n)
  (t : FABL.F₂Cube m) :
  CryptBoolean.walshTransform f
      (Fin.append s t) =
    2 ^ (n / 2) *
      CryptBoolean.walshTransform
        (CryptBoolean.dualSliceFunction f
          s)
        t
    The raw Walsh transform of nested bent slices factors through their dual slice.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NestedBent.lean
    complete
    theorem CryptBoolean.isBent_iff_forall_isBent_dualSliceFunction {n m : ℕ}
  (f : CryptBoolean.BooleanFunction (n + m)) (hn : Even n) (hm : Even m)
  (hslices :
    ∀ (y : FABL.F₂Cube m),
      CryptBoolean.IsBent (CryptBoolean.firstBlockSlice f y)) :
  CryptBoolean.IsBent f ↔
    ∀ (s : FABL.F₂Cube n),
      CryptBoolean.IsBent (CryptBoolean.dualSliceFunction f s)
    theorem CryptBoolean.isBent_iff_forall_isBent_dualSliceFunction
  {n m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + m))
  (hn : Even n) (hm : Even m)
  (hslices :
    ∀ (y : FABL.F₂Cube m),
      CryptBoolean.IsBent
        (CryptBoolean.firstBlockSlice f
          y)) :
  CryptBoolean.IsBent f ↔
    ∀ (s : FABL.F₂Cube n),
      CryptBoolean.IsBent
        (CryptBoolean.dualSliceFunction f
          s)
    Carlet Theorem 10: with bent first-block slices, the whole function is
bent exactly when every function of their dual values is bent.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NestedBent.lean
    complete
    theorem CryptBoolean.bentDual_append_eq_bentDual_dualSliceFunction {n m : ℕ}
  (f : CryptBoolean.BooleanFunction (n + m)) (hn : Even n) (hm : Even m)
  (hslices :
    ∀ (y : FABL.F₂Cube m),
      CryptBoolean.IsBent (CryptBoolean.firstBlockSlice f y))
  (hdualSlices :
    ∀ (s : FABL.F₂Cube n),
      CryptBoolean.IsBent (CryptBoolean.dualSliceFunction f s))
  (s : FABL.F₂Cube n) (t : FABL.F₂Cube m) :
  CryptBoolean.bentDual f (Fin.append s t) =
    CryptBoolean.bentDual (CryptBoolean.dualSliceFunction f s) t
    theorem CryptBoolean.bentDual_append_eq_bentDual_dualSliceFunction
  {n m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + m))
  (hn : Even n) (hm : Even m)
  (hslices :
    ∀ (y : FABL.F₂Cube m),
      CryptBoolean.IsBent
        (CryptBoolean.firstBlockSlice f
          y))
  (hdualSlices :
    ∀ (s : FABL.F₂Cube n),
      CryptBoolean.IsBent
        (CryptBoolean.dualSliceFunction f
          s))
  (s : FABL.F₂Cube n)
  (t : FABL.F₂Cube m) :
  CryptBoolean.bentDual f
      (Fin.append s t) =
    CryptBoolean.bentDual
      (CryptBoolean.dualSliceFunction f s)
      t
    Under Theorem 10's hypotheses, the dual is obtained by dualizing the
second-block function of first-slice dual values.
Theorem5.6.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.
uses 1used by 1✓L∃∀N
Tagscarletchapter-6indirect-sumpage-92fidelity-exact

Indirect sum (Carlet, p. 92). If f_1,f_2 are bent on V_n and g_1,g_2 are bent on V_m, then h(x,y)=f_1(x)+g_1(y)+(f_1+f_2)(x)(g_1+g_2)(y) is bent. Its dual is obtained by applying the same formula to the four duals.

Lean code for Theorem5.6.8●4 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/IndirectSum.lean
    complete
    def CryptBoolean.indirectSum {n m : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction n)
  (g₁ g₂ : CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (n + m)
    def CryptBoolean.indirectSum {n m : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction n)
  (g₁ g₂ :
    CryptBoolean.BooleanFunction m) :
  CryptBoolean.BooleanFunction (n + m)
    The indirect sum of two pairs of Boolean functions on disjoint blocks.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/IndirectSum.lean
    complete
    theorem CryptBoolean.indirectSum_append {n m : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction n)
  (g₁ g₂ : CryptBoolean.BooleanFunction m) (x : FABL.F₂Cube n)
  (y : FABL.F₂Cube m) :
  CryptBoolean.indirectSum f₁ f₂ g₁ g₂ (Fin.append x y) =
    f₁ x + g₁ y + (f₁ x + f₂ x) * (g₁ y + g₂ y)
    theorem CryptBoolean.indirectSum_append {n m : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction n)
  (g₁ g₂ : CryptBoolean.BooleanFunction m)
  (x : FABL.F₂Cube n)
  (y : FABL.F₂Cube m) :
  CryptBoolean.indirectSum f₁ f₂ g₁ g₂
      (Fin.append x y) =
    f₁ x + g₁ y +
      (f₁ x + f₂ x) * (g₁ y + g₂ y)
  • theoremdefined in CryptBoolean/Carlet/Chapter06/IndirectSum.lean
    complete
    theorem CryptBoolean.isBent_indirectSum {n m : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction n)
  (g₁ g₂ : CryptBoolean.BooleanFunction m) (hn : Even n) (hm : Even m)
  (_hnPositive : 0 < n) (_hmPositive : 0 < m)
  (hf₁ : CryptBoolean.IsBent f₁) (hf₂ : CryptBoolean.IsBent f₂)
  (hg₁ : CryptBoolean.IsBent g₁) (hg₂ : CryptBoolean.IsBent g₂) :
  CryptBoolean.IsBent (CryptBoolean.indirectSum f₁ f₂ g₁ g₂)
    theorem CryptBoolean.isBent_indirectSum {n m : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction n)
  (g₁ g₂ : CryptBoolean.BooleanFunction m)
  (hn : Even n) (hm : Even m)
  (_hnPositive : 0 < n)
  (_hmPositive : 0 < m)
  (hf₁ : CryptBoolean.IsBent f₁)
  (hf₂ : CryptBoolean.IsBent f₂)
  (hg₁ : CryptBoolean.IsBent g₁)
  (hg₂ : CryptBoolean.IsBent g₂) :
  CryptBoolean.IsBent
    (CryptBoolean.indirectSum f₁ f₂ g₁ g₂)
    The indirect sum of four bent functions is bent.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/IndirectSum.lean
    complete
    theorem CryptBoolean.bentDual_indirectSum_append {n m : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction n)
  (g₁ g₂ : CryptBoolean.BooleanFunction m) (hn : Even n) (hm : Even m)
  (_hnPositive : 0 < n) (_hmPositive : 0 < m)
  (hf₁ : CryptBoolean.IsBent f₁) (hf₂ : CryptBoolean.IsBent f₂)
  (hg₁ : CryptBoolean.IsBent g₁) (hg₂ : CryptBoolean.IsBent g₂)
  (s : FABL.F₂Cube n) (t : FABL.F₂Cube m) :
  CryptBoolean.bentDual (CryptBoolean.indirectSum f₁ f₂ g₁ g₂)
      (Fin.append s t) =
    CryptBoolean.indirectSum (CryptBoolean.bentDual f₁)
      (CryptBoolean.bentDual f₂) (CryptBoolean.bentDual g₁)
      (CryptBoolean.bentDual g₂) (Fin.append s t)
    theorem CryptBoolean.bentDual_indirectSum_append
  {n m : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction n)
  (g₁ g₂ : CryptBoolean.BooleanFunction m)
  (hn : Even n) (hm : Even m)
  (_hnPositive : 0 < n)
  (_hmPositive : 0 < m)
  (hf₁ : CryptBoolean.IsBent f₁)
  (hf₂ : CryptBoolean.IsBent f₂)
  (hg₁ : CryptBoolean.IsBent g₁)
  (hg₂ : CryptBoolean.IsBent g₂)
  (s : FABL.F₂Cube n)
  (t : FABL.F₂Cube m) :
  CryptBoolean.bentDual
      (CryptBoolean.indirectSum f₁ f₂ g₁
        g₂)
      (Fin.append s t) =
    CryptBoolean.indirectSum
      (CryptBoolean.bentDual f₁)
      (CryptBoolean.bentDual f₂)
      (CryptBoolean.bentDual g₁)
      (CryptBoolean.bentDual g₂)
      (Fin.append s t)
    The dual of an indirect sum is the indirect sum of the four duals.
Theorem5.6.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 2
Statement dependency previews
Preview
Theorem 5.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6secondary-constructionpage-93fidelity-exact

Maiorana--McFarland bent-family extension (Carlet, p. 93). Let \pi be a permutation of V_r, let g:V_r\to\mathbb F_2, and let (h_y)_{y\in V_r} be a family of bent functions on V_m, where m is even. Then F(x,y,z)=h_y(z)+x\mathbin\cdot\pi(y)+g(y) is bent on V_r\times V_r\times V_m.

Lean code for Theorem5.6.9●3 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/SecondarySpecializations.lean
    complete
    def CryptBoolean.maioranaMcFarlandBentFamilyExtension {m k : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m)) (g : CryptBoolean.BooleanFunction m)
  (h : FABL.F₂Cube m → CryptBoolean.BooleanFunction k) :
  CryptBoolean.BooleanFunction (m + m + k)
    def CryptBoolean.maioranaMcFarlandBentFamilyExtension
  {m k : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m)
  (h :
    FABL.F₂Cube m →
      CryptBoolean.BooleanFunction k) :
  CryptBoolean.BooleanFunction (m + m + k)
    The extension of Maiorana--McFarland type indexed by a family of Boolean
functions on an additional coordinate block.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondarySpecializations.lean
    complete
    theorem CryptBoolean.maioranaMcFarlandBentFamilyExtension_append {m k : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m)) (g : CryptBoolean.BooleanFunction m)
  (h : FABL.F₂Cube m → CryptBoolean.BooleanFunction k)
  (x y : FABL.F₂Cube m) (z : FABL.F₂Cube k) :
  CryptBoolean.maioranaMcFarlandBentFamilyExtension π g h
      (Fin.append (FABL.joinF₂CubeBlocks x y) z) =
    h y z + FABL.f₂DotProduct x (π y) + g y
    theorem CryptBoolean.maioranaMcFarlandBentFamilyExtension_append
  {m k : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m)
  (h :
    FABL.F₂Cube m →
      CryptBoolean.BooleanFunction k)
  (x y : FABL.F₂Cube m)
  (z : FABL.F₂Cube k) :
  CryptBoolean.maioranaMcFarlandBentFamilyExtension
      π g h
      (Fin.append
        (FABL.joinF₂CubeBlocks x y) z) =
    h y z + FABL.f₂DotProduct x (π y) +
      g y
    Evaluation of the Maiorana--McFarland bent-family extension on its three
coordinate blocks.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondarySpecializations.lean
    complete
    theorem CryptBoolean.isBent_maioranaMcFarlandBentFamilyExtension {m k : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m)) (g : CryptBoolean.BooleanFunction m)
  (h : FABL.F₂Cube m → CryptBoolean.BooleanFunction k) (hk : Even k)
  (hh : ∀ (y : FABL.F₂Cube m), CryptBoolean.IsBent (h y)) :
  CryptBoolean.IsBent
    (CryptBoolean.maioranaMcFarlandBentFamilyExtension π g h)
    theorem CryptBoolean.isBent_maioranaMcFarlandBentFamilyExtension
  {m k : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube m))
  (g : CryptBoolean.BooleanFunction m)
  (h :
    FABL.F₂Cube m →
      CryptBoolean.BooleanFunction k)
  (hk : Even k)
  (hh :
    ∀ (y : FABL.F₂Cube m),
      CryptBoolean.IsBent (h y)) :
  CryptBoolean.IsBent
    (CryptBoolean.maioranaMcFarlandBentFamilyExtension
      π g h)
    If every member of the indexed family is bent, the corresponding
Maiorana--McFarland extension is bent.
Theorem5.6.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 3
Statement dependency previews
Preview
Theorem 5.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6secondary-constructionpage-93fidelity-strengthened-zero-dimensional

Four-block class-D_0 construction (Carlet, p. 93). Let r,s be positive, let \pi and \pi' be permutations of V_r and V_s, respectively, and let h:V_s\to\mathbb F_2 be arbitrary. Then F(x,y,z,t)=x\mathbin\cdot\pi(y)+z\mathbin\cdot\pi'(t)+\delta_0(x)h(t) is bent on V_r\times V_r\times V_s\times V_s.

Lean code for Theorem5.6.10●3 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/SecondarySpecializations.lean
    complete
    def CryptBoolean.classDZeroFourBlock {p q : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube p)) (ρ : Equiv.Perm (FABL.F₂Cube q))
  (h : CryptBoolean.BooleanFunction q) :
  CryptBoolean.BooleanFunction (p + p + (q + q))
    def CryptBoolean.classDZeroFourBlock {p q : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube p))
  (ρ : Equiv.Perm (FABL.F₂Cube q))
  (h : CryptBoolean.BooleanFunction q) :
  CryptBoolean.BooleanFunction
    (p + p + (q + q))
    The four-block construction combining two permutation
Maiorana--McFarland terms with a class-`D₀` switch.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondarySpecializations.lean
    complete
    theorem CryptBoolean.classDZeroFourBlock_append {p q : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube p)) (ρ : Equiv.Perm (FABL.F₂Cube q))
  (h : CryptBoolean.BooleanFunction q) (x y : FABL.F₂Cube p)
  (z t : FABL.F₂Cube q) :
  CryptBoolean.classDZeroFourBlock π ρ h
      (Fin.append (FABL.joinF₂CubeBlocks x y)
        (FABL.joinF₂CubeBlocks z t)) =
    FABL.f₂DotProduct x (π y) + FABL.f₂DotProduct z (ρ t) +
      FABL.f₂PointIndicator 0 x * h t
    theorem CryptBoolean.classDZeroFourBlock_append
  {p q : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube p))
  (ρ : Equiv.Perm (FABL.F₂Cube q))
  (h : CryptBoolean.BooleanFunction q)
  (x y : FABL.F₂Cube p)
  (z t : FABL.F₂Cube q) :
  CryptBoolean.classDZeroFourBlock π ρ h
      (Fin.append
        (FABL.joinF₂CubeBlocks x y)
        (FABL.joinF₂CubeBlocks z t)) =
    FABL.f₂DotProduct x (π y) +
        FABL.f₂DotProduct z (ρ t) +
      FABL.f₂PointIndicator 0 x * h t
    Evaluation of the four-block class-`D₀` construction.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/SecondarySpecializations.lean
    complete
    theorem CryptBoolean.isBent_classDZeroFourBlock {p q : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube p)) (ρ : Equiv.Perm (FABL.F₂Cube q))
  (h : CryptBoolean.BooleanFunction q) :
  CryptBoolean.IsBent (CryptBoolean.classDZeroFourBlock π ρ h)
    theorem CryptBoolean.isBent_classDZeroFourBlock
  {p q : ℕ}
  (π : Equiv.Perm (FABL.F₂Cube p))
  (ρ : Equiv.Perm (FABL.F₂Cube q))
  (h : CryptBoolean.BooleanFunction q) :
  CryptBoolean.IsBent
    (CryptBoolean.classDZeroFourBlock π ρ
      h)
    Carlet's four-block construction is bent for arbitrary Boolean `h` and
arbitrary permutations on the two coordinate pairs.
Proposition5.6.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 2
Statement dependency previews
Preview
Definition 1.4.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6proposition-21pages-93-94fidelity-exact

Proposition 21 (Carlet, pp. 93--94). Let \sigma be a permutation of V_n, with coordinate functions \sigma_1,\ldots,\sigma_n. If d_H\!\left(f,\sum_{i=1}^n a_i\sigma_i\right) =2^{n-1}\pm2^{n/2-1} \qquad(a\in V_n), then f\circ\sigma^{-1} is bent.

Lean code for Proposition5.6.11●4 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter06/PermutationReindex.lean
    complete
    theorem CryptBoolean.hammingDistance_comp_perm {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (σ : Equiv.Perm (FABL.F₂Cube n)) :
  CryptBoolean.hammingDistance (f ∘ ⇑σ) (g ∘ ⇑σ) =
    CryptBoolean.hammingDistance f g
    theorem CryptBoolean.hammingDistance_comp_perm
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (σ : Equiv.Perm (FABL.F₂Cube n)) :
  CryptBoolean.hammingDistance (f ∘ ⇑σ)
      (g ∘ ⇑σ) =
    CryptBoolean.hammingDistance f g
    Simultaneous precomposition by a permutation preserves Hamming distance.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/PermutationReindex.lean
    complete
    theorem CryptBoolean.hammingDistance_comp_perm_symm_linearFunction {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (σ : Equiv.Perm (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  CryptBoolean.hammingDistance (f ∘ ⇑(Equiv.symm σ))
      (FABL.affineFunction 0 a) =
    CryptBoolean.hammingDistance f fun x => FABL.f₂DotProduct a (σ x)
    theorem CryptBoolean.hammingDistance_comp_perm_symm_linearFunction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (σ : Equiv.Perm (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  CryptBoolean.hammingDistance
      (f ∘ ⇑(Equiv.symm σ))
      (FABL.affineFunction 0 a) =
    CryptBoolean.hammingDistance f
      fun x => FABL.f₂DotProduct a (σ x)
    Reindexing by `σ⁻¹` converts distance from a linear function into
distance from its pullback along the arbitrary permutation `σ`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/PermutationReindex.lean
    complete
    theorem CryptBoolean.walshTransform_comp_perm_symm_eq_two_pow_sub_two_hammingDistance
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (σ : Equiv.Perm (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform (f ∘ ⇑(Equiv.symm σ)) a =
    2 ^ n -
      2 *
        ↑(CryptBoolean.hammingDistance f fun x =>
            FABL.f₂DotProduct a (σ x))
    theorem CryptBoolean.walshTransform_comp_perm_symm_eq_two_pow_sub_two_hammingDistance
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (σ : Equiv.Perm (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform
      (f ∘ ⇑(Equiv.symm σ)) a =
    2 ^ n -
      2 *
        ↑(CryptBoolean.hammingDistance f
            fun x =>
            FABL.f₂DotProduct a (σ x))
    The Walsh coefficient after an arbitrary permutation is the signed
distance from the corresponding pulled-back linear function.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/PermutationReindex.lean
    complete
    theorem CryptBoolean.isBent_comp_perm_symm_of_hammingDistance {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (σ : Equiv.Perm (FABL.F₂Cube n))
  (hnEven : Even n) (hnTwo : 2 ≤ n)
  (hdistance :
    ∀ (a : FABL.F₂Cube n),
      |↑(CryptBoolean.hammingDistance f fun x =>
                FABL.f₂DotProduct a (σ x)) -
            2 ^ (n - 1)| =
        2 ^ (n / 2 - 1)) :
  CryptBoolean.IsBent (f ∘ ⇑(Equiv.symm σ))
    theorem CryptBoolean.isBent_comp_perm_symm_of_hammingDistance
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (σ : Equiv.Perm (FABL.F₂Cube n))
  (hnEven : Even n) (hnTwo : 2 ≤ n)
  (hdistance :
    ∀ (a : FABL.F₂Cube n),
      |↑(CryptBoolean.hammingDistance f
                fun x =>
                FABL.f₂DotProduct a
                  (σ x)) -
            2 ^ (n - 1)| =
        2 ^ (n / 2 - 1)) :
  CryptBoolean.IsBent
    (f ∘ ⇑(Equiv.symm σ))
    Carlet Proposition 21, first assertion: if the distance from `f` to every
permutation-pulled-back linear function differs from `2^(n-1)` by exactly
`2^(n/2-1)`, then reindexing `f` by the inverse permutation is bent.
Proposition5.6.12
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
Definition 1.7.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Corollary 5.6.13
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6proposition-22relation-50pages-94-95fidelity-exact

Proposition 22 (Carlet, Relation (50), pp. 94--95). For Boolean functions f_1,f_2,f_3, put s_1=f_1+f_2+f_3, \qquad s_2=f_1f_2+f_1f_3+f_2f_3. As integer-valued functions, f_1+f_2+f_3=s_1+2s_2; consequently W_{f_1}+W_{f_2}+W_{f_3}=W_{s_1}+2W_{s_2}.

Lean code for Proposition5.6.12●6 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/ThreeFunctionIdentity.lean
    complete
    def CryptBoolean.threeFunctionSum {n : ℕ}
  (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.threeFunctionSum {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n) :
  CryptBoolean.BooleanFunction n
    The first elementary symmetric function of three Boolean functions.
  • defdefined in CryptBoolean/Carlet/Chapter06/ThreeFunctionIdentity.lean
    complete
    def CryptBoolean.threeFunctionPairwiseProductSum {n : ℕ}
  (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.threeFunctionPairwiseProductSum
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n) :
  CryptBoolean.BooleanFunction n
    The second elementary symmetric function of three Boolean functions.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/ThreeFunctionIdentity.lean
    complete
    theorem CryptBoolean.bitValueInt_threeFunctionIdentity {n : ℕ}
  (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) :
  (fun x =>
      CryptBoolean.bitValueInt (f₁ x) +
          CryptBoolean.bitValueInt (f₂ x) +
        CryptBoolean.bitValueInt (f₃ x)) =
    fun x =>
    CryptBoolean.bitValueInt
        (CryptBoolean.threeFunctionSum f₁ f₂ f₃ x) +
      2 *
        CryptBoolean.bitValueInt
          (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃ x)
    theorem CryptBoolean.bitValueInt_threeFunctionIdentity
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n) :
  (fun x =>
      CryptBoolean.bitValueInt (f₁ x) +
          CryptBoolean.bitValueInt
            (f₂ x) +
        CryptBoolean.bitValueInt (f₃ x)) =
    fun x =>
    CryptBoolean.bitValueInt
        (CryptBoolean.threeFunctionSum f₁
          f₂ f₃ x) +
      2 *
        CryptBoolean.bitValueInt
          (CryptBoolean.threeFunctionPairwiseProductSum
            f₁ f₂ f₃ x)
    Carlet Proposition 22: the ordinary integer sum of three bits is their
first elementary symmetric function plus twice their second.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/ThreeFunctionIdentity.lean
    complete
    theorem CryptBoolean.rawFourierTransform_threeFunctionIdentity {n : ℕ}
  (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform (FABL.booleanRealEmbedding f₁) a +
        CryptBoolean.rawFourierTransform (FABL.booleanRealEmbedding f₂)
          a +
      CryptBoolean.rawFourierTransform (FABL.booleanRealEmbedding f₃)
        a =
    CryptBoolean.rawFourierTransform
        (FABL.booleanRealEmbedding
          (CryptBoolean.threeFunctionSum f₁ f₂ f₃))
        a +
      2 *
        CryptBoolean.rawFourierTransform
          (FABL.booleanRealEmbedding
            (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃))
          a
    theorem CryptBoolean.rawFourierTransform_threeFunctionIdentity
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
          (FABL.booleanRealEmbedding f₁)
          a +
        CryptBoolean.rawFourierTransform
          (FABL.booleanRealEmbedding f₂)
          a +
      CryptBoolean.rawFourierTransform
        (FABL.booleanRealEmbedding f₃) a =
    CryptBoolean.rawFourierTransform
        (FABL.booleanRealEmbedding
          (CryptBoolean.threeFunctionSum
            f₁ f₂ f₃))
        a +
      2 *
        CryptBoolean.rawFourierTransform
          (FABL.booleanRealEmbedding
            (CryptBoolean.threeFunctionPairwiseProductSum
              f₁ f₂ f₃))
          a
    Applying the raw pseudo-Boolean Fourier transform to Proposition 22
preserves the three-function identity.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/ThreeFunctionIdentity.lean
    complete
    theorem CryptBoolean.walshTransform_cast_eq_rawFourierTransform_sub_two_mul
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f a) =
    CryptBoolean.rawFourierTransform (fun x => 1) a -
      2 *
        CryptBoolean.rawFourierTransform (FABL.booleanRealEmbedding f) a
    theorem CryptBoolean.walshTransform_cast_eq_rawFourierTransform_sub_two_mul
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform f a) =
    CryptBoolean.rawFourierTransform
        (fun x => 1) a -
      2 *
        CryptBoolean.rawFourierTransform
          (FABL.booleanRealEmbedding f) a
  • theoremdefined in CryptBoolean/Carlet/Chapter06/ThreeFunctionIdentity.lean
    complete
    theorem CryptBoolean.walshTransform_threeFunctionIdentity {n : ℕ}
  (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f₁ a + CryptBoolean.walshTransform f₂ a +
      CryptBoolean.walshTransform f₃ a =
    CryptBoolean.walshTransform (CryptBoolean.threeFunctionSum f₁ f₂ f₃)
        a +
      2 *
        CryptBoolean.walshTransform
          (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃) a
    theorem CryptBoolean.walshTransform_threeFunctionIdentity
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f₁ a +
        CryptBoolean.walshTransform f₂ a +
      CryptBoolean.walshTransform f₃ a =
    CryptBoolean.walshTransform
        (CryptBoolean.threeFunctionSum f₁
          f₂ f₃)
        a +
      2 *
        CryptBoolean.walshTransform
          (CryptBoolean.threeFunctionPairwiseProductSum
            f₁ f₂ f₃)
          a
    Carlet relation (50): the raw Walsh transforms of three Boolean functions
satisfy the same first-and-second symmetric-function identity.
Corollary5.6.13
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
Lemma 5.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6corollary-4page-95fidelity-exact

Corollary 4 (Carlet, p. 95). Suppose f_1,f_2,f_3 are bent. If s_1=f_1+f_2+f_3 is bent and \widetilde{s_1}=\widetilde f_1+\widetilde f_2+\widetilde f_3, then s_2=f_1f_2+f_1f_3+f_2f_3 is bent and \widetilde{s_2} =\widetilde f_1\widetilde f_2+ \widetilde f_1\widetilde f_3+ \widetilde f_2\widetilde f_3. Conversely, if 2^{n/2} divides every Walsh coefficient of s_2, then s_1 is bent.

Lean code for Corollary5.6.13●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter06/ThreeFunctionBent.lean
    complete
    theorem CryptBoolean.isBent_threeFunctionPairwiseProductSum_and_bentDual_eq
  {n : ℕ} (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) (_hnEven : Even n)
  (_hnTwo : 2 ≤ n) (hf₁ : CryptBoolean.IsBent f₁)
  (hf₂ : CryptBoolean.IsBent f₂) (hf₃ : CryptBoolean.IsBent f₃)
  (hsum : CryptBoolean.IsBent (CryptBoolean.threeFunctionSum f₁ f₂ f₃))
  (hdual :
    CryptBoolean.bentDual (CryptBoolean.threeFunctionSum f₁ f₂ f₃) =
      CryptBoolean.bentDual f₁ + CryptBoolean.bentDual f₂ +
        CryptBoolean.bentDual f₃) :
  CryptBoolean.IsBent
      (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃) ∧
    CryptBoolean.bentDual
        (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃) =
      CryptBoolean.threeFunctionPairwiseProductSum
        (CryptBoolean.bentDual f₁) (CryptBoolean.bentDual f₂)
        (CryptBoolean.bentDual f₃)
    theorem CryptBoolean.isBent_threeFunctionPairwiseProductSum_and_bentDual_eq
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n)
  (_hnEven : Even n) (_hnTwo : 2 ≤ n)
  (hf₁ : CryptBoolean.IsBent f₁)
  (hf₂ : CryptBoolean.IsBent f₂)
  (hf₃ : CryptBoolean.IsBent f₃)
  (hsum :
    CryptBoolean.IsBent
      (CryptBoolean.threeFunctionSum f₁ f₂
        f₃))
  (hdual :
    CryptBoolean.bentDual
        (CryptBoolean.threeFunctionSum f₁
          f₂ f₃) =
      CryptBoolean.bentDual f₁ +
          CryptBoolean.bentDual f₂ +
        CryptBoolean.bentDual f₃) :
  CryptBoolean.IsBent
      (CryptBoolean.threeFunctionPairwiseProductSum
        f₁ f₂ f₃) ∧
    CryptBoolean.bentDual
        (CryptBoolean.threeFunctionPairwiseProductSum
          f₁ f₂ f₃) =
      CryptBoolean.threeFunctionPairwiseProductSum
        (CryptBoolean.bentDual f₁)
        (CryptBoolean.bentDual f₂)
        (CryptBoolean.bentDual f₃)
    Carlet Corollary 4, first assertion: when the dual of the bent sum is the
sum of the three duals, the second elementary symmetric function is bent and
its dual is the second elementary symmetric function of the three duals.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/ThreeFunctionBent.lean
    complete
    theorem CryptBoolean.isBent_threeFunctionSum_of_two_pow_half_dvd_walshTransform
  {n : ℕ} (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) (hnEven : Even n)
  (hnTwo : 2 ≤ n) (hf₁ : CryptBoolean.IsBent f₁)
  (hf₂ : CryptBoolean.IsBent f₂) (hf₃ : CryptBoolean.IsBent f₃)
  (hdiv :
    ∀ (a : FABL.F₂Cube n),
      2 ^ (n / 2) ∣
        CryptBoolean.walshTransform
          (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃) a) :
  CryptBoolean.IsBent (CryptBoolean.threeFunctionSum f₁ f₂ f₃)
    theorem CryptBoolean.isBent_threeFunctionSum_of_two_pow_half_dvd_walshTransform
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n)
  (hnEven : Even n) (hnTwo : 2 ≤ n)
  (hf₁ : CryptBoolean.IsBent f₁)
  (hf₂ : CryptBoolean.IsBent f₂)
  (hf₃ : CryptBoolean.IsBent f₃)
  (hdiv :
    ∀ (a : FABL.F₂Cube n),
      2 ^ (n / 2) ∣
        CryptBoolean.walshTransform
          (CryptBoolean.threeFunctionPairwiseProductSum
            f₁ f₂ f₃)
          a) :
  CryptBoolean.IsBent
    (CryptBoolean.threeFunctionSum f₁ f₂
      f₃)
    Carlet Corollary 4, second assertion: in even dimension at least two, if
every Walsh coefficient of the second elementary symmetric function is
divisible by `2^(n/2)`, then the first elementary symmetric function is bent.