Explicit affine-plus-conjunction representations of circuit outputs

Every output coordinate is an affine function of the primary bits plus a linear combination of actual conjunction gate outputs. This representation allows arbitrary arity, depth, and nonlinear reuse, including signed and constant gates.

theorem Algebraic.Aggregate.Geometry.output_affine_conjunction_representation {n m : ℕ} (c : Circuit signature n m) (j : Fin m) : ∃ (b : ZMod 2) (L : (Fin n → ZMod 2) →ₗ[ZMod 2] ZMod 2) (w : { i : Fin c.size // Op.isConjunction (c.program.lines i).op = true } → ZMod 2), ∀ (x : Fin n → Bool), bitValue (c.eval interpretation x j) = b + L (bitVector x) + ∑ i : { i : Fin c.size // Op.isConjunction (c.program.lines i).op = true }, w i * bitValue (c.program.gateFunction interpretation (↑i) x)

Every output coordinate has an affine-plus-conjunction-feature representation, using actual conjunction outputs without changing their Boolean polarity.