Compiling jointly compressed aggregate circuits

The existing ordinary wiring compiler is unchanged. Only the guessed states and observations are compressed, so the original gate count and graph excess are retained.

theorem Algebraic.Cutwidth.Aggregate.Compressed.card_restriction_le {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {M : Type} [CommMonoid M] [Fintype M] {n g m : ℕ} (p : Program (Aggregate.signature State) n g) (compression : Aggregate.Compressed.Factorization p M) (out : Wire n g) (a₀ : Aggregate.Guess p) (K : MultiOutput.Internal.ClosedSet (Aggregate.erase p a₀)) (e : Fin m ≃ ↥(SingleCut.inputsIn K.carrier)) (outside : Fin n → Bool) (hm : 2 ≤ m) (hconn : ∀ u ∈ K.carrier, ∀ v ∈ K.carrier, Relation.ReflTransGen (MultiOutput.Linked (Aggregate.erase p a₀)) u v) {A η C : ℝ} (hAη : 0 ≤ A + η) (hC : 0 ≤ C) (order : Multigraph.OrderingBound A η C) {Krect : ℕ} (hK : 1 < Krect) (hrect : RectangleFree (fun (x : Cslib.BitString n) => p.trace Aggregate.interpretation x out) Krect) : ↑(accepting (restriction (fun (x : Cslib.BitString n) => p.trace Aggregate.interpretation x out) (SingleCut.inputsIn K.carrier) e.symm outside)).card ≤ ((↑n + 3 * ↑g) * 2 ^ ((A + η) * max (↑g - ↑m) 0 + 3 * Real.logb 2 (↑n + 3 * ↑g) + C + 3) + 1) * 2 ^ (Aggregate.Compressed.budget M + 1) * ↑Krect ^ 2

Summing exact guessed computations multiplies the component bound by at most 2 ^ (compressed budget + 1). The one extra bit observes the designated output without an edge.