The explicit family and the conditional-majority coefficient #
The existing balanced Chattopadhyay--Liao family requires more than (C-ε)n
signed unbounded AND/OR/XOR gates eventually, with C approximately 1.245391403.
The signature permits arbitrary fan-in, fanout, depth, and repeated signed literals.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.sourceReductionHardFamily_eventually_lt_size
{ε : ℝ}
(hε : 0 < ε)
:
∀ᶠ (n : ℕ) in Filter.atTop, ∀ (c : Circuit Aggregate.Geometry.signature n 1),
(c.Computes Aggregate.Geometry.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) =>
Extractor.sourceReductionHardFamily n x) →
(gateCoefficient - ε) * ↑n < ↑c.size
The fixed explicit balanced family attains the conditional-majority coefficient without depth, fanout, fan-in, or placement restrictions.