Conditional-majority lower bound for binary-field inversion #
For every supplied binary field and linear coordinate basis, all coordinates of
inversion require at least C * n - P gates for n ≥ 3, where
C ≈ 1.5659486596 and P ≈ 0.6016050397. The exact constants combine majority
fibers with residual entropy, both original entropy bounds, and affine geometry.
Fan-in, fanout, depth, and literal repetitions remain unrestricted.
theorem
Algebraic.Aggregate.Geometry.Inversion.conditionalFiberCoefficient_mul_sub_penalty_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))
:
Large majority fibers improve the gate bound for every binary-field coordinate basis.