A large component after aggregate-gate erasure #
The input sets of the erased circuit's components partition the coordinates. Every
union of components has a mixing summary with at most 2 ^ budget possible values.
Rectangle-freeness rules out a balanced union, forcing one component to contain all
but budget + clog 2 K + 3 inputs. No assumption about cancellation is used.
theorem
Algebraic.Cutwidth.Aggregate.exists_large_fibre_of_mixing
{n K D : ℕ}
{f : Cslib.BooleanFunction n}
(free : RectangleFree f K)
(dense : 2 ^ (n - 2) ≤ (accepting f).card)
{ι : Type u_1}
{T : Type u_2}
[Fintype ι]
[DecidableEq ι]
[Fintype T]
(color : Fin n → ι)
(short : Fintype.card T ≤ 2 ^ D)
(keys :
∀ (S : Finset ι),
∃ (key : (Fin n → Bool) → T),
∀ x ∈ accepting f, ∀ y ∈ accepting f, key x = key y → f (mix {i : Fin n | color i ∈ S} x y) = true)
(big : 3 * (D + Nat.clog 2 K + 3) ≤ n)
:
A finite partition with short mixing summaries has a part containing almost all inputs.
theorem
Algebraic.Cutwidth.Aggregate.exists_large_component
{J : Type}
{State : J → Type}
[(j : J) → CommMonoid (State j)]
[(j : J) → Fintype (State j)]
{n g K : ℕ}
(p : Program (Aggregate.signature State) n g)
(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.budget p + Nat.clog 2 K + 3) ≤ n)
:
∃ (w : Wire n g),
n - (Aggregate.budget p + 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.