A nonlinear-generator lower bound for multiple outputs

Every conjunction gate contributes at most one generator modulo affine functions of the primary inputs. Consequently, independent nonaffine output components require at least as many conjunction gates as output coordinates, with no bound on gate arity, circuit depth, or nonlinear reuse.

theorem Algebraic.Aggregate.Geometry.NonaffineComponents.output_le_conjunctionCount {n m : ℕ} {c : Circuit signature n m} (independent : NonaffineComponents (c.eval interpretation)) : m ≤ conjunctionCount c.program

The number of independent nonaffine output components bounds conjunction count.