Gate lower bounds for finite-field inversion

For every binary field and every linear coordinate basis, computing all bits of inversion requires at least 3n/2 - 2 signed unbounded AND/OR/XOR gates. The only size restriction is n ≥ 3; the permutation, nonprojection, and affine-restriction properties are proved for inversion itself, not assumed as hardness hypotheses. The entropy and output-rank refinement has leading coefficient (3 + 2c)/(2 + c), approximately 1.543112, where c = 1 - H₂(1/4). The actual nonlinear-feature budget further gives leading coefficient (3 + 4c)/(2 + 2c), approximately 1.579380, with its explicit additive penalty.

theorem Algebraic.Aggregate.Geometry.Inversion.three_mul_input_le_two_mul_size {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod 2) K] {n : ℕ} (e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K) (dimension : 3 ≤ n) (c : Circuit signature n n) (computes : c.Computes interpretation (inverseFunction e)) : 3 * n ≤ 2 * c.size + 4

Computing all coordinates of binary-field inversion costs at least 3n/2 - 2 gates, at arbitrary depth and with unrestricted fan-in and fanout.

theorem Algebraic.Aggregate.Geometry.Inversion.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) (dimension : 3 ≤ n) (c : Circuit signature n n) (computes : c.Computes interpretation (inverseFunction e)) : (3 + 2 * Cutwidth.Aggregate.Geometry.Entropy.bitSaving) * ↑n - 4 * Cutwidth.Aggregate.Geometry.Entropy.bitSaving ≤ (2 + Cutwidth.Aggregate.Geometry.Entropy.bitSaving) * ↑c.size

Output rank and biased messages strengthen the inversion coefficient above three halves.

theorem Algebraic.Aggregate.Geometry.Inversion.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) (dimension : 3 ≤ n) (c : Circuit signature n n) (computes : c.Computes interpretation (inverseFunction e)) : gateCoefficient * ↑n - constantPenalty ≤ ↑c.size

Every supplied binary-field coordinate basis has the same improved inversion gate bound.