Circuit hardness properties of the Gold map

All output coordinates of the encoded Gold map are simultaneously affine only on flats of at most two points. In odd dimension n, no nonzero linear output component is affine on a flat with at least 2^((n+3)/2) points: its direction space would be totally isotropic for the polar form, whose radical has dimension at most one. In dimension at least three no output coordinate is a signed primary literal.

theorem Algebraic.Aggregate.Geometry.Gold.card_flat_le_two {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (S : AffineFlat n) (affine : ∀ (i : Fin n), AffineOn S fun (x : Fin n → Bool) => goldFunction e x i) : S.carrier.card ≤ 2

Every simultaneous affine restriction of the Gold map contains at most two points.

theorem Algebraic.Aggregate.Geometry.Gold.goldFunction_nonaffineOnFlats {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} [Fintype K] (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (odd : Odd n) : NonaffineOnFlats (goldFunction e) ((n + 3) / 2)

In odd dimension, every nonzero linear component of the Gold map is nonaffine on each flat with at least 2^((n+3)/2) points.

theorem Algebraic.Aggregate.Geometry.Gold.goldFunction_nonliteral {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} [Fintype K] (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (odd : Odd n) (dimension : 3 ≤ n) (i j : Fin n) (b : Bool) : (fun (x : Fin n → Bool) => goldFunction e x i) ≠ fun (x : Fin n → Bool) => b ^^ x j

In odd dimension at least three, no Gold output coordinate is a signed primary literal.