An unconditional whole-basis geometric lower bound

The existing fixed polynomial-time family requires more than (gateCoefficient - ε)n gates over the signed unbounded AND/OR/XOR basis, where gateCoefficient = (1+2c)/(1+c) and c = 1 - H₂(1/4). This is approximately 1.15876032857. There is no sparsity, depth, fanout, or fan-in hypothesis.

The proof combines affine restrictions in the tradition of Demenkov--Kulikov with one-way communication accounting in the tradition of Roychowdhury--Orlitsky--Siu. The hard family is the already checked Chattopadhyay--Liao construction. No claim of historical priority is part of the theorem.

theorem Algebraic.Cutwidth.Aggregate.Geometry.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 same explicit family is gate-hard above coefficient one for arbitrary-depth signed unbounded AND/OR/XOR circuits, including every binary Boolean operation.