Cryptographic Boolean Functions in Lean

5.10. Geometric characterization🔗

Lemma5.10.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.
uses 0used by 1✓L∃∀N
Tagscarletchapter-6lemma-3subspace-indicatorssection-6-6-2page-99fidelity-exact

Lemma 3 (Carlet, p. 99). Let n be even and let F\le V_n have dimension d. There are n/2-dimensional subspaces E_1,\ldots,E_k, integers m_1,\ldots,m_k, and an integer m such that, pointwise on V_n, 2^{n/2-d}1_F\equiv m+\sum_{i=1}^k m_i1_{E_i} \pmod {2^{n/2}} \qquad(d<n/2), and there are n/2-dimensional subspaces E_1,\ldots,E_k and integers m_1,\ldots,m_k such that 1_F\equiv\sum_{i=1}^k m_i1_{E_i} \pmod {2^{n/2}} \qquad(d>n/2).

Lean code for Lemma5.10.1●18 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.linearSubspaceIndicatorInt {n : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (x : FABL.F₂Cube n) : ℤ
    def CryptBoolean.linearSubspaceIndicatorInt
  {n : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (x : FABL.F₂Cube n) : ℤ
    The integer indicator of a binary linear subspace.
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.halfSubspaceCombination {n : ℕ}
  (c : Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ) (x : FABL.F₂Cube n) : ℤ
    def CryptBoolean.halfSubspaceCombination
  {n : ℕ}
  (c :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ)
  (x : FABL.F₂Cube n) : ℤ
    An integer combination of all half-dimensional subspace indicators.
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.ambientFunctionalKernel {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (ell : Module.Dual FABL.𝔽₂ ↥F) : Submodule FABL.𝔽₂ (FABL.F₂Cube n)
    def CryptBoolean.ambientFunctionalKernel
  {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (ell : Module.Dual FABL.𝔽₂ ↥F) :
  Submodule FABL.𝔽₂ (FABL.F₂Cube n)
    The ambient image of the kernel of a linear functional on a subspace.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.mem_ambientFunctionalKernel_iff {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (ell : Module.Dual FABL.𝔽₂ ↥F)
  (x : FABL.F₂Cube n) (hx : x ∈ F) :
  x ∈ CryptBoolean.ambientFunctionalKernel F ell ↔ ell ⟨x, hx⟩ = 0
    theorem CryptBoolean.mem_ambientFunctionalKernel_iff
  {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (ell : Module.Dual FABL.𝔽₂ ↥F)
  (x : FABL.F₂Cube n) (hx : x ∈ F) :
  x ∈
      CryptBoolean.ambientFunctionalKernel
        F ell ↔
    ell ⟨x, hx⟩ = 0
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.finrank_ambientFunctionalKernel {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (ell : Module.Dual FABL.𝔽₂ ↥F)
  (hell : ell ≠ 0) :
  Module.finrank FABL.𝔽₂ ↥(CryptBoolean.ambientFunctionalKernel F ell) +
      1 =
    Module.finrank FABL.𝔽₂ ↥F
    theorem CryptBoolean.finrank_ambientFunctionalKernel
  {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (ell : Module.Dual FABL.𝔽₂ ↥F)
  (hell : ell ≠ 0) :
  Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.ambientFunctionalKernel
            F ell) +
      1 =
    Module.finrank FABL.𝔽₂ ↥F
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.nonzeroDualFinset.{u_1} (V : Type u_1) [Finite V]
  [AddCommGroup V] [Module FABL.𝔽₂ V] : Finset (Module.Dual FABL.𝔽₂ V)
    def CryptBoolean.nonzeroDualFinset.{u_1}
  (V : Type u_1) [Finite V]
  [AddCommGroup V] [Module FABL.𝔽₂ V] :
  Finset (Module.Dual FABL.𝔽₂ V)
    The finite set of nonzero linear functionals on a subspace.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.mem_nonzeroDualFinset.{u_1} (V : Type u_1) [Finite V]
  [AddCommGroup V] [Module FABL.𝔽₂ V] (ell : Module.Dual FABL.𝔽₂ V) :
  ell ∈ CryptBoolean.nonzeroDualFinset V ↔ ell ≠ 0
    theorem CryptBoolean.mem_nonzeroDualFinset.{u_1}
  (V : Type u_1) [Finite V]
  [AddCommGroup V] [Module FABL.𝔽₂ V]
  (ell : Module.Dual FABL.𝔽₂ V) :
  ell ∈ CryptBoolean.nonzeroDualFinset V ↔
    ell ≠ 0
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.card_nonzeroDualFinset.{u_1} (V : Type u_1) [Finite V]
  [AddCommGroup V] [Module FABL.𝔽₂ V] :
  (CryptBoolean.nonzeroDualFinset V).card =
    2 ^ Module.finrank FABL.𝔽₂ V - 1
    theorem CryptBoolean.card_nonzeroDualFinset.{u_1}
  (V : Type u_1) [Finite V]
  [AddCommGroup V] [Module FABL.𝔽₂ V] :
  (CryptBoolean.nonzeroDualFinset
        V).card =
    2 ^ Module.finrank FABL.𝔽₂ V - 1
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.functionalKernelCombination_modeq {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (hF : n / 2 < Module.finrank FABL.𝔽₂ ↥F) (x : FABL.F₂Cube n) :
  CryptBoolean.linearSubspaceIndicatorInt F x ≡
    -∑ ell ∈ CryptBoolean.nonzeroDualFinset ↥F,
        CryptBoolean.linearSubspaceIndicatorInt
          (CryptBoolean.ambientFunctionalKernel F ell) x [ZMOD
    2 ^ (n / 2)]
    theorem CryptBoolean.functionalKernelCombination_modeq
  {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (hF : n / 2 < Module.finrank FABL.𝔽₂ ↥F)
  (x : FABL.F₂Cube n) :
  CryptBoolean.linearSubspaceIndicatorInt
      F x ≡
    -∑
        ell ∈
          CryptBoolean.nonzeroDualFinset
            ↥F,
        CryptBoolean.linearSubspaceIndicatorInt
          (CryptBoolean.ambientFunctionalKernel
            F ell)
          x [ZMOD
    2 ^ (n / 2)]
    Above half dimension, the indicator of a subspace is congruent modulo
`2^(n/2)` to the negative sum of the indicators of the kernels of all its
nonzero linear functionals.
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.HasHalfSubspaceRepresentation {n : ℕ}
  (g : FABL.F₂Cube n → ℤ) : Prop
    def CryptBoolean.HasHalfSubspaceRepresentation
  {n : ℕ} (g : FABL.F₂Cube n → ℤ) : Prop
    An integer-valued function is representable modulo `2^(n/2)` by an
integer combination of half-dimensional subspace indicators.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.hasHalfSubspaceRepresentation_indicator_of_finrank_eq
  {n : ℕ} (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (hF : Module.finrank FABL.𝔽₂ ↥F = n / 2) :
  CryptBoolean.HasHalfSubspaceRepresentation
    (CryptBoolean.linearSubspaceIndicatorInt F)
    theorem CryptBoolean.hasHalfSubspaceRepresentation_indicator_of_finrank_eq
  {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (hF :
    Module.finrank FABL.𝔽₂ ↥F = n / 2) :
  CryptBoolean.HasHalfSubspaceRepresentation
    (CryptBoolean.linearSubspaceIndicatorInt
      F)
    The indicator of a half-dimensional subspace is itself a half-subspace
combination.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.hasHalfSubspaceRepresentation_indicator_of_half_le_finrank
  {n : ℕ} (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (hF : n / 2 ≤ Module.finrank FABL.𝔽₂ ↥F) :
  CryptBoolean.HasHalfSubspaceRepresentation
    (CryptBoolean.linearSubspaceIndicatorInt F)
    theorem CryptBoolean.hasHalfSubspaceRepresentation_indicator_of_half_le_finrank
  {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (hF :
    n / 2 ≤ Module.finrank FABL.𝔽₂ ↥F) :
  CryptBoolean.HasHalfSubspaceRepresentation
    (CryptBoolean.linearSubspaceIndicatorInt
      F)
    The high-dimensional branch of Carlet Lemma 3.
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.rankTwoIntermediateSubspace {n : ℕ}
  (F G : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (ell : Module.Dual FABL.𝔽₂ (↥G ⧸ Submodule.comap G.subtype F)) :
  Submodule FABL.𝔽₂ (FABL.F₂Cube n)
    def CryptBoolean.rankTwoIntermediateSubspace
  {n : ℕ}
  (F G :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (ell :
    Module.Dual FABL.𝔽₂
      (↥G ⧸
        Submodule.comap G.subtype F)) :
  Submodule FABL.𝔽₂ (FABL.F₂Cube n)
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.mem_rankTwoIntermediateSubspace_iff {n : ℕ}
  (F G : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (ell : Module.Dual FABL.𝔽₂ (↥G ⧸ Submodule.comap G.subtype F))
  (x : FABL.F₂Cube n) (hxG : x ∈ G) :
  x ∈ CryptBoolean.rankTwoIntermediateSubspace F G ell ↔
    ell ((Submodule.comap G.subtype F).mkQ ⟨x, hxG⟩) = 0
    theorem CryptBoolean.mem_rankTwoIntermediateSubspace_iff
  {n : ℕ}
  (F G :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (ell :
    Module.Dual FABL.𝔽₂
      (↥G ⧸ Submodule.comap G.subtype F))
  (x : FABL.F₂Cube n) (hxG : x ∈ G) :
  x ∈
      CryptBoolean.rankTwoIntermediateSubspace
        F G ell ↔
    ell
        ((Submodule.comap G.subtype F).mkQ
          ⟨x, hxG⟩) =
      0
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.finrank_rankTwoIntermediateSubspace {n : ℕ}
  (F G : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (ell : Module.Dual FABL.𝔽₂ (↥G ⧸ Submodule.comap G.subtype F))
  (hell : ell ≠ 0) :
  Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.rankTwoIntermediateSubspace F G ell) +
      1 =
    Module.finrank FABL.𝔽₂ ↥G
    theorem CryptBoolean.finrank_rankTwoIntermediateSubspace
  {n : ℕ}
  (F G :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (ell :
    Module.Dual FABL.𝔽₂
      (↥G ⧸ Submodule.comap G.subtype F))
  (hell : ell ≠ 0) :
  Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.rankTwoIntermediateSubspace
            F G ell) +
      1 =
    Module.finrank FABL.𝔽₂ ↥G
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.rankTwoSubspaceDiamond {n : ℕ}
  (F G : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (hFG : F ≤ G)
  (hG : Module.finrank FABL.𝔽₂ ↥G = Module.finrank FABL.𝔽₂ ↥F + 2) :
  (∀
      ell ∈
        CryptBoolean.nonzeroDualFinset
          (↥G ⧸ Submodule.comap G.subtype F),
      Module.finrank FABL.𝔽₂
          ↥(CryptBoolean.rankTwoIntermediateSubspace F G ell) =
        Module.finrank FABL.𝔽₂ ↥F + 1) ∧
    ∀ (x : FABL.F₂Cube n),
      ∑
          ell ∈
            CryptBoolean.nonzeroDualFinset
              (↥G ⧸ Submodule.comap G.subtype F),
          CryptBoolean.linearSubspaceIndicatorInt
            (CryptBoolean.rankTwoIntermediateSubspace F G ell) x =
        CryptBoolean.linearSubspaceIndicatorInt G x +
          2 * CryptBoolean.linearSubspaceIndicatorInt F x
    theorem CryptBoolean.rankTwoSubspaceDiamond
  {n : ℕ}
  (F G :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (hFG : F ≤ G)
  (hG :
    Module.finrank FABL.𝔽₂ ↥G =
      Module.finrank FABL.𝔽₂ ↥F + 2) :
  (∀
      ell ∈
        CryptBoolean.nonzeroDualFinset
          (↥G ⧸
            Submodule.comap G.subtype F),
      Module.finrank FABL.𝔽₂
          ↥(CryptBoolean.rankTwoIntermediateSubspace
              F G ell) =
        Module.finrank FABL.𝔽₂ ↥F + 1) ∧
    ∀ (x : FABL.F₂Cube n),
      ∑
          ell ∈
            CryptBoolean.nonzeroDualFinset
              (↥G ⧸
                Submodule.comap G.subtype
                  F),
          CryptBoolean.linearSubspaceIndicatorInt
            (CryptBoolean.rankTwoIntermediateSubspace
              F G ell)
            x =
        CryptBoolean.linearSubspaceIndicatorInt
            G x +
          2 *
            CryptBoolean.linearSubspaceIndicatorInt
              F x
    The rank-two subspace diamond: if `G/F` has dimension two, its three
nonzero dual kernels are the three intermediate subspaces, and their indicator
sum is `1_G + 2·1_F`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.hasHalfSubspaceRepresentation_scaledIndicator_of_finrank_le_half
  {n : ℕ} (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (hn : Even n)
  (hF : Module.finrank FABL.𝔽₂ ↥F ≤ n / 2) :
  CryptBoolean.HasHalfSubspaceRepresentation fun x =>
    2 ^ (n / 2 - Module.finrank FABL.𝔽₂ ↥F) *
      CryptBoolean.linearSubspaceIndicatorInt F x
    theorem CryptBoolean.hasHalfSubspaceRepresentation_scaledIndicator_of_finrank_le_half
  {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (hn : Even n)
  (hF :
    Module.finrank FABL.𝔽₂ ↥F ≤ n / 2) :
  CryptBoolean.HasHalfSubspaceRepresentation
    fun x =>
    2 ^
        (n / 2 -
          Module.finrank FABL.𝔽₂ ↥F) *
      CryptBoolean.linearSubspaceIndicatorInt
        F x
    The low-dimensional branch of Carlet Lemma 3, strengthened so that no
separate constant term is needed.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.carletLemma3 {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (hn : Even n) :
  (Module.finrank FABL.𝔽₂ ↥F < n / 2 →
      ∃ m c,
        ∀ (x : FABL.F₂Cube n),
          2 ^ (n / 2 - Module.finrank FABL.𝔽₂ ↥F) *
              CryptBoolean.linearSubspaceIndicatorInt F x ≡
            m + CryptBoolean.halfSubspaceCombination c x [ZMOD
            2 ^ (n / 2)]) ∧
    (n / 2 < Module.finrank FABL.𝔽₂ ↥F →
      ∃ c,
        ∀ (x : FABL.F₂Cube n),
          CryptBoolean.linearSubspaceIndicatorInt F x ≡
            CryptBoolean.halfSubspaceCombination c x [ZMOD 2 ^ (n / 2)])
    theorem CryptBoolean.carletLemma3 {n : ℕ}
  (F : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (hn : Even n) :
  (Module.finrank FABL.𝔽₂ ↥F < n / 2 →
      ∃ m c,
        ∀ (x : FABL.F₂Cube n),
          2 ^
                (n / 2 -
                  Module.finrank FABL.𝔽₂
                    ↥F) *
              CryptBoolean.linearSubspaceIndicatorInt
                F x ≡
            m +
              CryptBoolean.halfSubspaceCombination
                c x [ZMOD
            2 ^ (n / 2)]) ∧
    (n / 2 < Module.finrank FABL.𝔽₂ ↥F →
      ∃ c,
        ∀ (x : FABL.F₂Cube n),
          CryptBoolean.linearSubspaceIndicatorInt
              F x ≡
            CryptBoolean.halfSubspaceCombination
              c x [ZMOD
            2 ^ (n / 2)])
    Carlet Lemma 3 in its two source-facing branches.
Theorem5.10.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 5
Statement dependency previews
Preview
Proposition 1.8.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6theorem-12relation-51generalized-partial-spreadsection-6-6-2page-99fidelity-exact

Theorem 12 (Carlet, Relation (51), p. 99). Let n\ge2 be even. A Boolean function f:V_n\to\mathbb F_2 is bent if and only if there are n/2-dimensional subspaces E_1,\ldots,E_k\le V_n and integers m_1,\ldots,m_k such that, for every x\in V_n, f(x)\equiv\sum_{i=1}^k m_i1_{E_i}(x)-2^{n/2-1}\delta_0(x) \pmod {2^{n/2}}. If this congruence is an equality over the integers, then f belongs to the generalized partial-spread class and its dual is \widetilde f(x)= \sum_{i=1}^k m_i1_{E_i^\perp}(x)-2^{n/2-1}\delta_0(x). In particular, the dual also belongs to the generalized partial-spread class.

Lean code for Theorem5.10.2●20 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.originIndicatorInt {n : ℕ} (x : FABL.F₂Cube n) : ℤ
    def CryptBoolean.originIndicatorInt {n : ℕ}
  (x : FABL.F₂Cube n) : ℤ
    The integer indicator of the origin.
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.geometricBentExpression {n : ℕ}
  (c : Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ) (x : FABL.F₂Cube n) : ℤ
    def CryptBoolean.geometricBentExpression
  {n : ℕ}
  (c :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ)
  (x : FABL.F₂Cube n) : ℤ
    The right-hand side of Carlet Relation (51).
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.perpendicularGeometricBentExpression {n : ℕ}
  (c : Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ) (x : FABL.F₂Cube n) : ℤ
    def CryptBoolean.perpendicularGeometricBentExpression
  {n : ℕ}
  (c :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ)
  (x : FABL.F₂Cube n) : ℤ
    The expression obtained by replacing every half-dimensional subspace by
its perpendicular subspace.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.integerWalshTransform_linearSubspaceIndicatorInt {n : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (u : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.linearSubspaceIndicatorInt E) u =
    2 ^ Module.finrank FABL.𝔽₂ ↥E *
      CryptBoolean.linearSubspaceIndicatorInt
        (FABL.perpendicularSubspace E) u
    theorem CryptBoolean.integerWalshTransform_linearSubspaceIndicatorInt
  {n : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (u : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.linearSubspaceIndicatorInt
        E)
      u =
    2 ^ Module.finrank FABL.𝔽₂ ↥E *
      CryptBoolean.linearSubspaceIndicatorInt
        (FABL.perpendicularSubspace E) u
    Carlet Relation (16) in the integral normalization: the integer Fourier
transform of a subspace indicator is its cardinality on the perpendicular
subspace.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.integerWalshTransform_originIndicatorInt {n : ℕ}
  (u : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform CryptBoolean.originIndicatorInt u =
    1
    theorem CryptBoolean.integerWalshTransform_originIndicatorInt
  {n : ℕ} (u : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      CryptBoolean.originIndicatorInt u =
    1
    The integer Fourier transform of the origin indicator is identically one.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.integerWalshTransform_bitValueInt_eq_booleanNNFFourierCoeffInt
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (u : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (fun x => CryptBoolean.bitValueInt (f x)) u =
    CryptBoolean.booleanNNFFourierCoeffInt f u
    theorem CryptBoolean.integerWalshTransform_bitValueInt_eq_booleanNNFFourierCoeffInt
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (fun x =>
        CryptBoolean.bitValueInt (f x))
      u =
    CryptBoolean.booleanNNFFourierCoeffInt
      f u
    The integral Fourier transform of the zero-one embedding agrees with the
integral coefficient supplied by the numerical normal form.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.integerWalshTransform_halfSubspaceCombination {n : ℕ}
  (c : Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ) (u : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.halfSubspaceCombination c) u =
    2 ^ (n / 2) *
      ∑ E ∈ CryptBoolean.binaryLinearSubspaces (n / 2) n,
        c E *
          CryptBoolean.linearSubspaceIndicatorInt
            (FABL.perpendicularSubspace E) u
    theorem CryptBoolean.integerWalshTransform_halfSubspaceCombination
  {n : ℕ}
  (c :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ)
  (u : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.halfSubspaceCombination
        c)
      u =
    2 ^ (n / 2) *
      ∑
        E ∈
          CryptBoolean.binaryLinearSubspaces
            (n / 2) n,
        c E *
          CryptBoolean.linearSubspaceIndicatorInt
            (FABL.perpendicularSubspace E)
            u
    Fourier transformation sends a half-dimensional indicator combination to
the same coefficient combination on perpendicular subspaces, scaled by
`2^(n/2)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.integerWalshTransform_geometricBentExpression {n : ℕ}
  (c : Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ) (u : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.geometricBentExpression c) u =
    2 ^ (n / 2) *
        ∑ E ∈ CryptBoolean.binaryLinearSubspaces (n / 2) n,
          c E *
            CryptBoolean.linearSubspaceIndicatorInt
              (FABL.perpendicularSubspace E) u -
      2 ^ (n / 2 - 1)
    theorem CryptBoolean.integerWalshTransform_geometricBentExpression
  {n : ℕ}
  (c :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ)
  (u : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.geometricBentExpression
        c)
      u =
    2 ^ (n / 2) *
        ∑
          E ∈
            CryptBoolean.binaryLinearSubspaces
              (n / 2) n,
          c E *
            CryptBoolean.linearSubspaceIndicatorInt
              (FABL.perpendicularSubspace
                E)
              u -
      2 ^ (n / 2 - 1)
    The integral transform of Relation (51).
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.HasGeometricBentCongruence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.HasGeometricBentCongruence
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    A Boolean function satisfies Carlet Relation (51) when its integer
zero-one embedding is pointwise congruent to a geometric expression modulo
`2^(n/2)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.isBent_of_hasGeometricBentCongruence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : Even n) (hnTwo : 2 ≤ n)
  (hf : CryptBoolean.HasGeometricBentCongruence f) :
  CryptBoolean.IsBent f
    theorem CryptBoolean.isBent_of_hasGeometricBentCongruence
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Even n) (hnTwo : 2 ≤ n)
  (hf :
    CryptBoolean.HasGeometricBentCongruence
      f) :
  CryptBoolean.IsBent f
    The sufficient direction of Carlet Theorem 12: every function satisfying
the geometric congruence is bent.
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.HasExactGPSRepresentation {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (c : Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ) : Prop
    def CryptBoolean.HasExactGPSRepresentation
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (c :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n) →
      ℤ) :
  Prop
    An exact generalized partial-spread representation is Relation (51)
without reduction modulo `2^(n/2)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.isBent_and_bitValueInt_bentDual_of_exactGPSRepresentation
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (c : Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ) (hn : Even n)
  (hnTwo : 2 ≤ n) (hf : CryptBoolean.HasExactGPSRepresentation f c) :
  CryptBoolean.IsBent f ∧
    ∀ (u : FABL.F₂Cube n),
      CryptBoolean.bitValueInt (CryptBoolean.bentDual f u) =
        CryptBoolean.perpendicularGeometricBentExpression c u
    theorem CryptBoolean.isBent_and_bitValueInt_bentDual_of_exactGPSRepresentation
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (c :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n) → ℤ)
  (hn : Even n) (hnTwo : 2 ≤ n)
  (hf :
    CryptBoolean.HasExactGPSRepresentation
      f c) :
  CryptBoolean.IsBent f ∧
    ∀ (u : FABL.F₂Cube n),
      CryptBoolean.bitValueInt
          (CryptBoolean.bentDual f u) =
        CryptBoolean.perpendicularGeometricBentExpression
          c u
    Carlet Theorem 12, exact case: a generalized partial-spread
representation is bent, and its dual is obtained by replacing every subspace
with its perpendicular subspace.
  • defdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    def CryptBoolean.numericalMonomialInt {n : ℕ} (I : Finset (Fin n))
  (x : FABL.F₂Cube n) : ℤ
    def CryptBoolean.numericalMonomialInt {n : ℕ}
  (I : Finset (Fin n))
  (x : FABL.F₂Cube n) : ℤ
    The integer square-free numerical monomial indexed by a coordinate set.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.numericalMonomialInt_cast {n : ℕ} (I : Finset (Fin n))
  (x : FABL.F₂Cube n) :
  ↑(CryptBoolean.numericalMonomialInt I x) = FABL.numericalMonomial I x
    theorem CryptBoolean.numericalMonomialInt_cast
  {n : ℕ} (I : Finset (Fin n))
  (x : FABL.F₂Cube n) :
  ↑(CryptBoolean.numericalMonomialInt I
        x) =
    FABL.numericalMonomial I x
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.numericalMonomialInt_eq_sum_coordinateZeroIndicators
  {n : ℕ} (I : Finset (Fin n)) (x : FABL.F₂Cube n) :
  CryptBoolean.numericalMonomialInt I x =
    ∑ J ∈ I.powerset,
      (-1) ^ J.card *
        CryptBoolean.linearSubspaceIndicatorInt
          (FABL.F₂DecisionTree.coordinateZeroSubspace J) x
    theorem CryptBoolean.numericalMonomialInt_eq_sum_coordinateZeroIndicators
  {n : ℕ} (I : Finset (Fin n))
  (x : FABL.F₂Cube n) :
  CryptBoolean.numericalMonomialInt I x =
    ∑ J ∈ I.powerset,
      (-1) ^ J.card *
        CryptBoolean.linearSubspaceIndicatorInt
          (FABL.F₂DecisionTree.coordinateZeroSubspace
            J)
          x
    Inclusion-exclusion expresses a numerical monomial as an alternating sum
of indicators of coordinate zero subspaces.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.finrank_coordinateZeroSubspace {n : ℕ}
  (I : Finset (Fin n)) :
  Module.finrank FABL.𝔽₂
      ↥(FABL.F₂DecisionTree.coordinateZeroSubspace I) =
    n - I.card
    theorem CryptBoolean.finrank_coordinateZeroSubspace
  {n : ℕ} (I : Finset (Fin n)) :
  Module.finrank FABL.𝔽₂
      ↥(FABL.F₂DecisionTree.coordinateZeroSubspace
          I) =
    n - I.card
    The coordinate zero subspace indexed by `I` has dimension `n - |I|`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.linearSubspaceIndicatorInt_coordinateZeroSubspace_univ
  {n : ℕ} (x : FABL.F₂Cube n) :
  CryptBoolean.linearSubspaceIndicatorInt
      (FABL.F₂DecisionTree.coordinateZeroSubspace Finset.univ) x =
    CryptBoolean.originIndicatorInt x
    theorem CryptBoolean.linearSubspaceIndicatorInt_coordinateZeroSubspace_univ
  {n : ℕ} (x : FABL.F₂Cube n) :
  CryptBoolean.linearSubspaceIndicatorInt
      (FABL.F₂DecisionTree.coordinateZeroSubspace
        Finset.univ)
      x =
    CryptBoolean.originIndicatorInt x
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.bitValueInt_eq_sum_booleanNumericalCoeffInt_mul_numericalMonomialInt
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n) :
  CryptBoolean.bitValueInt (f x) =
    ∑ I,
      FABL.booleanNumericalCoeffInt f I *
        CryptBoolean.numericalMonomialInt I x
    theorem CryptBoolean.bitValueInt_eq_sum_booleanNumericalCoeffInt_mul_numericalMonomialInt
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  CryptBoolean.bitValueInt (f x) =
    ∑ I,
      FABL.booleanNumericalCoeffInt f I *
        CryptBoolean.numericalMonomialInt
          I x
    The integral numerical normal form evaluates to the zero-one embedding of
a Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.hasGeometricBentCongruence_of_isBent {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : Even n) (hnTwo : 2 ≤ n)
  (hf : CryptBoolean.IsBent f) :
  CryptBoolean.HasGeometricBentCongruence f
    theorem CryptBoolean.hasGeometricBentCongruence_of_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Even n) (hnTwo : 2 ≤ n)
  (hf : CryptBoolean.IsBent f) :
  CryptBoolean.HasGeometricBentCongruence
    f
    The necessary direction of Carlet Theorem 12.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/GeometricCharacterization.lean
    complete
    theorem CryptBoolean.isBent_iff_hasGeometricBentCongruence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : Even n) (hnTwo : 2 ≤ n) :
  CryptBoolean.IsBent f ↔ CryptBoolean.HasGeometricBentCongruence f
    theorem CryptBoolean.isBent_iff_hasGeometricBentCongruence
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Even n) (hnTwo : 2 ≤ n) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.HasGeometricBentCongruence
      f
    Carlet Theorem 12: in positive even dimension, bentness is equivalent to
the geometric congruence by half-dimensional subspace indicators.