Cryptographic Boolean Functions in Lean

5.14. Normal and non-normal bent functions🔗

Definition5.14.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 1
Used by 5
Reverse dependency previews
Preview
Theorem 5.14.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6definition-8normal-extensionpages-107-108fidelity-exact-coordinate-invariant-form

Normal extension (Carlet, Definition 8, pp. 107--108). Let \beta:V_k\to\mathbb F_2 and f:V_n\to\mathbb F_2 be bent. Write \beta\preccurlyeq f when there are a nonnegative integer m and a linear isomorphism L:V_k\times V_m\times V_m\longrightarrow V_n such that f\bigl(L(u,w,0)\bigr)=\beta(u) \qquad(u\in V_k,\ w\in V_m). Equivalently, V_n=U\oplus W_1\oplus W_2 with \dim W_1=\dim W_2, and the restriction of f to U\oplus W_1 is \beta pulled back from U. Every bent function is a normal extension of itself.

Lean code for Definition5.14.1●4 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    def CryptBoolean.IsNormalExtension {k n : ℕ}
  (β : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.IsNormalExtension {k n : ℕ}
  (β : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    Carlet Definition 8, expressed invariantly under a linear choice of
coordinates for the decomposition `V = U ⊕ W₁ ⊕ W₂`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.IsNormalExtension.isBent_left {k n : ℕ}
  {β : CryptBoolean.BooleanFunction k}
  {f : CryptBoolean.BooleanFunction n}
  (h : CryptBoolean.IsNormalExtension β f) : CryptBoolean.IsBent β
    theorem CryptBoolean.IsNormalExtension.isBent_left
  {k n : ℕ}
  {β : CryptBoolean.BooleanFunction k}
  {f : CryptBoolean.BooleanFunction n}
  (h :
    CryptBoolean.IsNormalExtension β f) :
  CryptBoolean.IsBent β
    A normal extension includes bentness of its smaller function.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.IsNormalExtension.isBent_right {k n : ℕ}
  {β : CryptBoolean.BooleanFunction k}
  {f : CryptBoolean.BooleanFunction n}
  (h : CryptBoolean.IsNormalExtension β f) : CryptBoolean.IsBent f
    theorem CryptBoolean.IsNormalExtension.isBent_right
  {k n : ℕ}
  {β : CryptBoolean.BooleanFunction k}
  {f : CryptBoolean.BooleanFunction n}
  (h :
    CryptBoolean.IsNormalExtension β f) :
  CryptBoolean.IsBent f
    A normal extension includes bentness of its larger function.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.isNormalExtension_refl {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f) :
  CryptBoolean.IsNormalExtension f f
    theorem CryptBoolean.isNormalExtension_refl
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) :
  CryptBoolean.IsNormalExtension f f
    Every bent function is a zero-codimension normal extension of itself.
Theorem5.14.2
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 5.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6normal-extensiondualitytransitivitypage-108fidelity-exact

Composition and duality of normal extensions (Carlet, p. 108). The relation \preccurlyeq is transitive. Moreover, if \beta\preccurlyeq f, then \widetilde\beta\preccurlyeq\widetilde f. In standard coordinates, duality exchanges the two equal complementary summands.

Lean code for Theorem5.14.2●6 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    def CryptBoolean.walshAdjointLinearEquiv {r s : ℕ}
  (L : FABL.F₂Cube r ≃ₗ[FABL.𝔽₂] FABL.F₂Cube s) :
  FABL.F₂Cube s ≃ₗ[FABL.𝔽₂] FABL.F₂Cube r
    def CryptBoolean.walshAdjointLinearEquiv
  {r s : ℕ}
  (L :
    FABL.F₂Cube r ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube s) :
  FABL.F₂Cube s ≃ₗ[FABL.𝔽₂] FABL.F₂Cube r
    The adjoint of a cube linear equivalence for the standard binary dot
pairings.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.walshTransform_comp_linearEquiv {r s : ℕ}
  (f : CryptBoolean.BooleanFunction s)
  (L : FABL.F₂Cube r ≃ₗ[FABL.𝔽₂] FABL.F₂Cube s) (a : FABL.F₂Cube r) :
  CryptBoolean.walshTransform (f ∘ ⇑L) a =
    CryptBoolean.walshTransform f
      ((CryptBoolean.walshAdjointLinearEquiv L.symm) a)
    theorem CryptBoolean.walshTransform_comp_linearEquiv
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction s)
  (L :
    FABL.F₂Cube r ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube s)
  (a : FABL.F₂Cube r) :
  CryptBoolean.walshTransform (f ∘ ⇑L) a =
    CryptBoolean.walshTransform f
      ((CryptBoolean.walshAdjointLinearEquiv
          L.symm)
        a)
    A linear change of input coordinates transports Walsh frequencies by
the inverse adjoint map.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.bentDual_comp_linearEquiv {r s : ℕ}
  (f : CryptBoolean.BooleanFunction s)
  (L : FABL.F₂Cube r ≃ₗ[FABL.𝔽₂] FABL.F₂Cube s) (a : FABL.F₂Cube r) :
  CryptBoolean.bentDual (f ∘ ⇑L) a =
    CryptBoolean.bentDual f
      ((CryptBoolean.walshAdjointLinearEquiv L.symm) a)
    theorem CryptBoolean.bentDual_comp_linearEquiv
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction s)
  (L :
    FABL.F₂Cube r ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube s)
  (a : FABL.F₂Cube r) :
  CryptBoolean.bentDual (f ∘ ⇑L) a =
    CryptBoolean.bentDual f
      ((CryptBoolean.walshAdjointLinearEquiv
          L.symm)
        a)
    Bent duals transform contragrediently under a linear change of input
coordinates.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.bentDual_canonical_normalExtension {k r : ℕ}
  (β : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction (k + (r + r)))
  (hβ : CryptBoolean.IsBent β) (hf : CryptBoolean.IsBent f)
  (hrestriction :
    ∀ (u : Fin k → FABL.𝔽₂) (w : Fin r → FABL.𝔽₂),
      f (Fin.append u (Fin.append w 0)) = β u)
  (a : FABL.F₂Cube k) (z : FABL.F₂Cube r) :
  CryptBoolean.bentDual f (Fin.append a (Fin.append 0 z)) =
    CryptBoolean.bentDual β a
    theorem CryptBoolean.bentDual_canonical_normalExtension
  {k r : ℕ}
  (β : CryptBoolean.BooleanFunction k)
  (f :
    CryptBoolean.BooleanFunction
      (k + (r + r)))
  (hβ : CryptBoolean.IsBent β)
  (hf : CryptBoolean.IsBent f)
  (hrestriction :
    ∀ (u : Fin k → FABL.𝔽₂)
      (w : Fin r → FABL.𝔽₂),
      f (Fin.append u (Fin.append w 0)) =
        β u)
  (a : FABL.F₂Cube k)
  (z : FABL.F₂Cube r) :
  CryptBoolean.bentDual f
      (Fin.append a (Fin.append 0 z)) =
    CryptBoolean.bentDual β a
    In standard extension coordinates, duality exchanges the two equal
complementary blocks.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.IsNormalExtension.trans {k n p : ℕ}
  {β : CryptBoolean.BooleanFunction k}
  {f : CryptBoolean.BooleanFunction n}
  {g : CryptBoolean.BooleanFunction p}
  (hβf : CryptBoolean.IsNormalExtension β f)
  (hfg : CryptBoolean.IsNormalExtension f g) :
  CryptBoolean.IsNormalExtension β g
    theorem CryptBoolean.IsNormalExtension.trans
  {k n p : ℕ}
  {β : CryptBoolean.BooleanFunction k}
  {f : CryptBoolean.BooleanFunction n}
  {g : CryptBoolean.BooleanFunction p}
  (hβf :
    CryptBoolean.IsNormalExtension β f)
  (hfg :
    CryptBoolean.IsNormalExtension f g) :
  CryptBoolean.IsNormalExtension β g
    Carlet's normal-extension relation is transitive.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.IsNormalExtension.bentDual {k n : ℕ}
  {β : CryptBoolean.BooleanFunction k}
  {f : CryptBoolean.BooleanFunction n}
  (h : CryptBoolean.IsNormalExtension β f) :
  CryptBoolean.IsNormalExtension (CryptBoolean.bentDual β)
    (CryptBoolean.bentDual f)
    theorem CryptBoolean.IsNormalExtension.bentDual
  {k n : ℕ}
  {β : CryptBoolean.BooleanFunction k}
  {f : CryptBoolean.BooleanFunction n}
  (h :
    CryptBoolean.IsNormalExtension β f) :
  CryptBoolean.IsNormalExtension
    (CryptBoolean.bentDual β)
    (CryptBoolean.bentDual f)
    Normal extension is preserved by bent duality; the two complementary
directions are exchanged by the dual coordinate decomposition.
Theorem5.14.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 3
Statement dependency previews
Preview
Theorem 1.4.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Proposition 5.14.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6normalityzero-dimensional-extensionpage-108fidelity-source-correction

Zero-dimensional normal extensions (Carlet, p. 108; corrected normality convention). Let f:V_n\to\mathbb F_2 be bent. If normality means that f is constant on an n/2-dimensional linear subspace, then f\text{ is normal} \quad\Longleftrightarrow\quad \varepsilon\preccurlyeq f \text{ for some }\varepsilon\in\mathbb F_2. For the affine-flat convention of Definition 4, the exact statement is instead f\text{ is }(n/2)\text{-normal} \quad\Longleftrightarrow\quad \varepsilon\preccurlyeq(f\circ A) for some \varepsilon\in\mathbb F_2 and some affine automorphism A of V_n.

The affine automorphism cannot in general be omitted. The two-variable function f(x_1,x_2)=(x_1+1)(x_2+1) is bent and constant on a one-dimensional affine flat, but it is not constant on any one-dimensional linear subspace.

Lean code for Theorem5.14.3●9 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    def CryptBoolean.zeroDimensionalBooleanFunction (ε : FABL.𝔽₂) :
  CryptBoolean.BooleanFunction 0
    def CryptBoolean.zeroDimensionalBooleanFunction
  (ε : FABL.𝔽₂) :
  CryptBoolean.BooleanFunction 0
    The Boolean function on the zero-dimensional cube with value `ε`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.zeroDimensionalBooleanFunction_apply (ε : FABL.𝔽₂)
  (x : FABL.F₂Cube 0) :
  CryptBoolean.zeroDimensionalBooleanFunction ε x = ε
    theorem CryptBoolean.zeroDimensionalBooleanFunction_apply
  (ε : FABL.𝔽₂) (x : FABL.F₂Cube 0) :
  CryptBoolean.zeroDimensionalBooleanFunction
      ε x =
    ε
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.isBent_zeroDimensionalBooleanFunction (ε : FABL.𝔽₂) :
  CryptBoolean.IsBent (CryptBoolean.zeroDimensionalBooleanFunction ε)
    theorem CryptBoolean.isBent_zeroDimensionalBooleanFunction
  (ε : FABL.𝔽₂) :
  CryptBoolean.IsBent
    (CryptBoolean.zeroDimensionalBooleanFunction
      ε)
    Every Boolean function on the zero-dimensional cube is bent.
  • defdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    def CryptBoolean.IsSubspaceNormal {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.IsSubspaceNormal {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    The linear-subspace convention for normality used in Carlet Section 6.9:
`f` is constant on a subspace of half the ambient dimension.
  • defdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    def CryptBoolean.IsAffineNormalExtension {k n : ℕ}
  (β : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.IsAffineNormalExtension
  {k n : ℕ}
  (β : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    The affine-input closure of normal extension.  It retains Definition 8
after choosing an affinely equivalent representative of the ambient bent
function.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.isKNormal_comp_affineEquiv_iff {k n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (A : FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂] FABL.F₂Cube n) :
  CryptBoolean.IsKNormal (f ∘ ⇑A) k ↔ CryptBoolean.IsKNormal f k
    theorem CryptBoolean.isKNormal_comp_affineEquiv_iff
  {k n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (A :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.IsKNormal (f ∘ ⇑A) k ↔
    CryptBoolean.IsKNormal f k
    Normality on affine flats is invariant under an affine change of input
coordinates.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.exists_isNormalExtension_zeroDimensional_iff_isSubspaceNormal
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) :
  (∃ ε,
      CryptBoolean.IsNormalExtension
        (CryptBoolean.zeroDimensionalBooleanFunction ε) f) ↔
    CryptBoolean.IsSubspaceNormal f
    theorem CryptBoolean.exists_isNormalExtension_zeroDimensional_iff_isSubspaceNormal
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) :
  (∃ ε,
      CryptBoolean.IsNormalExtension
        (CryptBoolean.zeroDimensionalBooleanFunction
          ε)
        f) ↔
    CryptBoolean.IsSubspaceNormal f
    Under the linear-subspace convention of Section 6.9, a bent function is
normal exactly when a zero-dimensional constant bent function normally
extends to it.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.exists_isAffineNormalExtension_zeroDimensional_iff_isKNormal
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) :
  (∃ ε,
      CryptBoolean.IsAffineNormalExtension
        (CryptBoolean.zeroDimensionalBooleanFunction ε) f) ↔
    CryptBoolean.IsKNormal f (n / 2)
    theorem CryptBoolean.exists_isAffineNormalExtension_zeroDimensional_iff_isKNormal
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) :
  (∃ ε,
      CryptBoolean.IsAffineNormalExtension
        (CryptBoolean.zeroDimensionalBooleanFunction
          ε)
        f) ↔
    CryptBoolean.IsKNormal f (n / 2)
    With Chapter 5's affine-flat definition of normality, the
zero-dimensional characterization of Section 6.9 holds after taking the
affine-input closure of the normal-extension relation.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.exists_isKNormal_not_isNormalExtension_zeroDimensional :
  ∃ f,
    CryptBoolean.IsBent f ∧
      CryptBoolean.IsKNormal f 1 ∧
        ¬∃ ε,
            CryptBoolean.IsNormalExtension
              (CryptBoolean.zeroDimensionalBooleanFunction ε) f
    theorem CryptBoolean.exists_isKNormal_not_isNormalExtension_zeroDimensional :
  ∃ f,
    CryptBoolean.IsBent f ∧
      CryptBoolean.IsKNormal f 1 ∧
        ¬∃ ε,
            CryptBoolean.IsNormalExtension
              (CryptBoolean.zeroDimensionalBooleanFunction
                ε)
              f
    Chapter 5 affine-flat normality does not imply the unclosed statement
`ε ⊑ f`: a translated two-variable quadratic bent function is normal only
on affine lines and on no one-dimensional linear subspace.
Proposition5.14.4
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Corollary 4.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6proposition-29normalitydirect-sumpage-108fidelity-exact-linear-subspace-convention

Proposition 29 (Carlet, p. 108). Let f_i:V_i\to\mathbb F_2 be bent for i=1,2. The direct sum f_1\oplus f_2 is normal if and only if there are bent functions \beta_i such that \beta_i\preccurlyeq f_i for i=1,2 and either \beta_1 is linearly equivalent to \beta_2, or \beta_1 is linearly equivalent to \beta_2+1.

Lean code for Proposition5.14.4●2 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    def CryptBoolean.AreLinearlyEquivalentOrComplementary {m n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (g : CryptBoolean.BooleanFunction m) : Prop
    def CryptBoolean.AreLinearlyEquivalentOrComplementary
  {m n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (g : CryptBoolean.BooleanFunction m) :
  Prop
    Linear equivalence up to addition of a constant Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.isSubspaceNormal_booleanDirectSum_iff {m n : ℕ}
  {f₁ : CryptBoolean.BooleanFunction n}
  {f₂ : CryptBoolean.BooleanFunction m} (hf₁ : CryptBoolean.IsBent f₁)
  (hf₂ : CryptBoolean.IsBent f₂) :
  CryptBoolean.IsSubspaceNormal (CryptBoolean.booleanDirectSum f₁ f₂) ↔
    ∃ k₁ k₂ beta₁ beta₂,
      CryptBoolean.IsNormalExtension beta₁ f₁ ∧
        CryptBoolean.IsNormalExtension beta₂ f₂ ∧
          CryptBoolean.AreLinearlyEquivalentOrComplementary beta₁ beta₂
    theorem CryptBoolean.isSubspaceNormal_booleanDirectSum_iff
  {m n : ℕ}
  {f₁ : CryptBoolean.BooleanFunction n}
  {f₂ : CryptBoolean.BooleanFunction m}
  (hf₁ : CryptBoolean.IsBent f₁)
  (hf₂ : CryptBoolean.IsBent f₂) :
  CryptBoolean.IsSubspaceNormal
      (CryptBoolean.booleanDirectSum f₁
        f₂) ↔
    ∃ k₁ k₂ beta₁ beta₂,
      CryptBoolean.IsNormalExtension beta₁
          f₁ ∧
        CryptBoolean.IsNormalExtension
            beta₂ f₂ ∧
          CryptBoolean.AreLinearlyEquivalentOrComplementary
            beta₁ beta₂
    Carlet Proposition 29: a direct sum of bent functions is normal on a
linear subspace exactly when there are linearly equivalent or complementary
normal extensions of its summands.
Proposition5.14.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 4
Statement dependency previews
Preview
Corollary 4.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6proposition-30normalitynormal-extensionpage-108fidelity-exact-linear-subspace-convention

Proposition 30 (Carlet, p. 108). If \beta\preccurlyeq f and the bent function f is normal, then the bent function \beta is normal.

Lean code for Proposition5.14.5●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.isSubspaceNormal_comp_linearEquiv_iff {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L : FABL.F₂Cube n ≃ₗ[FABL.𝔽₂] FABL.F₂Cube n) :
  CryptBoolean.IsSubspaceNormal (f ∘ ⇑L) ↔
    CryptBoolean.IsSubspaceNormal f
    theorem CryptBoolean.isSubspaceNormal_comp_linearEquiv_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.IsSubspaceNormal (f ∘ ⇑L) ↔
    CryptBoolean.IsSubspaceNormal f
    Linear changes of input coordinates preserve the linear-subspace
normality convention of Section 6.9.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.IsNormalExtension.isSubspaceNormal_left {k n : ℕ}
  {beta : CryptBoolean.BooleanFunction k}
  {f : CryptBoolean.BooleanFunction n}
  (hextension : CryptBoolean.IsNormalExtension beta f)
  (hnormal : CryptBoolean.IsSubspaceNormal f) :
  CryptBoolean.IsSubspaceNormal beta
    theorem CryptBoolean.IsNormalExtension.isSubspaceNormal_left
  {k n : ℕ}
  {beta : CryptBoolean.BooleanFunction k}
  {f : CryptBoolean.BooleanFunction n}
  (hextension :
    CryptBoolean.IsNormalExtension beta f)
  (hnormal :
    CryptBoolean.IsSubspaceNormal f) :
  CryptBoolean.IsSubspaceNormal beta
    Carlet Proposition 30: linear-subspace normality descends along a
normal extension.
Proposition5.14.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 3
Statement dependency previews
Preview
Theorem 5.2.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6proposition-31normal-extensionreplacementpage-108fidelity-exact-coordinate-invariant-form

Proposition 31 (Carlet, p. 108). Let \beta be bent on U, let f be bent on U\times W\times W, and suppose \beta\preccurlyeq f through f(x,y,0)=\beta(x). For any bent \beta':U\to\mathbb F_2, define f'(x,y,z)= \begin{cases} \beta'(x),&z=0,\\ f(x,y,z),&z\ne0. \end{cases} Then f' is bent and \beta'\preccurlyeq f'.

Lean code for Proposition5.14.6●6 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    def CryptBoolean.canonicalNormalExtensionReplacement {k r : ℕ}
  (β' : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction (k + (r + r))) :
  CryptBoolean.BooleanFunction (k + (r + r))
    def CryptBoolean.canonicalNormalExtensionReplacement
  {k r : ℕ}
  (β' : CryptBoolean.BooleanFunction k)
  (f :
    CryptBoolean.BooleanFunction
      (k + (r + r))) :
  CryptBoolean.BooleanFunction
    (k + (r + r))
    Replace the restriction on the distinguished `W₂ = 0` flat in
standard normal-extension coordinates.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.canonicalNormalExtensionReplacement_apply_append {k r : ℕ}
  (β' : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction (k + (r + r))) (u : FABL.F₂Cube k)
  (w z : FABL.F₂Cube r) :
  CryptBoolean.canonicalNormalExtensionReplacement β' f
      (Fin.append u (Fin.append w z)) =
    if z = 0 then β' u else f (Fin.append u (Fin.append w z))
    theorem CryptBoolean.canonicalNormalExtensionReplacement_apply_append
  {k r : ℕ}
  (β' : CryptBoolean.BooleanFunction k)
  (f :
    CryptBoolean.BooleanFunction
      (k + (r + r)))
  (u : FABL.F₂Cube k)
  (w z : FABL.F₂Cube r) :
  CryptBoolean.canonicalNormalExtensionReplacement
      β' f
      (Fin.append u (Fin.append w z)) =
    if z = 0 then β' u
    else f (Fin.append u (Fin.append w z))
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.isBent_canonicalNormalExtensionReplacement {k r : ℕ}
  (β β' : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction (k + (r + r)))
  (hβ : CryptBoolean.IsBent β) (hβ' : CryptBoolean.IsBent β')
  (hf : CryptBoolean.IsBent f)
  (hrestriction :
    ∀ (u : Fin k → FABL.𝔽₂) (w : Fin r → FABL.𝔽₂),
      f (Fin.append u (Fin.append w 0)) = β u) :
  CryptBoolean.IsBent
    (CryptBoolean.canonicalNormalExtensionReplacement β' f)
    theorem CryptBoolean.isBent_canonicalNormalExtensionReplacement
  {k r : ℕ}
  (β β' : CryptBoolean.BooleanFunction k)
  (f :
    CryptBoolean.BooleanFunction
      (k + (r + r)))
  (hβ : CryptBoolean.IsBent β)
  (hβ' : CryptBoolean.IsBent β')
  (hf : CryptBoolean.IsBent f)
  (hrestriction :
    ∀ (u : Fin k → FABL.𝔽₂)
      (w : Fin r → FABL.𝔽₂),
      f (Fin.append u (Fin.append w 0)) =
        β u) :
  CryptBoolean.IsBent
    (CryptBoolean.canonicalNormalExtensionReplacement
      β' f)
    Carlet Proposition 31 in standard decomposition coordinates: replacing
the smaller bent restriction preserves bentness.
  • defdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    def CryptBoolean.normalExtensionReplacement {k n r : ℕ}
  (β' : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction n)
  (L : FABL.F₂Cube (k + (r + r)) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction n
    def CryptBoolean.normalExtensionReplacement
  {k n r : ℕ}
  (β' : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube (k + (r + r)) ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction n
    Replace the distinguished restriction of a normal extension after
transporting to the coordinates of its direct-sum decomposition.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.normalExtensionReplacement_apply {k n r : ℕ}
  (β' : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction n)
  (L : FABL.F₂Cube (k + (r + r)) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube n)
  (u : FABL.F₂Cube k) (w : FABL.F₂Cube r) :
  CryptBoolean.normalExtensionReplacement β' f L
      (L (Fin.append u (Fin.append w 0))) =
    β' u
    theorem CryptBoolean.normalExtensionReplacement_apply
  {k n r : ℕ}
  (β' : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube (k + (r + r)) ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube n)
  (u : FABL.F₂Cube k)
  (w : FABL.F₂Cube r) :
  CryptBoolean.normalExtensionReplacement
      β' f L
      (L
        (Fin.append u (Fin.append w 0))) =
    β' u
  • theoremdefined in CryptBoolean/Carlet/Chapter06/NormalExtension.lean
    complete
    theorem CryptBoolean.normalExtensionReplacement_isNormalExtension {k n r : ℕ}
  (β β' : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction n) (hβ : CryptBoolean.IsBent β)
  (hβ' : CryptBoolean.IsBent β') (hf : CryptBoolean.IsBent f)
  (L : FABL.F₂Cube (k + (r + r)) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube n)
  (hrestriction :
    ∀ (u : Fin k → FABL.𝔽₂) (w : Fin r → FABL.𝔽₂),
      f (L (Fin.append u (Fin.append w 0))) = β u) :
  CryptBoolean.IsNormalExtension β'
    (CryptBoolean.normalExtensionReplacement β' f L)
    theorem CryptBoolean.normalExtensionReplacement_isNormalExtension
  {k n r : ℕ}
  (β β' : CryptBoolean.BooleanFunction k)
  (f : CryptBoolean.BooleanFunction n)
  (hβ : CryptBoolean.IsBent β)
  (hβ' : CryptBoolean.IsBent β')
  (hf : CryptBoolean.IsBent f)
  (L :
    FABL.F₂Cube (k + (r + r)) ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube n)
  (hrestriction :
    ∀ (u : Fin k → FABL.𝔽₂)
      (w : Fin r → FABL.𝔽₂),
      f
          (L
            (Fin.append u
              (Fin.append w 0))) =
        β u) :
  CryptBoolean.IsNormalExtension β'
    (CryptBoolean.normalExtensionReplacement
      β' f L)
    Carlet Proposition 31: the restriction of a normal extension can be
replaced by any bent function on the smaller space.