Cut counting for commutative aggregate networks

An aggregate network checks local Boolean wire constraints and an arbitrary predicate of the product of its vertex contributions. The finite state space can be any commutative monoid, including noncancellative operations such as AND, OR, and capped counting. Every extra aggregate state multiplies the usual cut-counting bound once.

The proof charges the first large past set to the cut values and accumulator before processing the vertex, together with its incident edge values. This outgoing key determines the next aggregate even when multiplication cannot be inverted.

theorem Algebraic.Cutwidth.AggregateNetwork.card_accepting_le {n : ℕ} {V E M : Type} [CommMonoid M] [Fintype V] [Fintype E] [Fintype M] (N : AggregateNetwork n V E M) [LinearOrder V] [Nonempty V] {f : Cslib.BooleanFunction n} (hf : N.Computes f) (hdeg : N.MaxDegreeLE 3) {w : ℕ} (hw : ∀ (v : V), (N.cut (Network.below v)).card ≤ w) {K : ℕ} (hK : 1 < K) (hrect : RectangleFree f K) : (accepting f).card ≤ Fintype.card M * (K - 1) * 2 ^ (n - N.read.card) + Fintype.card V * 2 ^ (w + 3) * Fintype.card M * (K - 1) ^ 2

Cut counting with one finite commutative aggregate. The first term accounts for terminal aggregate states with small past sets; the second counts outgoing transitions.

theorem Algebraic.Cutwidth.AggregateNetwork.card_accepting_le_of_read_eq_univ {n : ℕ} {V E M : Type} [CommMonoid M] [Fintype V] [Fintype E] [Fintype M] (N : AggregateNetwork n V E M) [LinearOrder V] [Nonempty V] {f : Cslib.BooleanFunction n} (hf : N.Computes f) (hread : N.read = Finset.univ) (hdeg : N.MaxDegreeLE 3) {w : ℕ} (hw : ∀ (v : V), (N.cut (Network.below v)).card ≤ w) {K : ℕ} (hK : 1 < K) (hrect : RectangleFree f K) : (accepting f).card ≤ (Fintype.card V * 2 ^ (w + 3) + 1) * Fintype.card M * (K - 1) ^ 2

If every input has a port, one additional layer absorbs the terminal-state term.