Cryptographic Boolean Functions in Lean

5.12. Hyper-bent functions🔗

Definition5.12.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 3
Statement dependency previews
Preview
Definition 1.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 5.12.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6hyper-bentpages-100-101fidelity-exact

Hyper-bent functions (Carlet, pp. 100--101). Let n be even and f:\operatorname{GF}(2^n)\to\mathbb F_2. The function f is hyper-bent when, for every integer i coprime to 2^n-1, every a in the field, and both \varepsilon\in\mathbb F_2, its distance to x\mapsto\operatorname{Tr}_n(ax^i)+\varepsilon is 2^{n-1}\pm2^{n/2-1}. Equivalently, every function x\mapsto f(x^i) is bent. In particular, every hyper-bent function is bent.

Lean code for Definition5.12.1●13 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    def CryptBoolean.fieldWalshTransform {n : ℕ}
  (f : CryptBoolean.FieldBooleanFunction n)
  (a : CryptBoolean.BinaryGaloisField n) : ℤ
    def CryptBoolean.fieldWalshTransform {n : ℕ}
  (f :
    CryptBoolean.FieldBooleanFunction n)
  (a : CryptBoolean.BinaryGaloisField n) :
  ℤ
    The raw Walsh transform of a Boolean function represented on `GF(2^n)`,
using the absolute-trace pairing for its linear characters.
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    def CryptBoolean.IsFieldBent {n : ℕ}
  (f : CryptBoolean.FieldBooleanFunction n) : Prop
    def CryptBoolean.IsFieldBent {n : ℕ}
  (f :
    CryptBoolean.FieldBooleanFunction n) :
  Prop
    Bentness in finite-field coordinates.
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    def CryptBoolean.fieldPowerReindex {n : ℕ}
  (f : CryptBoolean.FieldBooleanFunction n) (i : ℕ) :
  CryptBoolean.FieldBooleanFunction n
    def CryptBoolean.fieldPowerReindex {n : ℕ}
  (f :
    CryptBoolean.FieldBooleanFunction n)
  (i : ℕ) :
  CryptBoolean.FieldBooleanFunction n
    Reindex a finite-field Boolean function by a power map.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.fieldPowerMap_bijective {n i : ℕ} (hn : 2 ≤ n)
  (hi : i.Coprime (2 ^ n - 1)) : Function.Bijective fun x => x ^ i
    theorem CryptBoolean.fieldPowerMap_bijective
  {n i : ℕ} (hn : 2 ≤ n)
  (hi : i.Coprime (2 ^ n - 1)) :
  Function.Bijective fun x => x ^ i
    A power map with exponent coprime to the order of the multiplicative
group is a permutation of `GF(2^n)`.
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    def CryptBoolean.fieldPowerEquiv {n i : ℕ} (hn : 2 ≤ n)
  (hi : i.Coprime (2 ^ n - 1)) :
  CryptBoolean.BinaryGaloisField n ≃ CryptBoolean.BinaryGaloisField n
    def CryptBoolean.fieldPowerEquiv {n i : ℕ}
  (hn : 2 ≤ n)
  (hi : i.Coprime (2 ^ n - 1)) :
  CryptBoolean.BinaryGaloisField n ≃
    CryptBoolean.BinaryGaloisField n
    The power permutation attached to a coprime exponent.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.fieldPowerEquiv_apply {n i : ℕ} (hn : 2 ≤ n)
  (hi : i.Coprime (2 ^ n - 1)) (x : CryptBoolean.BinaryGaloisField n) :
  (CryptBoolean.fieldPowerEquiv hn hi) x = x ^ i
    theorem CryptBoolean.fieldPowerEquiv_apply
  {n i : ℕ} (hn : 2 ≤ n)
  (hi : i.Coprime (2 ^ n - 1))
  (x : CryptBoolean.BinaryGaloisField n) :
  (CryptBoolean.fieldPowerEquiv hn hi) x =
    x ^ i
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.fieldPowerReindex_eq_comp_fieldPowerEquiv {n : ℕ}
  (f : CryptBoolean.FieldBooleanFunction n) {i : ℕ} (hn : 2 ≤ n)
  (hi : i.Coprime (2 ^ n - 1)) :
  CryptBoolean.fieldPowerReindex f i =
    f ∘ ⇑(CryptBoolean.fieldPowerEquiv hn hi)
    theorem CryptBoolean.fieldPowerReindex_eq_comp_fieldPowerEquiv
  {n : ℕ}
  (f :
    CryptBoolean.FieldBooleanFunction n)
  {i : ℕ} (hn : 2 ≤ n)
  (hi : i.Coprime (2 ^ n - 1)) :
  CryptBoolean.fieldPowerReindex f i =
    f ∘
      ⇑(CryptBoolean.fieldPowerEquiv hn
          hi)
    Power reindexing is precomposition by the corresponding field
permutation.
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    def CryptBoolean.IsHyperBent {n : ℕ}
  (f : CryptBoolean.FieldBooleanFunction n) : Prop
    def CryptBoolean.IsHyperBent {n : ℕ}
  (f :
    CryptBoolean.FieldBooleanFunction n) :
  Prop
    Carlet's hyper-bent predicate: in even dimension, every power reindexing
whose exponent is coprime to `2^n-1` is bent.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.exists_fieldWalshTransform_eq_walshTransform {n : ℕ}
  (theta : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (f : CryptBoolean.FieldBooleanFunction n) (u : FABL.F₂Cube n) :
  ∃ a,
    CryptBoolean.fieldWalshTransform f a =
      CryptBoolean.walshTransform (f ∘ ⇑theta) u
    theorem CryptBoolean.exists_fieldWalshTransform_eq_walshTransform
  {n : ℕ}
  (theta :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (f :
    CryptBoolean.FieldBooleanFunction n)
  (u : FABL.F₂Cube n) :
  ∃ a,
    CryptBoolean.fieldWalshTransform f a =
      CryptBoolean.walshTransform
        (f ∘ ⇑theta) u
    Every cube frequency has a unique finite-field trace coefficient, so its
raw Walsh coefficient is a field Walsh coefficient.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.exists_walshTransform_eq_fieldWalshTransform {n : ℕ}
  (theta : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (f : CryptBoolean.FieldBooleanFunction n)
  (a : CryptBoolean.BinaryGaloisField n) :
  ∃ u,
    CryptBoolean.walshTransform (f ∘ ⇑theta) u =
      CryptBoolean.fieldWalshTransform f a
    theorem CryptBoolean.exists_walshTransform_eq_fieldWalshTransform
  {n : ℕ}
  (theta :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (f :
    CryptBoolean.FieldBooleanFunction n)
  (a : CryptBoolean.BinaryGaloisField n) :
  ∃ u,
    CryptBoolean.walshTransform
        (f ∘ ⇑theta) u =
      CryptBoolean.fieldWalshTransform f a
    Conversely, every finite-field trace coefficient is represented by a
cube frequency under any linear choice of field coordinates.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.isFieldBent_iff_isBent_comp_linearEquiv {n : ℕ}
  (theta : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (f : CryptBoolean.FieldBooleanFunction n) :
  CryptBoolean.IsFieldBent f ↔ CryptBoolean.IsBent (f ∘ ⇑theta)
    theorem CryptBoolean.isFieldBent_iff_isBent_comp_linearEquiv
  {n : ℕ}
  (theta :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (f :
    CryptBoolean.FieldBooleanFunction n) :
  CryptBoolean.IsFieldBent f ↔
    CryptBoolean.IsBent (f ∘ ⇑theta)
    Finite-field bentness agrees with canonical cube bentness under every
linear coordinate identification.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.IsHyperBent.isFieldBent {n : ℕ}
  {f : CryptBoolean.FieldBooleanFunction n}
  (hf : CryptBoolean.IsHyperBent f) : CryptBoolean.IsFieldBent f
    theorem CryptBoolean.IsHyperBent.isFieldBent
  {n : ℕ}
  {f :
    CryptBoolean.FieldBooleanFunction n}
  (hf : CryptBoolean.IsHyperBent f) :
  CryptBoolean.IsFieldBent f
    The power exponent `1` shows that every hyper-bent function is bent.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.isHyperBent_iff_forall_isBent_powerReindex_comp_linearEquiv
  {n : ℕ}
  (theta : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField n)
  (f : CryptBoolean.FieldBooleanFunction n) :
  CryptBoolean.IsHyperBent f ↔
    Even n ∧
      ∀ (i : ℕ),
        i.Coprime (2 ^ n - 1) →
          CryptBoolean.IsBent
            (CryptBoolean.fieldPowerReindex f i ∘ ⇑theta)
    theorem CryptBoolean.isHyperBent_iff_forall_isBent_powerReindex_comp_linearEquiv
  {n : ℕ}
  (theta :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (f :
    CryptBoolean.FieldBooleanFunction n) :
  CryptBoolean.IsHyperBent f ↔
    Even n ∧
      ∀ (i : ℕ),
        i.Coprime (2 ^ n - 1) →
          CryptBoolean.IsBent
            (CryptBoolean.fieldPowerReindex
                f i ∘
              ⇑theta)
    Coordinate form of the hyper-bent definition.
Lemma5.12.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
Definition 1.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6lemma-4page-102fidelity-corrected-even-dimension

Lemma 4 (Carlet, p. 102; corrected dimension convention). Let m>0, let K=\operatorname{GF}(2^m) be the quadratic subfield of L=\operatorname{GF}(2^{2m}), and let a,\omega\in L\setminus K. If i is coprime to 2^{2m}-1, then there is a unique z\in K such that a(z+\omega)^i\in K.

Lean code for Lemma5.12.2●4 declarations
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.quadraticSubfieldBasisMap_bijective {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (c : CryptBoolean.BinaryGaloisField (2 * m))
  (hc : c ∉ Set.range ⇑iota) :
  Function.Bijective fun p => iota p.1 + c * iota p.2
    theorem CryptBoolean.quadraticSubfieldBasisMap_bijective
  {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (c :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (hc : c ∉ Set.range ⇑iota) :
  Function.Bijective fun p =>
    iota p.1 + c * iota p.2
    The two directions `1` and `c` span the quadratic extension when `c`
does not lie in the embedded subfield.
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    def CryptBoolean.quadraticSubfieldBasisEquiv {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (c : CryptBoolean.BinaryGaloisField (2 * m))
  (hc : c ∉ Set.range ⇑iota) :
  CryptBoolean.BinaryGaloisField m × CryptBoolean.BinaryGaloisField m ≃
    CryptBoolean.BinaryGaloisField (2 * m)
    def CryptBoolean.quadraticSubfieldBasisEquiv
  {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (c :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (hc : c ∉ Set.range ⇑iota) :
  CryptBoolean.BinaryGaloisField m ×
      CryptBoolean.BinaryGaloisField m ≃
    CryptBoolean.BinaryGaloisField (2 * m)
    Coordinates in a quadratic binary extension relative to the basis
formed by `1` and an element outside the embedded subfield.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.quadraticSubfieldBasisEquiv_apply {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (c : CryptBoolean.BinaryGaloisField (2 * m))
  (hc : c ∉ Set.range ⇑iota)
  (p :
    CryptBoolean.BinaryGaloisField m ×
      CryptBoolean.BinaryGaloisField m) :
  (CryptBoolean.quadraticSubfieldBasisEquiv hm iota c hc) p =
    iota p.1 + c * iota p.2
    theorem CryptBoolean.quadraticSubfieldBasisEquiv_apply
  {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (c :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (hc : c ∉ Set.range ⇑iota)
  (p :
    CryptBoolean.BinaryGaloisField m ×
      CryptBoolean.BinaryGaloisField m) :
  (CryptBoolean.quadraticSubfieldBasisEquiv
        hm iota c hc)
      p =
    iota p.1 + c * iota p.2
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.existsUnique_subfield_power_intersection {m i : ℕ}
  (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (a omega : CryptBoolean.BinaryGaloisField (2 * m))
  (ha : a ∉ Set.range ⇑iota) (_homega : omega ∉ Set.range ⇑iota)
  (hi : i.Coprime (2 ^ (2 * m) - 1)) :
  ∃! z, ∃ k, a * (iota z + omega) ^ i = iota k
    theorem CryptBoolean.existsUnique_subfield_power_intersection
  {m i : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (a omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (ha : a ∉ Set.range ⇑iota)
  (_homega : omega ∉ Set.range ⇑iota)
  (hi : i.Coprime (2 ^ (2 * m) - 1)) :
  ∃! z,
    ∃ k, a * (iota z + omega) ^ i = iota k
    Carlet Lemma 4: a coprime power of a translated quadratic-subfield
line meets every non-subfield scalar multiple of the subfield exactly once.
Proposition5.12.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
Theorem 4.2.10
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6proposition-25pages-101-102fidelity-corrected-positive-half-dimension

Proposition 25 (Carlet, pp. 101--102). Let m\ge2, put K=\operatorname{GF}(2^m) and L=\operatorname{GF}(2^{2m}), choose \omega\in L\setminus K, and write every x\in L uniquely as x=y'+\omega y with y',y\in K. If g:K\to\mathbb F_2 is balanced and g(0)=0, define f(y'+\omega y)=g(y'/y), with y'/y=0 when y=0. Then f is hyper-bent. Equivalently, every function in Dillon's class PS_{ap} is hyper-bent.

Lean code for Proposition5.12.3●15 declarations
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.quadraticSubfield_powerMap_bijective {m i : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (hi : i.Coprime (2 ^ (2 * m) - 1)) : Function.Bijective fun r => r ^ i
    theorem CryptBoolean.quadraticSubfield_powerMap_bijective
  {m i : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (hi : i.Coprime (2 ^ (2 * m) - 1)) :
  Function.Bijective fun r => r ^ i
    A coprime power permutation of the quadratic extension restricts to a
power permutation of its embedded middle field.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBent.lean
    complete
    theorem CryptBoolean.pow_mem_quadraticSubfield_iff {m i : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (hi : i.Coprime (2 ^ (2 * m) - 1))
  (x : CryptBoolean.BinaryGaloisField (2 * m)) :
  x ^ i ∈ Set.range ⇑iota ↔ x ∈ Set.range ⇑iota
    theorem CryptBoolean.pow_mem_quadraticSubfield_iff
  {m i : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (hi : i.Coprime (2 ^ (2 * m) - 1))
  (x :
    CryptBoolean.BinaryGaloisField
      (2 * m)) :
  x ^ i ∈ Set.range ⇑iota ↔
    x ∈ Set.range ⇑iota
    Membership in the quadratic subfield is invariant under every coprime
power permutation of the ambient field.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.relativeTrace_eq_zero_iff_mem_quadraticSubfield {m : ℕ}
  (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (x : CryptBoolean.BinaryGaloisField (2 * m)) :
  (Algebra.trace (CryptBoolean.BinaryGaloisField m)
          (CryptBoolean.BinaryGaloisField (2 * m)))
        x =
      0 ↔
    x ∈ Set.range ⇑iota
    theorem CryptBoolean.relativeTrace_eq_zero_iff_mem_quadraticSubfield
  {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (x :
    CryptBoolean.BinaryGaloisField
      (2 * m)) :
  (Algebra.trace
          (CryptBoolean.BinaryGaloisField
            m)
          (CryptBoolean.BinaryGaloisField
            (2 * m)))
        x =
      0 ↔
    x ∈ Set.range ⇑iota
    In a quadratic binary extension, the kernel of the relative trace is
exactly the embedded middle field.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.absoluteTrace_mul_quadraticSubfield {m : ℕ}
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (x : CryptBoolean.BinaryGaloisField (2 * m))
  (y : CryptBoolean.BinaryGaloisField m) :
  (CryptBoolean.absoluteTrace (2 * m)) (x * iota y) =
    (CryptBoolean.absoluteTrace m)
      ((Algebra.trace (CryptBoolean.BinaryGaloisField m)
            (CryptBoolean.BinaryGaloisField (2 * m)))
          x *
        y)
    theorem CryptBoolean.absoluteTrace_mul_quadraticSubfield
  {m : ℕ}
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (x :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (y : CryptBoolean.BinaryGaloisField m) :
  (CryptBoolean.absoluteTrace (2 * m))
      (x * iota y) =
    (CryptBoolean.absoluteTrace m)
      ((Algebra.trace
            (CryptBoolean.BinaryGaloisField
              m)
            (CryptBoolean.BinaryGaloisField
              (2 * m)))
          x *
        y)
    The absolute trace of a product with an embedded middle-field element
factors through the relative trace.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.sum_bitSignInt_absoluteTrace_mul_eq_zero {m : ℕ}
  (t : CryptBoolean.BinaryGaloisField m) (ht : t ≠ 0) :
  ∑ y,
      CryptBoolean.bitSignInt ((CryptBoolean.absoluteTrace m) (t * y)) =
    0
    theorem CryptBoolean.sum_bitSignInt_absoluteTrace_mul_eq_zero
  {m : ℕ}
  (t : CryptBoolean.BinaryGaloisField m)
  (ht : t ≠ 0) :
  ∑ y,
      CryptBoolean.bitSignInt
        ((CryptBoolean.absoluteTrace m)
          (t * y)) =
    0
    Every nontrivial absolute-trace additive character has zero sum over a binary field.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.sum_quadraticSubfieldTraceCharacter_of_mem {m : ℕ}
  (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (x : CryptBoolean.BinaryGaloisField (2 * m))
  (hx : x ∈ Set.range ⇑iota) :
  ∑ y,
      CryptBoolean.bitSignInt
        ((CryptBoolean.absoluteTrace (2 * m)) (x * iota y)) =
    2 ^ m
    theorem CryptBoolean.sum_quadraticSubfieldTraceCharacter_of_mem
  {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (x :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (hx : x ∈ Set.range ⇑iota) :
  ∑ y,
      CryptBoolean.bitSignInt
        ((CryptBoolean.absoluteTrace
            (2 * m))
          (x * iota y)) =
    2 ^ m
    A quadratic-extension trace character sums to the middle-field cardinality
when its coefficient lies in the middle field.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.sum_quadraticSubfieldTraceCharacter_of_not_mem {m : ℕ}
  (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (x : CryptBoolean.BinaryGaloisField (2 * m))
  (hx : x ∉ Set.range ⇑iota) :
  ∑ y,
      CryptBoolean.bitSignInt
        ((CryptBoolean.absoluteTrace (2 * m)) (x * iota y)) =
    0
    theorem CryptBoolean.sum_quadraticSubfieldTraceCharacter_of_not_mem
  {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (x :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (hx : x ∉ Set.range ⇑iota) :
  ∑ y,
      CryptBoolean.bitSignInt
        ((CryptBoolean.absoluteTrace
            (2 * m))
          (x * iota y)) =
    0
    A quadratic-extension trace character sums to zero when its coefficient
lies outside the middle field.
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    def CryptBoolean.psapFunction {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (g : CryptBoolean.FieldBooleanFunction m) :
  CryptBoolean.FieldBooleanFunction (2 * m)
    def CryptBoolean.psapFunction {m : ℕ}
  (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (g :
    CryptBoolean.FieldBooleanFunction m) :
  CryptBoolean.FieldBooleanFunction
    (2 * m)
    Dillon's partial-spread function in quadratic-extension coordinates, with
field division defining the zero-denominator case.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.psapFunction_coordinate {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (g : CryptBoolean.FieldBooleanFunction m)
  (y' y : CryptBoolean.BinaryGaloisField m) :
  CryptBoolean.psapFunction hm iota omega homega g
      (iota y' + omega * iota y) =
    g (y' / y)
    theorem CryptBoolean.psapFunction_coordinate
  {m : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (g :
    CryptBoolean.FieldBooleanFunction m)
  (y' y :
    CryptBoolean.BinaryGaloisField m) :
  CryptBoolean.psapFunction hm iota omega
      homega g
      (iota y' + omega * iota y) =
    g (y' / y)
    The partial-spread function evaluates to the quotient rule in its defining
quadratic-extension coordinates.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.sum_bitSignInt_field_eq_zero_of_balanced {m : ℕ}
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (g : CryptBoolean.FieldBooleanFunction m)
  (hg : CryptBoolean.IsBalanced (g ∘ ⇑theta)) :
  ∑ z, CryptBoolean.bitSignInt (g z) = 0
    theorem CryptBoolean.sum_bitSignInt_field_eq_zero_of_balanced
  {m : ℕ}
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (g :
    CryptBoolean.FieldBooleanFunction m)
  (hg :
    CryptBoolean.IsBalanced
      (g ∘ ⇑theta)) :
  ∑ z, CryptBoolean.bitSignInt (g z) = 0
    The sign sum of a field Boolean function vanishes when its pullback to the
Boolean cube is balanced.
  • defdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    def CryptBoolean.fieldPowerTraceTransform {n : ℕ}
  (f : CryptBoolean.FieldBooleanFunction n) (i : ℕ)
  (a : CryptBoolean.BinaryGaloisField n) : ℤ
    def CryptBoolean.fieldPowerTraceTransform
  {n : ℕ}
  (f :
    CryptBoolean.FieldBooleanFunction n)
  (i : ℕ)
  (a : CryptBoolean.BinaryGaloisField n) :
  ℤ
    The source-normalized power-trace transform used in the hyper-bent criterion.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.fieldPowerTraceTransform_psap_eq {m i : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (g : CryptBoolean.FieldBooleanFunction m) (hg0 : g 0 = 0)
  (hi : i.Coprime (2 ^ (2 * m) - 1))
  (a : CryptBoolean.BinaryGaloisField (2 * m)) :
  CryptBoolean.fieldPowerTraceTransform
      (CryptBoolean.psapFunction hm iota omega homega g) i a =
    ∑ y,
        CryptBoolean.bitSignInt
          ((CryptBoolean.absoluteTrace (2 * m)) (a * iota y)) +
      ∑ z,
        CryptBoolean.bitSignInt (g z) *
          (∑ y,
              CryptBoolean.bitSignInt
                ((CryptBoolean.absoluteTrace (2 * m))
                  (a * (iota z + omega) ^ i * iota y)) -
            1)
    theorem CryptBoolean.fieldPowerTraceTransform_psap_eq
  {m i : ℕ} (hm : 0 < m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (g :
    CryptBoolean.FieldBooleanFunction m)
  (hg0 : g 0 = 0)
  (hi : i.Coprime (2 ^ (2 * m) - 1))
  (a :
    CryptBoolean.BinaryGaloisField
      (2 * m)) :
  CryptBoolean.fieldPowerTraceTransform
      (CryptBoolean.psapFunction hm iota
        omega homega g)
      i a =
    ∑ y,
        CryptBoolean.bitSignInt
          ((CryptBoolean.absoluteTrace
              (2 * m))
            (a * iota y)) +
      ∑ z,
        CryptBoolean.bitSignInt (g z) *
          (∑ y,
              CryptBoolean.bitSignInt
                ((CryptBoolean.absoluteTrace
                    (2 * m))
                  (a *
                      (iota z + omega) ^
                        i *
                    iota y)) -
            1)
    The power-trace transform of a partial-spread function decomposes into
middle-field character sums.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.fieldPowerTraceTransform_psap_natAbs {m i : ℕ} (hm : 2 ≤ m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (g : CryptBoolean.FieldBooleanFunction m)
  (hg : CryptBoolean.IsBalanced (g ∘ ⇑theta)) (hg0 : g 0 = 0)
  (hi : i.Coprime (2 ^ (2 * m) - 1))
  (a : CryptBoolean.BinaryGaloisField (2 * m)) :
  (CryptBoolean.fieldPowerTraceTransform
        (CryptBoolean.psapFunction ⋯ iota omega homega g) i a).natAbs =
    2 ^ m
    theorem CryptBoolean.fieldPowerTraceTransform_psap_natAbs
  {m i : ℕ} (hm : 2 ≤ m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (g :
    CryptBoolean.FieldBooleanFunction m)
  (hg :
    CryptBoolean.IsBalanced (g ∘ ⇑theta))
  (hg0 : g 0 = 0)
  (hi : i.Coprime (2 ^ (2 * m) - 1))
  (a :
    CryptBoolean.BinaryGaloisField
      (2 * m)) :
  (CryptBoolean.fieldPowerTraceTransform
        (CryptBoolean.psapFunction ⋯ iota
          omega homega g)
        i a).natAbs =
    2 ^ m
    Every coprime power-trace transform of a partial-spread function has bent magnitude.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.isHyperBent_of_forall_fieldPowerTraceTransform {n : ℕ}
  (hn : 2 ≤ n) (hnEven : Even n)
  (f : CryptBoolean.FieldBooleanFunction n)
  (htransform :
    ∀ (i : ℕ),
      i.Coprime (2 ^ n - 1) →
        ∀ (a : CryptBoolean.BinaryGaloisField n),
          (CryptBoolean.fieldPowerTraceTransform f i a).natAbs =
            2 ^ (n / 2)) :
  CryptBoolean.IsHyperBent f
    theorem CryptBoolean.isHyperBent_of_forall_fieldPowerTraceTransform
  {n : ℕ} (hn : 2 ≤ n) (hnEven : Even n)
  (f :
    CryptBoolean.FieldBooleanFunction n)
  (htransform :
    ∀ (i : ℕ),
      i.Coprime (2 ^ n - 1) →
        ∀
          (a :
            CryptBoolean.BinaryGaloisField
              n),
          (CryptBoolean.fieldPowerTraceTransform
                f i a).natAbs =
            2 ^ (n / 2)) :
  CryptBoolean.IsHyperBent f
    Constant bent magnitude for all coprime power-trace transforms implies hyper-bentness.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/HyperBentPartialSpread.lean
    complete
    theorem CryptBoolean.isHyperBent_psapFunction {m : ℕ} (hm : 2 ≤ m)
  (iota :
    CryptBoolean.BinaryGaloisField m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * m))
  (omega : CryptBoolean.BinaryGaloisField (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] CryptBoolean.BinaryGaloisField m)
  (g : CryptBoolean.FieldBooleanFunction m)
  (hg : CryptBoolean.IsBalanced (g ∘ ⇑theta)) (hg0 : g 0 = 0) :
  CryptBoolean.IsHyperBent
    (CryptBoolean.psapFunction ⋯ iota omega homega g)
    theorem CryptBoolean.isHyperBent_psapFunction
  {m : ℕ} (hm : 2 ≤ m)
  (iota :
    CryptBoolean.BinaryGaloisField
        m →ₐ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * m))
  (omega :
    CryptBoolean.BinaryGaloisField
      (2 * m))
  (homega : omega ∉ Set.range ⇑iota)
  (theta :
    FABL.F₂Cube m ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField m)
  (g :
    CryptBoolean.FieldBooleanFunction m)
  (hg :
    CryptBoolean.IsBalanced (g ∘ ⇑theta))
  (hg0 : g 0 = 0) :
  CryptBoolean.IsHyperBent
    (CryptBoolean.psapFunction ⋯ iota
      omega homega g)
    Carlet Proposition 25: every partial-spread function of the stated quotient
form is hyper-bent.