TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Uniform threshold iterated integer arithmetic

Statement

For $m, w \geq 1$ explicitly listed nonnegative $w$ -bit integers, iterated sum and product have constant-depth polynomial-size uniform threshold-circuit families over AND, OR, NOT and MAJ. Their exact binary outputs need at most $w + ⌈ \log_{2} m ⌉$ and $m w$ bits, respectively. Addition is DLOGTIME-uniform and multiplication is logspace-uniform, each in the total input length, under the explicit bit-array convention: input bit $x_{i, j}$ has tuple address $(i, j)$ , dimensions are supplied to the uniformity machine, and power-of-two padding uses zero entries. Circuit gate addresses have a fixed number of binary coordinate fields. The claim concerns this explicit representation, rather than arbitrary effectively decodable encodings.

Facts & Assumptions

Given: $m, w \geq 1$ and the explicit input array and uniformity conventions in the Statement.

[F1]

DLOGTIME uniform iterated addition threshold circuits constructs exact iterated addition with DLOGTIME-uniform constant-depth polynomial-size threshold circuits in this array convention.

[F2]

Logspace uniform iterated multiplication threshold circuits constructs exact iterated multiplication with logspace-uniform constant-depth polynomial-size threshold circuits in this array convention.

Proof

1.1givenalgebra

Each summand is at most $2^{w} - 1$ , so their sum is at most $m (2^{w} - 1) < m 2^{w} \leq 2^{w + ⌈ \log_{2} m ⌉}$ . Each factor is less than $2^{w}$ , so their product is less than $2^{m w}$ . Thus the stated widths suffice, including zero inputs and leading-zero padding.

2.1F1F2step 1.1construct∎

Apply [F1] to the input bit array to obtain the sum circuit, with precisely the permitted sum output width and the declared DLOGTIME uniformity. Its construction permits arbitrary $m, w$ ; in particular the uniformity bound is logarithmic in the explicit array length even when the number of summands is large. Apply [F2] to the same array to obtain the product circuit, padded to $m w$ bits, with the declared logspace uniformity. These suppliers use exactly the gate basis and representation required here. Together with step 1.1, they establish all the circuit and output claims.

Depends on

Used by

Counting time space to linear hierarchy Lemma

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Eric Allender et al., Time-Space Tradeoffs in the Counting Hierarchy (standard reference, not scraped)
Hesse, Allender, and Barrington, Uniform Constant-Depth Threshold Circuits for Division and Iterated Multiplication (standard reference, not scraped)