Majority-fiber 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.5644077959 and P ≈ 0.5640721944. The exact constants combine majority
fibers, both entropy bounds, and affine geometry.
Fan-in, fanout, depth, and literal repetitions remain unrestricted.
theorem
Algebraic.Aggregate.Geometry.Inversion.fiberCoefficient_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.