Large components from joint aggregate states

The compressed component key consists of the actual joint state and one partial joint state. Its cardinality replaces the product of all special registers and outputs.

theorem Algebraic.Cutwidth.Aggregate.Compressed.exists_large_component {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {M : Type} [CommMonoid M] [Fintype M] {n g K : ℕ} (p : Program (Aggregate.signature State) n g) (compression : Aggregate.Compressed.Factorization p M) (out : Wire n g) (a : Aggregate.Guess p) (free : RectangleFree (fun (x : Cslib.BitString n) => p.trace Aggregate.interpretation x out) K) (dense : 2 ^ (n - 2) ≤ (accepting fun (x : Cslib.BitString n) => p.trace Aggregate.interpretation x out).card) (big : 3 * (Aggregate.Compressed.budget M + Nat.clog 2 K + 3) ≤ n) : ∃ (w : Wire n g), n - (Aggregate.Compressed.budget M + Nat.clog 2 K + 3) < (SingleCut.inputsIn (MultiOutput.component (Aggregate.erase p a) w)).card

For a dense rectangle-free output, one component of any guessed erasure contains almost all input coordinates. This includes guesses that are never realized by an input.