Exact output-guess simulation of commutative aggregate circuits

The mixed signature combines arbitrary binary Boolean operations with finite commutative-monoid aggregates. One guessed bit per special occurrence replaces that gate by a nullary constant. All wire indices and ordinary slots are retained.

consistent_iff_eq_actualGuess gives exact unique-witness simulation, including special-to-special wiring. accepts_mix_of_componentKey_eq gives the component rectangle-cover property with at most 2 ^ budget p keys. componentAccept_iff expresses each fixed-guess, fixed-outside computation as a product of local signal observations, suitable for the aggregate network compiler.

theorem Algebraic.Aggregate.eval_eraseCircuit_of_consistent {J : Type} {State : J → Type} {n m : ℕ} [(j : J) → CommMonoid (State j)] (c : Circuit (signature State) n m) (a : Guess c.program) (input : Fin n → Bool) (consistent : Consistent c.program a input) : (eraseCircuit c a).eval ordinaryInterpretation input = c.eval interpretation input

Every designated output is preserved by a consistent special-output guess.

theorem Algebraic.Aggregate.eval_eq_iff_exists_consistent {J : Type} {State : J → Type} {n m : ℕ} [(j : J) → CommMonoid (State j)] (c : Circuit (signature State) n m) (input : Fin n → Bool) (outputs : Fin m → Bool) : c.eval interpretation input = outputs ↔ ∃ (a : Guess c.program), Consistent c.program a input ∧ (eraseCircuit c a).eval ordinaryInterpretation input = outputs

Exact circuit semantics via output guesses and their original consistency equations.