128 Boolean Analysis — Circuit Size

128.1 Overview

This file identifies the layerwise gate count $\mathrm{gateCountBefore}$ accumulated by the Razborov–Smolensky induction with the total circuit size $F.\mathrm{size}$ of a feed-forward circuit, by writing both as the sum of the cardinalities of the non-input layers. The identification is then used to restate the polynomial-approximation existence theorems of the previous chapter with their error bounds phrased directly in terms of the number of gates.

128.2 Declarations

Definition 128.1 Index of a non-input layer

✓

For a feed-forward circuit $F$, a bound $d \le F.\mathrm{depth}$ and an index $j : \mathrm{Fin}\, d$, the layer index $\mathrm{gateLayerIdx}\, F\, h_d\, j \in \mathrm{Fin}(F.\mathrm{depth}+1)$ is $j+1$, i.e. the $(j+1)$-st node layer of $F$. It packages the non-input layers $1, \dots , d$ as indices into $F.\mathrm{nodes}$ so that they can be summed over.

Lemma 128.2 Partial gate count as a sum of layer cardinalities

✓

Let $F$ be a feed-forward circuit with all node layers finite. Then for every $d$ with $d \le F.\mathrm{depth}$,

\[ \mathrm{gateCountBefore}\, F\, d \; =\; \sum _{j : \mathrm{Fin}\, d} \left\lvert F.\mathrm{nodes}(\mathrm{gateLayerIdx}\, F\, h_d\, j)\right\rvert , \]

that is, the number of non-input gates in the first $d$ layers is the sum of the cardinalities of those layers.

Lemma 128.3 Circuit size as a sum of layer cardinalities

✓

For a feed-forward circuit $F$ with all node layers finite,

\[ F.\mathrm{size} \; =\; \sum _{d : \mathrm{Fin}\, F.\mathrm{depth}} \left\lvert F.\mathrm{nodes}(d+1)\right\rvert , \]

so the total number of non-input gates equals the sum of the cardinalities of all non-input layers.

Lemma 128.4 Full-depth gate count is the circuit size

✓

For a feed-forward circuit $F$ with all node layers finite, taking $d = F.\mathrm{depth}$ gives

\[ \mathrm{gateCountBefore}\, F\, F.\mathrm{depth} \; =\; F.\mathrm{size}. \]

Theorem 128.5 Polynomial distribution for all outputs, size form

✓

Let $p$ be prime and let $F$ be a feed-forward circuit with finite node layers and a finite output type, all of whose gates lie in the $\mathrm{AC}^0[p]$ gate set. For every $\ell $ there exist a finite nonempty seed type $\mathrm{Seed}$ and polynomials $P : \mathrm{Seed} \to \mathrm{out} \to \mathbb {Z}/p[X_1,\dots ,X_n]$ such that every $P_{s,o}$ has total degree at most $\mathrm{circuitDegreeBound}\, p\, \ell \, F.\mathrm{depth}$, and for every Boolean input $x$ the seeds on which some output node is computed incorrectly, i.e. $P_{s,o}(\mathrm{boolInput}_p(x)) \ne F.\mathrm{eval}(x)(o)$ for some $o$, satisfy

\[ \left\lvert \{ s : \text{$s$ is bad for $x$}\} \right\rvert \cdot 2^{\ell } \; \le \; F.\mathrm{size} \cdot \left\lvert \mathrm{Seed}\right\rvert . \]

Theorem 128.6 Polynomial distribution for a single output, size form

✓

Same statement for a circuit with a unique output node: there exist a finite nonempty seed type $\mathrm{Seed}$ and polynomials $P : \mathrm{Seed} \to \mathbb {Z}/p[X_1,\dots ,X_n]$, each of total degree at most $\mathrm{circuitDegreeBound}\, p\, \ell \, F.\mathrm{depth}$, such that for every Boolean input $x$ the number of seeds $s$ with $P_s(\mathrm{boolInput}_p(x)) \ne F.\mathrm{eval}_1(x)$ obeys

\[ \left\lvert \{ s : \text{$s$ is bad for $x$}\} \right\rvert \cdot 2^{\ell } \; \le \; F.\mathrm{size} \cdot \left\lvert \mathrm{Seed}\right\rvert . \]

Theorem 128.7 Polynomial list for a single output, size form

✓

The list formulation of the previous theorem: for a circuit $F$ with a unique output node whose gates all lie in the $\mathrm{AC}^0[p]$ gate set, there is a nonempty list $Ps$ of polynomials in $\mathbb {Z}/p[X_1,\dots ,X_n]$, each of total degree at most $\mathrm{circuitDegreeBound}\, p\, \ell \, F.\mathrm{depth}$, such that for every Boolean input $x$ the sublist of $P \in Ps$ with $P(\mathrm{boolInput}_p(x)) \ne F.\mathrm{eval}_1(x)$ satisfies

\[ \left\lvert \{ P \in Ps : \text{$P$ is wrong at $x$}\} \right\rvert \cdot 2^{\ell } \; \le \; F.\mathrm{size} \cdot \left\lvert Ps\right\rvert . \]