The explicit family and the joint-message coefficient

The existing Chattopadhyay--Liao family requires more than (C-ε)n signed unbounded AND/OR/XOR gates eventually, where C = (H₂(1/4)+3/4)/(H₂(1/4)+1/2), approximately 1.19065368005. No sparsity, depth, fanout, or fan-in hypothesis is imposed.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.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 family attains the joint-message coefficient over the whole basis.