Nonlinear generators span all circuit outputs

Modulo affine primary functions, every affine gate is a linear combination of earlier values. The conjunction gates therefore span every output in this quotient. Independent output components force at least as many conjunction gates as outputs.

theorem Algebraic.Aggregate.Geometry.gateValues_mem {n g : ℕ} (p : Program signature n g) (S : Submodule (ZMod 2) ((Fin n → Bool) → ZMod 2)) (constants : ∀ (b : ZMod 2), (fun (x : Fin n → Bool) => b) ∈ S) (inputs : ∀ (i : Fin n), (fun (x : Fin n → Bool) => bitValue (x i)) ∈ S) (conjunctions : ∀ (i : Fin g), Op.isConjunction (p.lines i).op = true → (fun (x : Fin n → Bool) => bitValue (p.gateFunction interpretation i x)) ∈ S) (i : Fin g) : (fun (x : Fin n → Bool) => bitValue (p.gateFunction interpretation i x)) ∈ S

A linear subspace containing constants, primary bits, and conjunction outputs contains every gate function, including gates that reuse nonlinear values.

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

Independent nonlinear output coordinates require distinct nonlinear generators.