Differential and affine-residual collision bounds for inversion #
In characteristic two, every nonzero derivative of inversion has fibres of size
at most four. The existing reciprocal ternary identity proves this directly.
Adding an arbitrary additive map and a constant therefore leaves at most
q + 4 * (q - 1) ordered collisions on a field of size q.
The differential uniformity of inversion is classical; see Claude Carlet, "Vectorial Boolean Functions for Cryptography", Section 3.1.7.
theorem
Algebraic.Aggregate.Geometry.Inversion.collisionCount_inverse_add_affine_le
{K : Type u_1}
[Field K]
[CharP K 2]
[Fintype K]
(A : K →+ K)
(a : K)
:
(Cutwidth.Aggregate.Geometry.Entropy.collisionCount fun (x : K) => x⁻¹ + A x + a) ≤ Fintype.card K + 4 * (Fintype.card K - 1)
Affine input terms do not evade inversion's ordered-collision bound.
theorem
Algebraic.Aggregate.Geometry.Inversion.collisionCount_inverse_add_affine_le_five_mul
{K : Type u_1}
[Field K]
[CharP K 2]
[Fintype K]
(A : K →+ K)
(a : K)
:
(Cutwidth.Aggregate.Geometry.Entropy.collisionCount fun (x : K) => x⁻¹ + A x + a) ≤ 5 * Fintype.card K
The coarser average collision budget of five is independent of the field size.
theorem
Algebraic.Aggregate.Geometry.Inversion.log_card_le_of_inverse_features_and_bias
{K : Type u_1}
[Field K]
[CharP K 2]
[Fintype K]
{ι : Type u_2}
[Fintype ι]
(key : K → ι → Bool)
(decode : (ι → Bool) → K)
(A : K →+ K)
(a : K)
(represents : ∀ (x : K), x⁻¹ + A x + a = decode (key x))
(biased : Finset ι)
(rare : ι → Bool)
(bias : ∀ i ∈ biased, 4 * {x : K | key x i = rare i}.card ≤ Fintype.card K)
:
Real.log ↑(Fintype.card K) ≤ Real.log 5 + ↑(Fintype.card ι) * Real.log 2 - ↑biased.card * Cutwidth.Aggregate.Geometry.Entropy.biasSaving
Any Boolean feature representation of an affine residual of inversion pays for biased bits.