Gate lower bounds for the Gold map

Let K be a binary field of odd dimension n ≥ 3 with any linear coordinate basis. Every signed unbounded AND/OR/XOR circuit computing all n output bits of x ↦ x³ has at least (3n - 3)/2 conjunction gates, and its total gate count g satisfies (4 + 2c)g ≥ (7 + 4c)n - (3 + 4c) with c = 1 - H₂(1/4), so g ≥ 1.771556n - 0.857781. Fan-in, fanout, depth, literal repetitions, and nonlinear reuse are unrestricted; the permutation, nonliteral, affine-restriction, and component properties are proved for the Gold map itself.

theorem Algebraic.Aggregate.Geometry.Gold.three_mul_input_le_two_mul_conjunctionCount_add_three {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (odd : Odd n) (dimension : 3 ≤ n) (c : Circuit signature n n) (computes : c.Computes interpretation (goldFunction e)) : 3 * n ≤ 2 * conjunctionCount c.program + 3

In odd dimension n ≥ 3, computing the Gold map requires at least (3n - 3)/2 conjunction gates, for every supplied linear coordinate basis.

theorem Algebraic.Aggregate.Geometry.Gold.entropy_mul_size_lower_bound {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (odd : Odd n) (dimension : 3 ≤ n) (c : Circuit signature n n) (computes : c.Computes interpretation (goldFunction e)) : (7 + 4 * Cutwidth.Aggregate.Geometry.Entropy.bitSaving) * ↑n - (3 + 4 * Cutwidth.Aggregate.Geometry.Entropy.bitSaving) ≤ (4 + 2 * Cutwidth.Aggregate.Geometry.Entropy.bitSaving) * ↑c.size

The restriction–rank and entropy inequalities for the Gold map in odd dimension.

theorem Algebraic.Aggregate.Geometry.Gold.gateCoefficient_mul_sub_constantPenalty_le_size {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (odd : Odd n) (dimension : 3 ≤ n) (c : Circuit signature n n) (computes : c.Computes interpretation (goldFunction e)) : gateCoefficient * ↑n - constantPenalty ≤ ↑c.size

The Gold-map gate bound in normalized form: g ≥ C n - P with C ≈ 1.771556 and P ≈ 0.857781.

theorem Algebraic.Aggregate.Geometry.Gold.exists_gateCoefficient_sub_mul_lt_size {ε : ℝ} (positive : 0 < ε) : ∃ (N : ℕ), ∀ {L : Type u_2} [inst : Field L] [Fintype L] [inst_2 : Algebra (ZMod 2) L] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] L), N ≤ n → Odd n → ∀ (c : Circuit signature n n), c.Computes interpretation (goldFunction e) → (gateCoefficient - ε) * ↑n < ↑c.size

For every ε > 0, all sufficiently large odd dimensions require more than (C - ε)n gates for the Gold map, uniformly over binary fields and coordinate bases.