Counting aggregate-network states

A first large past set is charged to an outgoing transition, consisting of the old cut values, old aggregate, and incident values. The transition need not be invertible.

theorem Algebraic.Cutwidth.AggregateNetwork.Internal.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

Aggregate cut counting, with a separate term for terminal states whose past sets never reach the rectangle threshold. The accumulator only needs a commutative monoid structure; outgoing transition keys avoid any cancellation assumption.

theorem Algebraic.Cutwidth.AggregateNetwork.Internal.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

When every input is read, the terminal term is absorbed into one extra layer.