Affine restrictions of the Gold map in characteristic two

In characteristic two, (a + b + c)³ differs from a³ + b³ + c³ by the product of the three pairwise sums. Hence cubing preserves ternary addition only on sets of at most two points (it is almost perfect nonlinear), and a linear component ℓ(x³) is affine on a coset of U exactly when U is totally isotropic for the alternating form B(u, w) = ℓ(u²w + uw²). When cubing is injective, this form has at most one nonzero radical vector, so its totally isotropic subspaces have dimension at most (dim K + 1) / 2.

The Gold map x ↦ x^(2^k+1) and its almost perfect nonlinearity are classical; see Robert Gold, "Maximal recursive sequences with 3-valued recursive cross-correlation functions", IEEE Transactions on Information Theory 14 (1968), 154–156, and Claude Carlet, "Vectorial Boolean Functions for Cryptography", Section 3.1.

theorem Algebraic.Aggregate.Geometry.Gold.cube_add_add {K : Type u_1} [Field K] [CharP K 2] (a b c : K) : (a + b + c) ^ 3 = a ^ 3 + b ^ 3 + c ^ 3 + (a + b) * (b + c) * (c + a)

The cube of a ternary sum differs from the sum of cubes by the product of the three pairwise sums.

theorem Algebraic.Aggregate.Geometry.Gold.card_le_two_of_cube_affine {K : Type u_1} [Field K] [CharP K 2] (S : Finset K) (affine : ∀ a ∈ S, ∀ b ∈ S, ∀ c ∈ S, (a + b + c) ^ 3 = a ^ 3 + b ^ 3 + c ^ 3) : S.card ≤ 2

Cubing preserves ternary addition on at most two points of a binary field.

theorem Algebraic.Aggregate.Geometry.Gold.map_product_eq_zero_of_cube_affine {K : Type u_1} [Field K] [CharP K 2] (ℓ : K →+ ZMod 2) {a b c : K} (affine : ℓ ((a + b + c) ^ 3) = ℓ (a ^ 3) + ℓ (b ^ 3) + ℓ (c ^ 3)) : ℓ ((a + b) * (b + c) * (c + a)) = 0

A linear component of cubing is affine on three points exactly when it vanishes on the product of their pairwise sums.

theorem Algebraic.Aggregate.Geometry.Gold.cube_injective {K : Type u_1} [Field K] [Fintype K] (coprime : Nat.Coprime 3 (Fintype.card K - 1)) : Function.Injective fun (x : K) => x ^ 3

Cubing is injective when three is coprime to the multiplicative group order.

theorem Algebraic.Aggregate.Geometry.Gold.map_eq_map_sq_div_of_radical {K : Type u_1} [Field K] (ℓ : K →+ ZMod 2) {u : K} (hu : u ≠ 0) (radical : ∀ (w : K), ℓ (u ^ 2 * w + u * w ^ 2) = 0) (r : K) : ℓ r = ℓ (r ^ 2 / u ^ 3)

A nonzero radical vector u of the polar form identifies ℓ r with ℓ (r² / u³).

theorem Algebraic.Aggregate.Geometry.Gold.eq_of_radical {K : Type u_1} [Field K] [CharP K 2] [Finite K] (ℓ : K →+ ZMod 2) (nonzero : ℓ ≠ 0) (cube : Function.Injective fun (x : K) => x ^ 3) {u v : K} (hu : u ≠ 0) (hv : v ≠ 0) (ru : ∀ (w : K), ℓ (u ^ 2 * w + u * w ^ 2) = 0) (rv : ∀ (w : K), ℓ (v ^ 2 * w + v * w ^ 2) = 0) : u = v

When cubing is injective, the polar form of a nonzero component has at most one nonzero radical vector.

theorem Algebraic.Aggregate.Geometry.Gold.coprime_three_two_pow_sub_one {n : ℕ} (odd : Odd n) : Nat.Coprime 3 (2 ^ n - 1)

In odd dimension, three is coprime to the order 2^n - 1 of the multiplicative group.

noncomputable def Algebraic.Aggregate.Geometry.Gold.polarForm {K : Type u_1} [Field K] [Algebra (ZMod 2) K] [CharP K 2] (ℓ : K →ₗ[ZMod 2] ZMod 2) : LinearMap.BilinForm (ZMod 2) K

The alternating polar form B(u, w) = ℓ(u²w + uw²) of the Gold component ℓ(x³).

Equations

• Algebraic.Aggregate.Geometry.Gold.polarForm ℓ = LinearMap.mk₂ (ZMod 2) (fun (u w : K) => ℓ (u ^ 2 * w + u * w ^ 2)) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Algebraic.Aggregate.Geometry.Gold.polarForm_apply {K : Type u_1} [Field K] [Algebra (ZMod 2) K] [CharP K 2] (ℓ : K →ₗ[ZMod 2] ZMod 2) (u w : K) : ((polarForm ℓ) u) w = ℓ (u ^ 2 * w + u * w ^ 2)

theorem Algebraic.Aggregate.Geometry.Gold.two_mul_finrank_le_of_isotropic {K : Type u_1} [Field K] [Algebra (ZMod 2) K] [CharP K 2] [Finite K] (ℓ : K →ₗ[ZMod 2] ZMod 2) (nonzero : ℓ ≠ 0) (cube : Function.Injective fun (x : K) => x ^ 3) (U : Submodule (ZMod 2) K) (isotropic : ∀ u ∈ U, ∀ w ∈ U, ℓ (u ^ 2 * w + u * w ^ 2) = 0) : 2 * Module.finrank (ZMod 2) ↥U ≤ Module.finrank (ZMod 2) K + 1

If cubing is injective, every subspace on which the polar form of a nonzero component vanishes has at most half of one more than the field dimension.