Finite capacity lower bounds for unrestricted aggregate circuits

Primary-input summaries let the receiving party reconstruct every gate in order. One additional bit handles a designated output that is itself a sending-party input. The number of special gates, their placement, and their fan-in are unrestricted.

This is a deterministic one-way communication argument. The broader gatewise communication approach is classical; see Roychowdhury, Orlitsky, and Siu, Lower Bounds on Threshold and Related Circuits via Communication Complexity (1994).

noncomputable def Algebraic.Cutwidth.Aggregate.circuitOneWaySummary {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {n : ℕ} (c : Circuit (Aggregate.signature State) n 1) (U : Finset (Fin n)) : OneWaySummary (c.outputFunction Aggregate.interpretation 0) U (Aggregate.Capacity.OutputKey c.program)

Per-gate primary-input summaries and one output bit form a one-way summary.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Aggregate.input_le_summaryBits_of_circuit {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] {n : ℕ} (c : Circuit (Aggregate.signature State) n 1) {K : ℕ} (free : RectangleFree (c.outputFunction Aggregate.interpretation 0) K) (dense : 2 ^ (n - 2) ≤ (accepting (c.outputFunction Aggregate.interpretation 0)).card) : n ≤ Nat.clog 2 (Fintype.card (Aggregate.Capacity.OutputKey c.program)) + 2 * Nat.clog 2 K + 5

Jointly encoding all summary registers can improve on rounding each register.

theorem Algebraic.Cutwidth.Aggregate.input_le_capacity_of_circuit {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] {n : ℕ} (c : Circuit (Aggregate.signature State) n 1) {K : ℕ} (free : RectangleFree (c.outputFunction Aggregate.interpretation 0) K) (dense : 2 ^ (n - 2) ≤ (accepting (c.outputFunction Aggregate.interpretation 0)).card) : n ≤ Aggregate.Capacity.capacity c.program + 2 * Nat.clog 2 K + 6

Every dense rectangle-free output requires nearly n bits of aggregate capacity. The six-bit constant includes the optional primary-output bit.

theorem Algebraic.Cutwidth.Aggregate.input_le_logCard_of_circuit {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] {n : ℕ} (c : Circuit (Aggregate.signature State) n 1) {K : ℕ} (free : RectangleFree (c.outputFunction Aggregate.interpretation 0) K) (dense : 2 ^ (n - 2) ≤ (accepting (c.outputFunction Aggregate.interpretation 0)).card) : ↑n ≤ Real.logb 2 ↑(Fintype.card (Aggregate.Capacity.Key c.program)) + 2 * ↑(Nat.clog 2 K) + 7

The finite bound also charges the exact logarithm of the joint summary space.

theorem Algebraic.Cutwidth.Aggregate.input_le_capacity_of_computes {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] {n : ℕ} (c : Circuit (Aggregate.signature State) n 1) {f : Cslib.BooleanFunction n} (computes : c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) {K : ℕ} (free : RectangleFree f K) (dense : 2 ^ (n - 2) ≤ (accepting f).card) : n ≤ Aggregate.Capacity.capacity c.program + 2 * Nat.clog 2 K + 6

The finite capacity bound stated for a circuit computing a specified function.