5.3. Bent functions of low algebraic degrees
Theorem5.3.1
✓L∃∀N
Associated Lean declarations
Quadratic bent functions (Carlet, Section 6.2, pp. 80--81). Let n\ge2
be even and let f:V_n\to\mathbb F_2 have algebraic degree at most two. The
following conditions are equivalent:
-
fis bent; -
w_H(f)=2^{n-1}\pm2^{n/2-1}; -
the alternating polar form
\phi_f(x,y)=f(0)+f(x)+f(y)+f(x+y)is nondegenerate, equivalently the linear kernel offis\{0\}; -
the symmetric zero-diagonal coefficient matrix of the quadratic part of
fis nonsingular; -
after an invertible affine change of variables,
fhas the formx_1x_2+x_3x_4+\cdots+x_{n-1}x_n+\varepsilon \qquad(\varepsilon\in\mathbb F_2).
Lean code for Theorem5.3.1●2 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter06/QuadraticBent.leancomplete
theorem CryptBoolean.isBent_iff_quadraticRadical_eq_bot {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hdegree : FABL.functionAlgebraicDegree f ≤ 2) : CryptBoolean.IsBent f ↔ CryptBoolean.quadraticRadical f hdegree = ⊥
theorem CryptBoolean.isBent_iff_quadraticRadical_eq_bot {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hdegree : FABL.functionAlgebraicDegree f ≤ 2) : CryptBoolean.IsBent f ↔ CryptBoolean.quadraticRadical f hdegree = ⊥
A quadratic Boolean function is bent exactly when the radical of its polar form is trivial.
-
theoremdefined in CryptBoolean/Carlet/Chapter06/QuadraticBent.leancomplete
theorem CryptBoolean.isBent_iff_linearKernel_eq_bot_of_degree_le_two {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hdegree : FABL.functionAlgebraicDegree f ≤ 2) : CryptBoolean.IsBent f ↔ CryptBoolean.linearKernel f = ⊥
theorem CryptBoolean.isBent_iff_linearKernel_eq_bot_of_degree_le_two {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hdegree : FABL.functionAlgebraicDegree f ≤ 2) : CryptBoolean.IsBent f ↔ CryptBoolean.linearKernel f = ⊥
A quadratic Boolean function is bent exactly when its linear kernel is trivial.