ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

A concrete multilinearization calculation

Example

Over $F = Z / 101$ let $P (x, z) = x^{3} z + 2 x^{2} + z .$ Then $P (0, z) = z$ and $P (1, z) = 2 z + 2$ , so the multilinearization in the first variable is $R_{x} P = (1 - x) z + x (2 z + 2) = z + x (z + 2) .$ The polynomial $R_{x} P$ agrees with $P$ at $x = 0$ and at $x = 1$ for every value of $z$ , its degree in $x$ is at most one, and it is exactly one precisely when $z \neq 99$ ; its degree in $z$ is one, while the original $P$ has degree three in $x$ .

Facts & Assumptions

Given: The field $Z / 101$ and the polynomial $P (x, z) = x^{3} z + 2 x^{2} + z$ .

[A1]

The multilinearization in one variable is $R_{X} P = (1 - X) (P ∣_{X = 0}) + X (P ∣_{X = 1})$ ; substituting $X = 0$ and $X = 1$ into the right-hand side returns $P ∣_{X = 0}$ and $P ∣_{X = 1}$ (Multilinearization in one variable).

[A2]

The reduction $R_{X} P$ agrees with $P$ wherever $x$ is Boolean, has degree at most one in $x$ , and has degree in every other variable at most that of $P$ in that variable (Multilinearization preserves Boolean values and bounds individual degree).

[A3]

The classes of $Z / 101$ form a field, so its arithmetic is addition and multiplication modulo $101$ and every nonzero residue is invertible (For every prime $p$ , the two operations on $Z / p$ make it a field).

Verification

1.1

Substituting $x = 0$ gives $P (0, z) = 0 + 0 + z = z$ , and substituting $x = 1$ gives $P (1, z) = z + 2 + z = 2 z + 2$ ; both are computed in $Z / 101$ by [A3].

A3givenalgebra

2.1

By [A1] and step 1.1, $R_{x} P = (1 - x) z + x (2 z + 2) = z - x z + 2 x z + 2 x = z + x (z + 2)$ , a polynomial of degree one in $x$ with $x$ -coefficient $z + 2$ and of degree one in $z$ .

A1step 1.1algebra

3.1

Evaluating the result of step 2.1 at the Boolean points: $R_{x} P (0, z) = z + 0 = z = P (0, z)$ and $R_{x} P (1, z) = z + z + 2 = 2 z + 2 = P (1, z)$ , which is the agreement asserted in [A2].

step 2.1A2algebra

4.1

The coefficient of $x$ in $z + x (z + 2)$ is $z + 2$ , which vanishes exactly when $z = - 2 \equiv 99$ in $Z / 101$ by [A3]; hence the $x$ -degree is one for $z \neq 99$ and zero at $z = 99$ , and in either case it is at most one, as [A2] requires. The degree in $z$ is one, which does not exceed the $z$ -degree one of $P$ , and the degree in $x$ dropped from three to one while the values at the Boolean points were preserved.

step 3.1A2A3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

A. Shen, IP = PSPACE: Simplified Proof, JACM 39(4) 1992, pp. 878–880 (standard reference, not scraped)
Arora and Barak, Computational Complexity: A Modern Approach, Remark 8.19, author-hosted draft (standard reference, not scraped)