The Gold map in Boolean coordinates

A linear coordinate equivalence e : 𝔽₂ⁿ ≃ K supplies an arbitrary basis of a binary field K. The Gold map encodes its input with e, cubes it in K, and decodes all n output bits in the same basis. When n is odd, three is coprime to 2^n - 1, so cubing and hence the encoded map are permutations.

noncomputable def Algebraic.Aggregate.Geometry.Gold.goldFunction {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (x : Fin n → Bool) : Fin n → Bool

The Gold map x ↦ x³ of a binary field, in the Boolean coordinates of e.

Equations

• Algebraic.Aggregate.Geometry.Gold.goldFunction e x = (Algebraic.Aggregate.Geometry.Inversion.encode e).symm ((Algebraic.Aggregate.Geometry.Inversion.encode e) x ^ 3)

theorem Algebraic.Aggregate.Geometry.Gold.encode_goldFunction {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (x : Fin n → Bool) : (Inversion.encode e) (goldFunction e x) = (Inversion.encode e) x ^ 3

Decoding the Gold map recovers exactly the field cube.

theorem Algebraic.Aggregate.Geometry.Gold.cube_injective_of_odd {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} [Fintype K] (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (odd : Odd n) : Function.Injective fun (x : K) => x ^ 3

In odd dimension, cubing is injective on the field.

theorem Algebraic.Aggregate.Geometry.Gold.goldFunction_bijective {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} [Fintype K] (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (odd : Odd n) : Function.Bijective (goldFunction e)

In odd dimension, the encoded Gold map is a permutation.