LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Sum-check verifier resources

Statement

With $D = \sum_{i = 1}^{n} (d_{i} + 1)$ , call a prover transcript well formed when every coefficient list meets its format and degree cap. In the next paragraph, “execution” means an execution whose received transcript is well formed, and “ $n$ rounds” is the protocol's schedule; an early-rejecting execution may complete fewer. Under streaming reception, an arbitrary execution receives at most $D + 1$ prover field elements before the verifier can detect and reject the first excess coefficient.

In sum-check with $n \geq 1$ , put $D = \sum_{i = 1}^{n} (d_{i} + 1)$ . An execution uses at most $D$ prover field elements, at most $n$ verifier field elements, $n$ independent uniform field samples on a full execution, and $n$ rounds. The verifier uses $O (D)$ field operations plus at most one trusted point evaluation; a full execution reaching the terminal check uses exactly one such evaluation. Early rejection may shorten these costs. Coefficient lists may be zero-padded to attain the $D$ bound.

With supplied $b$ -bit field representations, efficient encoding checks and field operations of bit cost at most $A (b)$ , the bit work is $O (D (A (b) + b))$ plus trusted evaluation and sampling costs. Polynomial time is conditional on polynomial bounds for these quantities and $D$ . With an efficient bijective indexing of field elements by ${0, \dots, q - 1}$ , $q = ∣ F ∣$ , rejection sampling uses expected $O (⌈ \log_{2} q ⌉)$ random bits per sample. If $q = 2^{b}$ with such a $b$ -bit encoding, a full execution uses exactly $n b$ random bits.

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

[F1]

Sum-check caps each coefficient list at d_i+1, samples a fresh challenge each round and uses trusted evaluation only for the terminal comparison (Sum-check with explicit degree bounds).

Proof

1.1

At round $i$ a well-formed coefficient list has at most $d_{i} + 1$ entries. Under streaming reception, read at most $d_{i} + 2$ field elements and reject immediately upon receiving the first excess coefficient; an explicit valid length prefix can make this detection cheaper. For a well-formed list, evaluate $h_{i}$ at $0, 1, r_{i}$ by the recurrence $v \leftarrow T v + a_{j}$ from highest coefficient downwards. Each evaluation costs $O (d_{i} + 1)$ field operations, also for a zero or constant message.

F1algebra

2.1

Summing the per-round work for a well-formed transcript gives $O (D)$ operations and at most $D$ received field elements. If the first overlength message occurs in round $i$ , the earlier rounds contribute at most $\sum_{j < i} (d_{j} + 1)$ elements and that round contributes at most $d_{i} + 2$ , for a total at most $D + 1$ ; other malformed messages stop no later. The protocol uses one fresh sample per completed round and sends at most one field element per round; the last need not be sent. It makes its only call to $g$ at the terminal comparison. Encoding checks and reading cost $O (D b)$ , and arithmetic costs $O (D A (b))$ ; adding evaluation and sampling costs gives the stated bit bound. This includes $n = 1$ and every zero bound $d_{i} = 0$ .

F1step 1.1algebra

3.1

For indexed sampling put $c = ⌈ \log_{2} q ⌉$ . Draw $c$ fair bits as an integer $J$ and retry if $J \geq q$ . The acceptance probability is $q / 2^{c} > 1 / 2$ (or one if $q$ is a power of two), and conditional on acceptance every valid index has probability $1 / q$ . The expected number of trials is $\sum_{k \geq 0} (1 - q / 2^{c})^{k} = 2^{c} / q < 2$ . Thus expected random-bit use is less than $2 c$ per sample; for $q = 2^{b}$ every trial succeeds and exactly $n b$ bits suffice for all rounds. Efficient index conversion is part of the sampling assumption, not a consequence of arbitrary encodings.

givenalgebra∎

Depends on

Sum-check with explicit degree bounds

Used by

One point evaluation for an exponentially large cube Counterexample
False: the sum-check verifier enumerates the cube False statement
Verifying formula counts over a supplied field Proposition

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

Justin Thaler, Proofs, Arguments, and Zero-Knowledge (2023), §4.1 Discussion of costs, Table 4.1 and Remark 4.2, pp.37–39 (standard reference, not scraped)