Aggregate counting from a graph ordering bound

The graph ordering theorem controls the Boolean frontier, while the cardinality of the finite commutative monoid contributes one multiplicative factor. Every input is read, so the terminal-state term costs only one additional layer.

theorem Algebraic.Cutwidth.AggregateNetwork.card_accepting_le_of_orderingBound {n : ℕ} {V E M : Type} [CommMonoid M] [Fintype V] [Fintype E] [Fintype M] [Nonempty V] (N : AggregateNetwork n V E M) {A η C : ℝ} (hAη : 0 ≤ A + η) (hC : 0 ≤ C) (order : Multigraph.OrderingBound A η C) {f : Cslib.BooleanFunction n} (hf : N.Computes f) (hread : N.read = Finset.univ) (hloop : N.Loopless) (hdeg : N.MaxDegreeLE 3) (hconn : N.Connected) {s : ℕ} {Vb : ℝ} (hV : ↑(Fintype.card V) ≤ Vb) (hdiff : ↑(Fintype.card E) - ↑(Fintype.card V) ≤ ↑s - ↑n) {K : ℕ} (hK : 1 < K) (hrect : RectangleFree f K) : ↑(accepting f).card ≤ (Vb * 2 ^ ((A + η) * max (↑s - ↑n) 0 + 3 * Real.logb 2 Vb + C + 3) + 1) * ↑(Fintype.card M) * ↑K ^ 2

A graph ordering bound gives the real-valued accepting-input bound with one aggregate state factor. The vertex bound and edge-excess bound can be supplied by any compiler.