Internal gate \(i\) reads only wires below \(N + i\), and the output vertices come last. Each edge comes from at least one gate-input occurrence.

Fix the inputs one at a time; each step removes one input wire, rewires the gates that read it so that they compute the same values, and keeps the gates.

Induction on \(k\). Fixing the first input of a function to a constant does not increase its size, since the input can be hardwired without adding gates, and the disjunction of two functions has size at most the sum of their sizes plus one.

Count the same uses by their slots and by their supplying wires. Each gate contributes its first use and its excess; each shared gate has at least one excess use.

Convert between polynomial bounds and big-O power bounds.

The program lists the internal gates and then the output gates, with each wire renumbered in CSLib’s layout, and the outputs are the last \(M\) gates. Induction on the position shows that every gate of the program carries the value of the corresponding typed gate.

The two models share their wire layout, so the first translation maps each CSLib gate to one of ours: \(\neg w\) becomes \(\neg w \wedge \neg w\) and a constant becomes \(x_0 \wedge \neg x_0\) or \(x_0 \vee \neg x_0\). For the second, keep every wire and its negation available, at a cost of \(N\) gates for the negated inputs, two gates per internal gate, and one gate per output. The length-zero slice, which our families answer separately, is a single constant gate in CSLib’s model.

By the equality with CSLib’s \(\mathsf{P/poly}\), this is CSLib’s theorem that some language lies outside its \(\mathsf{P/poly}\): by Shannon’s counting argument some language has, at every large length \(n\), no De Morgan circuit with at most \(2^n / n\) gates, and every bound \(n^k + k\) falls below \(2^n / n\) for large \(n\). That theorem, like CSLib’s \(\mathsf{P/poly}\), comes from the author’s work outside upstream CSLib described in Theorem 281.

The first translation replaces each CSLib gate by one gate of ours. For the second, keep both rails of every wire: negate the inputs once, compute each gate’s positive rail directly and its negative rail by De Morgan from the complementary rails, so each gate costs two gates and no extra depth.

Unroll a polynomial-time decider into its circuit family.

The actual values give a consistent guess by induction in program order. Conversely, a consistent cut evaluation satisfies every gate equation, so CSLib’s uniqueness theorem for program evaluation identifies it with the original evaluation.

At each length, unroll the advised machine and hardwire the fixed advice prefix of its input.

The advice at length \(n\) is the family code at length \(n\), which has polynomial length by Lemma 292, and the machine is the serialized circuit evaluator, whose quadratic running time in the length of the paired input is polynomial in \(|x|\).

Combine the two containments.

The iterative evaluator agrees gate by gate with typed evaluation.

Validate the outer pair and copy the code and the input onto work tapes in linear time. Then stream the gates once, appending each gate value to a memo tape and reading the two referenced values by unary lookup; each gate costs \(O(|\mathrm{memo}|)\) steps, for a total of \(20(|c| + |x| + 1)^2\) steps in the core.

Encode bounded configurations one-hot, compile the initial configuration and one transition layer as Boolean formula fragments, tile \(T\) layers, and append a final halt-and-output gate.

A deterministic machine ignores its choices, so any fixed choice string gives the output bit.

Forget the generator.

Since \(\mathsf{FL} \subseteq \mathsf{FP}\), the map \(x \mapsto \langle \mathrm{gen}(1^{|x|}), x \rangle \) is in \(\mathsf{FP}\). The language is the preimage of the evaluation language under this map, and \(\mathsf{P}\) is closed under preimages by \(\mathsf{FP}\) functions. The size bound of the family is not used.

The padding gates are never read and the final gate copies the acceptance bit, so correctness and the size bound come from Theorem 294, the choices being irrelevant to a deterministic machine. For the code map, the direct unrolling is an initialization fragment, a stream of fixed-size transition fragments whose wire offsets have closed forms, and a final gate. A streaming transducer computes the offsets with binary counters, addition, multiply-add and fixed-polynomial evaluation, and writes each reference in terminated unary. One polynomial bounds every counter value, so the auxiliary space is logarithmic.

A machine that decides \(L\) in time \(q\) also decides it in time \(h(n) = q(n) + n + 1\). At horizon \(h\) its padded direct unrolling decides \(L\), has polynomial size, and has a code map in \(\mathsf{FL}\).

Combine the two containments.

Amplification makes the error on each input less than \(2^{-(n+1)}\), and a union bound over the \(2^n\) inputs leaves a good seed.

Compose copies of the original acceptance circuit rather than unrolling the repeated machine, whose control state would store the whole vote vector.

Apply the hardwired amplification family to a \(\mathsf{BPP}\) machine.

Compose the two containments.

Monotonicity is monotonicity of the depth envelope. For \(\mathsf{AC}^i \subseteq \mathsf{TC}^i\), transport circuits along the embedding of AND and OR gates as threshold gates, which preserves semantics, size and depth exactly.

Monotonicity is monotonicity of the depth envelope. Every AND or OR gate is an AND/OR/\(\mathrm{MOD}_m\) gate with the same semantics, so circuits transport along this embedding with the same size and depth.

A fan-in-two gate is an unbounded gate. Conversely, size does not count wires, so first merge repeated inputs of each unbounded gate: a gate of a circuit with \(n\) inputs and \(G\) internal gates then reads at most \(2(n + G)\) distinct literals, a polynomial number. Replace each such gate by a balanced fan-in-two tree of depth \(O(\log n)\), and a gate with no inputs by a constant built from an input and its negation.

Accepting shifts correspond bijectively to permutations of \(G\) via \(s_i=\pi (i)-w_i\). The inequality \(k^k\le 3^k k!\) bounds the failure probability, and a finite union bound supplies the covering family. The formalization samples all shifts and rejects incorrect sums, instead of restricting the sampling space to compatible sums as in the paper.

Induct on depth, using a truth-table CNF or DNF at depth two. At the next depth, choose powers of distinct primes, each comparable to an integer root scale, whose product exceeds \(n\). For each modulus, partition the inputs into balanced residue blocks. Complementing the second block makes a difference of two block weights a symmetric function of the combined inputs, so the induction hypothesis computes each comparison. Merge their AND roots to build shifted tests, and add one OR layer over a covering family. Coprimality makes the modular equalities certify exact weight. Merge the OR roots for all accepted weights to compute \(f\). The explicit finite recurrence bounds size by \(2^{O(k)}\) when \(n\le k^{d-1}\). The layer compiler preserves gate count, bounds CSLib’s circuit depth, and restricts all negations to primary inputs.

Specialize to depth three, or to the majority function, respectively.

Structural recursion on wire indices; an edge negation followed by its gate costs two formula levels.

One explicit pair is checked by kernel computation, and the \(5\)-cycles form a single conjugacy class.

Induction on the formula, for all target \(5\)-cycles at once. The variable \(x_i\) is the instruction \((i, 1, \sigma )\), the constant true is a single constant instruction, and false is the empty program. For a negation, compute the subformula through \(\sigma ^{-1}\) and fold a final multiplication by \(\sigma \) into the last instruction, so the length does not grow. For a conjunction, write \(\sigma = [a, b]\) with \(5\)-cycles \(a\) and \(b\) and concatenate programs for the two conjuncts through \(a\) and \(b\) and their inverses, four blocks of length at most \(4^{d-1}\). A disjunction is a negated conjunction of negations, with the negations folded in the same way.

Follow the recursion of Theorem 320, writing each target \(5\)-cycle \(\sigma \) as the commutator of the conjugates of \(a_0\) and \(b_0\) by the first permutation, in an explicit enumeration of \(S_5\), that conjugates \(\sigma _0\) to \(\sigma \).

Split the program in half and compose the two halves through the \(w\) possible intermediate points.

Compile \(\varphi _n\) at the fixed \(5\)-cycle \(\sigma _0\). The program evaluates to \(\sigma _0\) or to the identity, and a \(5\)-cycle moves every point, so any designated point is moved exactly when \(\varphi _n\) is true. Its length is at most \(4^{c \lfloor \log _2 n \rfloor + c} \le 4^c n^{2c}\), and it reads only variables below \(n\) (constant instructions read variable \(0\)). Conversely, a program of length at most \(C (n + 1)^k\) has a balanced decision formula of depth at most \(6 \lceil \log _2 (C (n + 1)^k) \rceil + 2\), which is logarithmic in \(n\), with its variables below \(n\).

Unfold the output of each circuit; the depth at most doubles, from \(c \lfloor \log _2 n \rfloor + c\) to \(2c \lfloor \log _2 n \rfloor + 2c\), and the variables stay below the arity. The polynomial size bound is not used.

A formula of depth \(d\) has fewer than \(2^{d+1}\) nodes, so logarithmic depth gives polynomial size. At each length \(n \ge 1\), compile each node to a gate, pushing negations down by De Morgan’s laws into input flags and building constants from an input and its negation; the stored answer at length \(0\) is the value of \(\varphi _0\).

Run the compiler on the decoded formula and bound each serialized instruction by the code length of the formula.

Emit the compiled program instruction by instruction: an instruction index is a path of length \(\mathrm{depth}(\varphi )\) in the recursion tree, with a constant amount of permutation data per level, and the formula node at the current position is located by counting in the input code.

Forward: compose the formula generator with the small-space Barrington generator; the depth is \(O(\log n)\), so the space is \(O(\log n)\). Backward: generate the balanced decision formula of each program in logarithmic space.

OpenAI’s construction parses a linear hash, a binary polynomial modulus, and coefficient blocks, then evaluates a polynomial in the quotient ring. Its finite tape program implements this evaluation in polynomial time. The lower bound combines sparse-CNF decomposition, random restrictions, hard parameter slices, and the resulting correlation estimates.

Every surviving variable is the image of a variable in the original clause’s scope. Its scope therefore has no greater cardinality. Clause normalization preserves disjunctions; discarded clauses are true.

OpenAI’s hard-slice theorem bounds every such CNF indicator’s correlation by \(6\, 2^{-4(s+1)\sqrt d}\) on a suitable restriction of the input. Restrict all features together, preserving their widths and coefficients. Average the margin inequality and use the triangle inequality.

An integer score \(t\) is nonnegative exactly when \(2t+1\) is positive. The new score has signed margin at least one and coefficient weight \(1+2\sum _j|z_j|\). Apply the preceding corollary.

Exactly one fresh bit accepts for each assignment to the old inputs; reuse the library’s existing balanced-padding count. De Morgan’s laws exchange the three layers and complement the bottom inputs.

Fix the fresh bit to recover the original hard function from either output polarity. Input substitution preserves the gate count. Apply the source bound with exponent constant \(2A\) and use \(\sqrt{n+1}\le 2\sqrt n\) for \(n\ge 1\).

Represent each source tape by one binary track per alphabet symbol. Copy and rewind the input in \(2n+2\) steps, simulate each source step in one step, then emit the verdict and halt in one step. Apply the existing CSLib machine bridge.

Apply the machine bridge to the explicit decider. The verdict characterization of \(\mathsf P\) and the existing balanced-padding \(\mathsf{FP}\) closure preserve uniform polynomial time; the preceding lower-bound and counting theorems apply.

Removing repeated literals does not change disjunction and only decreases the number of distinct variables. Index bottom gates by a CNF and a clause position, and evaluate each middle gate as that CNF.

Apply the source-model theorems to the semantics-preserving conversion and use its gate-count equality and width bound.

A program adapter preserves each wire’s value and depth, so the existing typed wire normalizer applies. Flatten adjacent equal-polarity formula gates, and negate an AND root when necessary. Count clauses and conjunctions.

The normalization theorem supplies a source circuit in one polarity, covered by balanced hardness. Eventually \(n\le 2^{\sqrt n}\), and if \(s\le 2^{A\sqrt n}\) the normalized gate count is at most \(2^{5(A+1)\sqrt n}\). Apply source hardness with the larger exponent constant.

Apply OpenAI’s finite-win theorem and its tensor amplification and Chinese-remainder Fourier factorization. The minimum is attained because every finite matrix has a finite scalar circuit. Nonnegativity and the cofinal upper bounds give the normalized liminf.

Induct on the source program to identify every available wire with its translated trace value. To absorb the zero gate, apply the source bound with coefficient \(c/2\) and choose the size large enough that \((c/2)n\log _2n{\gt}1\).

Scalar operations are polynomial, so the existing polynomial-circuit linearization supplies the certificate required by the DFT lower bound. Transfer this bound back through the one-gate translation and absorb the constant using \(\varepsilon /2\). Choose an upper-bound witness beyond the lower-bound threshold to obtain the simultaneous inequalities.