The affine pairing bound for signed AND/OR/XOR circuits

The theorem constructs an actual nonempty monochromatic affine flat. Its gate count consequence for sumset dispersers is unconditional on any geometric-saving interface: the pairing and all restriction invariants are proved for the actual acyclic program.

theorem Algebraic.Aggregate.Geometry.two_mul_input_le_size_add_multi {n g K : ℕ} (p : Program signature n g) (out : Wire n g) (disperse : Cutwidth.FlatSumsetDisperser (p.wireFunction interpretation out) K) : 2 * n ≤ g + multiCount p + 2 * Nat.clog 2 K

A sumset disperser requires twice its input length in gates plus the number of multiple-primary conjunctions, up to twice its logarithmic source threshold.