The actual nonlinear-feature budget for inversion circuits #
Actual conjunction gate outputs generate every output modulo affine primary functions. Their multiple-primary subfamily has quarter-biased marginals, so the average-collision estimate charges these features as well as the circuit's primary summaries. No independence, arity, depth, or reuse restriction is needed.
theorem
Algebraic.Aggregate.Geometry.Inversion.input_add_feature_bias_le_conjunctionCount
{K : Type u_1}
[Field K]
[Fintype K]
[Algebra (ZMod 2) K]
{n : ℕ}
(e : (Fin n → ZMod 2) ≃ₗ[ZMod 2] K)
(c : Circuit signature n n)
(computes : c.Computes interpretation (inverseFunction e))
:
↑n + ↑(multiCount c.program) * Cutwidth.Aggregate.Geometry.Entropy.bitSaving - Real.log 5 / Real.log 2 ≤ ↑(conjunctionCount c.program)
An inversion circuit's actual conjunction outputs pay an entropy charge for every multiple-primary conjunction.
theorem
Algebraic.Aggregate.Geometry.Inversion.feature_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))
:
Charging actual nonlinear features and primary summaries strengthens the inversion
bound, with leading coefficient (3 + 4c) / (2 + 2c) for c = 1 - H₂(1/4).
theorem
Algebraic.Aggregate.Geometry.Inversion.featureCoefficient_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))
:
The nonlinear-feature inequality in normalized gate-count form.