5.4. Bound on algebraic degree
Proposition 18: Rothaus' bound (Carlet, p. 83). Let n\ge4 be even.
Every bent function f:V_n\to\mathbb F_2 satisfies
\deg_{\mathrm{alg}}(f)\le n/2,
\qquad
\deg_{\mathrm{alg}}(\widetilde f)\le n/2.
In dimension n=2, every bent function, and hence its dual, has algebraic
degree exactly two.
Lean code for Proposition5.4.1●2 theorems
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter06/DegreeBounds.leancomplete
theorem CryptBoolean.functionAlgebraicDegree_le_half_of_isBent {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f) (hn : 4 ≤ n) : FABL.functionAlgebraicDegree f ≤ n / 2
theorem CryptBoolean.functionAlgebraicDegree_le_half_of_isBent {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f) (hn : 4 ≤ n) : FABL.functionAlgebraicDegree f ≤ n / 2
Carlet Proposition 18: in even dimension at least four, the algebraic degree of a bent Boolean function is at most half the dimension.
-
theoremdefined in CryptBoolean/Carlet/Chapter06/DegreeBounds.leancomplete
theorem CryptBoolean.functionAlgebraicDegree_eq_two_of_isBent (f : CryptBoolean.BooleanFunction 2) (hf : CryptBoolean.IsBent f) : FABL.functionAlgebraicDegree f = 2
theorem CryptBoolean.functionAlgebraicDegree_eq_two_of_isBent (f : CryptBoolean.BooleanFunction 2) (hf : CryptBoolean.IsBent f) : FABL.functionAlgebraicDegree f = 2
Every two-variable bent Boolean function has algebraic degree two.
Proposition 19 (Carlet, Relation (47), p. 83). Let n\ge2 be even, let
f:V_n\to\mathbb F_2 be bent, and put
d=\deg_{\mathrm{alg}}(f),
\qquad
\widetilde d=\deg_{\mathrm{alg}}(\widetilde f).
Then
\frac n2-d
\ge
\frac{\frac n2-\widetilde d}{\widetilde d-1}.
Lean code for Proposition5.4.2●2 theorems
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter06/McElieceAx.leancomplete
theorem CryptBoolean.two_pow_ceilDiv_dvd_booleanCharacterSum_of_degree_le {n : ℕ} (f : CryptBoolean.BooleanFunction n) (d : ℕ) (hd : 0 < d) (hdegree : FABL.functionAlgebraicDegree f ≤ d) : 2 ^ (n ⌈/⌉ d) ∣ ∑ x, CryptBoolean.bitSignInt (f x)
theorem CryptBoolean.two_pow_ceilDiv_dvd_booleanCharacterSum_of_degree_le {n : ℕ} (f : CryptBoolean.BooleanFunction n) (d : ℕ) (hd : 0 < d) (hdegree : FABL.functionAlgebraicDegree f ≤ d) : 2 ^ (n ⌈/⌉ d) ∣ ∑ x, CryptBoolean.bitSignInt (f x)
The McEliece--Ax divisibility exponent for a positive-degree Boolean function: its zero-frequency character sum is divisible by `2 ^ ⌈n / d⌉` whenever its algebraic degree is at most `d`.
-
theoremdefined in CryptBoolean/Carlet/Chapter06/DegreeRelation.leancomplete
theorem CryptBoolean.bentDual_functionAlgebraicDegree_relation {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f) (hn : 2 ≤ n) : ↑n / 2 - ↑(FABL.functionAlgebraicDegree f) ≥ (↑n / 2 - ↑(FABL.functionAlgebraicDegree (CryptBoolean.bentDual f))) / (↑(FABL.functionAlgebraicDegree (CryptBoolean.bentDual f)) - 1)
theorem CryptBoolean.bentDual_functionAlgebraicDegree_relation {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hf : CryptBoolean.IsBent f) (hn : 2 ≤ n) : ↑n / 2 - ↑(FABL.functionAlgebraicDegree f) ≥ (↑n / 2 - ↑(FABL.functionAlgebraicDegree (CryptBoolean.bentDual f))) / (↑(FABL.functionAlgebraicDegree (CryptBoolean.bentDual f)) - 1)
Carlet Proposition 19, Relation (47): if `f` is bent in positive even dimension, then the algebraic degrees of `f` and its dual satisfy `n / 2 - deg(f) ≥ (n / 2 - deg(f̃)) / (deg(f̃) - 1)`.
For a degree-d ANF monomial x^I of f, take
E=\{u\in V_n:u_i=0\text{ for every }i\in I\}. Relation (46) gives
\sum_{u\in E}(-1)^{\widetilde f(u)}
=2^{n/2-d}\sum_{x\in E^\perp}(-1)^{f(x)}.
The rightmost sum is divisible by two but not by four. The McEliece--Ax
divisibility theorem supplies the comparison exponent
\lceil(n-d)/\widetilde d\rceil; comparing the two powers of two yields
Relation (47).