Affine functions and actual conjunction features span circuit outputs

The submodule generated by affine primary functions and actual conjunction gate functions contains every gate, and hence every designated output wire.

theorem Algebraic.Aggregate.Geometry.output_mem_affine_sup_conjunctionRange {n m : ℕ} (c : Circuit signature n m) (j : Fin m) : (fun (x : Fin n → Bool) => bitValue (c.eval interpretation x j)) ∈ affineFunctions n ⊔ (Fintype.linearCombination (ZMod 2) fun (i : { i : Fin c.size // Op.isConjunction (c.program.lines i).op = true }) (x : Fin n → Bool) => bitValue (c.program.gateFunction interpretation (↑i) x)).range

Every output is an affine primary function plus a linear combination of the actual conjunction gate functions.