8.2. Nonlinearity bounds
Theorem8.2.1
used by 0✓L∃∀N
Associated Lean declarations
A nonlinearity bound from algebraic immunity (Carlet, p. 136). Let n>0
and f:V_n\to\mathbb F_2. Then
\operatorname{nl}(f)\ge
\sum_{i=0}^{\operatorname{AI}(f)-2}\binom ni,
where the sum is zero when \operatorname{AI}(f)<2.
Lean code for Theorem8.2.1●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter09/NonlinearityBounds.leancomplete
theorem CryptBoolean.sum_choose_below_algebraicImmunity_sub_one_le_nonlinearity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (_hn : 0 < n) : ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - 1), n.choose i ≤ CryptBoolean.nonlinearity f
theorem CryptBoolean.sum_choose_below_algebraicImmunity_sub_one_le_nonlinearity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (_hn : 0 < n) : ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - 1), n.choose i ≤ CryptBoolean.nonlinearity f
A positive-dimensional Boolean function has nonlinearity at least the binomial sum through degree `AI(f)-2`.
Theorem8.2.2
✓L∃∀N
Associated Lean declarations
Higher-order nonlinearity from algebraic immunity (Carlet, p. 136). For
every r\in\mathbb N,
\operatorname{nl}_r(f)\ge
\sum_{i=0}^{\operatorname{AI}(f)-r-1}\binom ni,
where the sum is zero when \operatorname{AI}(f)\le r.
Lean code for Theorem8.2.2●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter09/NonlinearityBounds.leancomplete
theorem CryptBoolean.sum_choose_below_algebraicImmunity_sub_le_higherOrderNonlinearity {n : ℕ} (r : ℕ) (f : CryptBoolean.BooleanFunction n) : ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - r), n.choose i ≤ CryptBoolean.higherOrderNonlinearity r f
theorem CryptBoolean.sum_choose_below_algebraicImmunity_sub_le_higherOrderNonlinearity {n : ℕ} (r : ℕ) (f : CryptBoolean.BooleanFunction n) : ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - r), n.choose i ≤ CryptBoolean.higherOrderNonlinearity r f
The order-`r` nonlinearity is bounded below by the binomial sum strictly below `AI(f)-r`.
Theorem8.2.3
✓L∃∀N
Associated Lean declarations
Lobanov's bound (Carlet, p. 136). For every f:V_n\to\mathbb F_2,
\operatorname{nl}(f)\ge
2\sum_{i=0}^{\operatorname{AI}(f)-2}\binom{n-1}{i},
where the sum is zero when \operatorname{AI}(f)<2.
Lean code for Theorem8.2.3●3 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter09/NonlinearityBounds.leancomplete
theorem CryptBoolean.algebraicImmunity_le_firstCoordinateSlice_add_one {n : ℕ} (f : CryptBoolean.BooleanFunction (n + 1)) (b : FABL.𝔽₂) : CryptBoolean.algebraicImmunity f ≤ CryptBoolean.algebraicImmunity (CryptBoolean.firstCoordinateSlice f b) + 1
theorem CryptBoolean.algebraicImmunity_le_firstCoordinateSlice_add_one {n : ℕ} (f : CryptBoolean.BooleanFunction (n + 1)) (b : FABL.𝔽₂) : CryptBoolean.algebraicImmunity f ≤ CryptBoolean.algebraicImmunity (CryptBoolean.firstCoordinateSlice f b) + 1
Restriction to a coordinate hyperplane can lower algebraic immunity by at most one.
-
theoremdefined in CryptBoolean/Carlet/Chapter05/QuadraticNormalForm.leancomplete
theorem CryptBoolean.exists_dotProduct_normalizing_linearEquiv {r : ℕ} (a : FABL.F₂Cube r) (ha : a ≠ 0) : ∃ (hr : 0 < r), ∃ e, ∀ (x : FABL.F₂Cube r), FABL.f₂DotProduct a (e x) = x ⟨0, hr⟩
theorem CryptBoolean.exists_dotProduct_normalizing_linearEquiv {r : ℕ} (a : FABL.F₂Cube r) (ha : a ≠ 0) : ∃ (hr : 0 < r), ∃ e, ∀ (x : FABL.F₂Cube r), FABL.f₂DotProduct a (e x) = x ⟨0, hr⟩
A nonzero binary dot-product functional can be made the first coordinate by a linear change of variables.
-
theoremdefined in CryptBoolean/Carlet/Chapter09/NonlinearityBounds.leancomplete
theorem CryptBoolean.two_mul_sum_choose_below_algebraicImmunity_sub_one_le_nonlinearity {n : ℕ} (f : CryptBoolean.BooleanFunction n) : 2 * ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - 1), (n - 1).choose i ≤ CryptBoolean.nonlinearity f
theorem CryptBoolean.two_mul_sum_choose_below_algebraicImmunity_sub_one_le_nonlinearity {n : ℕ} (f : CryptBoolean.BooleanFunction n) : 2 * ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - 1), (n - 1).choose i ≤ CryptBoolean.nonlinearity f
Lobanov's bound: nonlinearity is at least twice the binomial sum through degree `AI(f)-2` in one fewer variable.
Theorem8.2.4
used by 0✓L∃∀N
Associated Lean declarations
Carlet's higher-order extension (Carlet, p. 136). Let
0<r<\operatorname{AI}(f). Then
\operatorname{nl}_r(f)\ge
2\sum_{i=0}^{\operatorname{AI}(f)-r-1}\binom{n-r}{i}.
Lean code for Theorem8.2.4●3 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter09/PrescribedDegreeAnnihilators.leancomplete
theorem CryptBoolean.annihilatorSpaceDimension_add_sum_choose_sub_degree_le {n : ℕ} (h : CryptBoolean.BooleanFunction n) (hne : h ≠ 0) (r k : ℕ) (hdegree : FABL.functionAlgebraicDegree h ≤ r) : CryptBoolean.annihilatorSpaceDimension h k + ∑ i ∈ Finset.range (k + 1), (n - r).choose i ≤ ∑ i ∈ Finset.range (k + 1), n.choose i
theorem CryptBoolean.annihilatorSpaceDimension_add_sum_choose_sub_degree_le {n : ℕ} (h : CryptBoolean.BooleanFunction n) (hne : h ≠ 0) (r k : ℕ) (hdegree : FABL.functionAlgebraicDegree h ≤ r) : CryptBoolean.annihilatorSpaceDimension h k + ∑ i ∈ Finset.range (k + 1), (n - r).choose i ≤ ∑ i ∈ Finset.range (k + 1), n.choose i
Carlet's prescribed-degree annihilator-dimension estimate, in additive form: a nonzero degree-at-most-`r` function loses at least the dimension of `R(k,n-r)` from its annihilator space.
-
theoremdefined in CryptBoolean/Carlet/Chapter09/PrescribedDegreeAnnihilators.leancomplete
theorem CryptBoolean.sum_choose_sub_degree_le_hammingWeight_mul {n : ℕ} (f h : CryptBoolean.BooleanFunction n) (hne : h ≠ 0) (r : ℕ) (hdegree : FABL.functionAlgebraicDegree h ≤ r) (hrAI : r < CryptBoolean.algebraicImmunity f) : ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - r), (n - r).choose i ≤ CryptBoolean.hammingWeight (f * h)
theorem CryptBoolean.sum_choose_sub_degree_le_hammingWeight_mul {n : ℕ} (f h : CryptBoolean.BooleanFunction n) (hne : h ≠ 0) (r : ℕ) (hdegree : FABL.functionAlgebraicDegree h ≤ r) (hrAI : r < CryptBoolean.algebraicImmunity f) : ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - r), (n - r).choose i ≤ CryptBoolean.hammingWeight (f * h)
A prescribed-degree multiplier of degree below `AI(f)` cannot make the product `f * h` lighter than the Reed–Muller dimension in the remaining coordinates.
-
theoremdefined in CryptBoolean/Carlet/Chapter09/HigherOrderAlgebraicImmunity.leancomplete
theorem CryptBoolean.two_mul_sum_choose_sub_le_higherOrderNonlinearity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (r : ℕ) (hr : 0 < r) (hrAI : r < CryptBoolean.algebraicImmunity f) : 2 * ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - r), (n - r).choose i ≤ CryptBoolean.higherOrderNonlinearity r f
theorem CryptBoolean.two_mul_sum_choose_sub_le_higherOrderNonlinearity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (r : ℕ) (hr : 0 < r) (hrAI : r < CryptBoolean.algebraicImmunity f) : 2 * ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - r), (n - r).choose i ≤ CryptBoolean.higherOrderNonlinearity r f
Carlet's higher-order algebraic-immunity bound: for positive order below `AI(f)`, the order-`r` nonlinearity is at least twice the Reed–Muller dimension in `n-r` variables below degree `AI(f)-r`.
Theorem8.2.5
used by 0✓L∃∀N
Associated Lean declarations
Mesnager's higher-order bound (Carlet, p. 136). Set
k=\operatorname{AI}(f) and let 0<r<k. Then
\operatorname{nl}_r(f)\ge
\sum_{i=0}^{k-r-1}\binom ni+
\sum_{i=\max(0,k-2r)}^{k-r-1}\binom{n-r}{i}.
Lean code for Theorem8.2.5●3 theorems
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in CryptBoolean/Carlet/Chapter09/MesnagerHigherOrder.leancomplete
theorem CryptBoolean.annihilatorSpaceDimension_le_hammingWeight_productMismatch {n : ℕ} (f g : CryptBoolean.BooleanFunction n) (s : ℕ) (hsAI : s < CryptBoolean.algebraicImmunity f) : CryptBoolean.annihilatorSpaceDimension g s ≤ CryptBoolean.hammingWeight (f * (g + 1))
theorem CryptBoolean.annihilatorSpaceDimension_le_hammingWeight_productMismatch {n : ℕ} (f g : CryptBoolean.BooleanFunction n) (s : ℕ) (hsAI : s < CryptBoolean.algebraicImmunity f) : CryptBoolean.annihilatorSpaceDimension g s ≤ CryptBoolean.hammingWeight (f * (g + 1))
The dimension of degree-at-most-`s` annihilators of `g` is bounded by the part of the distance from `f` to `g` where `f` is one.
-
theoremdefined in CryptBoolean/Carlet/Chapter09/MesnagerHigherOrder.leancomplete
theorem CryptBoolean.annihilatorSpaceDimensions_add_le_hammingWeight_add {n : ℕ} (f g : CryptBoolean.BooleanFunction n) (s : ℕ) (hsAI : s < CryptBoolean.algebraicImmunity f) : CryptBoolean.annihilatorSpaceDimension g s + CryptBoolean.annihilatorSpaceDimension (g + 1) s ≤ CryptBoolean.hammingWeight (f + g)
theorem CryptBoolean.annihilatorSpaceDimensions_add_le_hammingWeight_add {n : ℕ} (f g : CryptBoolean.BooleanFunction n) (s : ℕ) (hsAI : s < CryptBoolean.algebraicImmunity f) : CryptBoolean.annihilatorSpaceDimension g s + CryptBoolean.annihilatorSpaceDimension (g + 1) s ≤ CryptBoolean.hammingWeight (f + g)
Below `AI(f)`, the sum of the prescribed-degree annihilator dimensions of `g` and its complement is bounded by the distance from `f` to `g`.
-
theoremdefined in CryptBoolean/Carlet/Chapter09/MesnagerHigherOrder.leancomplete
theorem CryptBoolean.sum_choose_add_degreeBand_le_higherOrderNonlinearity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (r : ℕ) (_hr : 0 < r) (hrAI : r < CryptBoolean.algebraicImmunity f) : ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - r), n.choose i + ∑ i ∈ Finset.Icc (CryptBoolean.algebraicImmunity f - 2 * r) (CryptBoolean.algebraicImmunity f - r - 1), (n - r).choose i ≤ CryptBoolean.higherOrderNonlinearity r f
theorem CryptBoolean.sum_choose_add_degreeBand_le_higherOrderNonlinearity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (r : ℕ) (_hr : 0 < r) (hrAI : r < CryptBoolean.algebraicImmunity f) : ∑ i ∈ Finset.range (CryptBoolean.algebraicImmunity f - r), n.choose i + ∑ i ∈ Finset.Icc (CryptBoolean.algebraicImmunity f - 2 * r) (CryptBoolean.algebraicImmunity f - r - 1), (n - r).choose i ≤ CryptBoolean.higherOrderNonlinearity r f
Mesnager's improvement: for positive order below `AI(f)`, the order-`r` nonlinearity is bounded below by a full-cube Reed–Muller dimension plus the upper degree band in `n-r` variables.
Theorem8.2.6
uses 1used by 0✓L∃∀N
Associated Lean declarations
-
CryptBoolean.nonlinearity_lowerBound_of_even_optimalAlgebraicImmunity[complete] -
CryptBoolean.even_optimalAlgebraicImmunity_lowerBound_eq[complete] -
CryptBoolean.centralBinomial_le_nonlinearity_of_even_optimalAlgebraicImmunity[complete] -
CryptBoolean.nonlinearity_lowerBound_of_odd_optimalAlgebraicImmunity[complete]
Lobanov bounds at optimal algebraic immunity (Carlet, p. 137). Let n>0
and let f:V_n\to\mathbb F_2 have optimal algebraic immunity. If n is
even, then
\operatorname{nl}(f)\ge
2^{n-1}-2\binom{n-1}{n/2-1}
=2^{n-1}-\binom n{n/2}.
If n is odd, then
\operatorname{nl}(f)\ge
2^{n-1}-\binom{n-1}{(n-1)/2}.
Lean code for Theorem8.2.6●4 theorems
Associated Lean declarations
-
CryptBoolean.nonlinearity_lowerBound_of_even_optimalAlgebraicImmunity[complete]
-
CryptBoolean.even_optimalAlgebraicImmunity_lowerBound_eq[complete]
-
CryptBoolean.centralBinomial_le_nonlinearity_of_even_optimalAlgebraicImmunity[complete]
-
CryptBoolean.nonlinearity_lowerBound_of_odd_optimalAlgebraicImmunity[complete]
Associated Lean declarations
-
CryptBoolean.nonlinearity_lowerBound_of_even_optimalAlgebraicImmunity[complete] -
CryptBoolean.even_optimalAlgebraicImmunity_lowerBound_eq[complete] -
CryptBoolean.centralBinomial_le_nonlinearity_of_even_optimalAlgebraicImmunity[complete] -
CryptBoolean.nonlinearity_lowerBound_of_odd_optimalAlgebraicImmunity[complete]
-
theoremdefined in CryptBoolean/Carlet/Chapter09/OptimalNonlinearity.leancomplete
theorem CryptBoolean.nonlinearity_lowerBound_of_even_optimalAlgebraicImmunity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) (hneven : Even n) (hAI : CryptBoolean.algebraicImmunity f = n / 2) : 2 ^ (n - 1) - 2 * (n - 1).choose (n / 2 - 1) ≤ CryptBoolean.nonlinearity f
theorem CryptBoolean.nonlinearity_lowerBound_of_even_optimalAlgebraicImmunity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) (hneven : Even n) (hAI : CryptBoolean.algebraicImmunity f = n / 2) : 2 ^ (n - 1) - 2 * (n - 1).choose (n / 2 - 1) ≤ CryptBoolean.nonlinearity f
Lobanov's lower bound at optimal algebraic immunity in positive even dimension.
-
theoremdefined in CryptBoolean/Carlet/Chapter09/OptimalNonlinearity.leancomplete
theorem CryptBoolean.even_optimalAlgebraicImmunity_lowerBound_eq (n : ℕ) (hn : 0 < n) (hneven : Even n) : 2 ^ (n - 1) - 2 * (n - 1).choose (n / 2 - 1) = 2 ^ (n - 1) - n.choose (n / 2)
theorem CryptBoolean.even_optimalAlgebraicImmunity_lowerBound_eq (n : ℕ) (hn : 0 < n) (hneven : Even n) : 2 ^ (n - 1) - 2 * (n - 1).choose (n / 2 - 1) = 2 ^ (n - 1) - n.choose (n / 2)
The two central-binomial forms of the even optimal-immunity lower bound are equal.
-
theoremdefined in CryptBoolean/Carlet/Chapter09/OptimalNonlinearity.leancomplete
theorem CryptBoolean.centralBinomial_le_nonlinearity_of_even_optimalAlgebraicImmunity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) (hneven : Even n) (hAI : CryptBoolean.algebraicImmunity f = n / 2) : 2 ^ (n - 1) - n.choose (n / 2) ≤ CryptBoolean.nonlinearity f
theorem CryptBoolean.centralBinomial_le_nonlinearity_of_even_optimalAlgebraicImmunity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) (hneven : Even n) (hAI : CryptBoolean.algebraicImmunity f = n / 2) : 2 ^ (n - 1) - n.choose (n / 2) ≤ CryptBoolean.nonlinearity f
Lobanov's even optimal-immunity bound in its central-binomial form.
-
theoremdefined in CryptBoolean/Carlet/Chapter09/OptimalNonlinearity.leancomplete
theorem CryptBoolean.nonlinearity_lowerBound_of_odd_optimalAlgebraicImmunity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hnodd : Odd n) (hAI : CryptBoolean.algebraicImmunity f = (n + 1) / 2) : 2 ^ (n - 1) - (n - 1).choose ((n - 1) / 2) ≤ CryptBoolean.nonlinearity f
theorem CryptBoolean.nonlinearity_lowerBound_of_odd_optimalAlgebraicImmunity {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hnodd : Odd n) (hAI : CryptBoolean.algebraicImmunity f = (n + 1) / 2) : 2 ^ (n - 1) - (n - 1).choose ((n - 1) / 2) ≤ CryptBoolean.nonlinearity f
Lobanov's lower bound at optimal algebraic immunity in odd dimension.