LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Symmetrizing a Boolean-cube polynomial gives a Hamming-weight polynomial

Statement

Let $D \subseteq {0, 1}^{N}$ be invariant under coordinate permutations and let $f : D \to {0, 1}$ satisfy $f (π x) = f (x)$ for every permutation $π$ and $x \in D$ . If a real polynomial $p$ of total degree at most $d$ is an $ϵ$ -approximant to $f$ on $D$ , then there is a univariate real polynomial $q (t)$ of degree at most $d$ such that $q (∣ x ∣)$ is also an $ϵ$ -approximant on $D$ , where $∣ x ∣ : = \sum_{i < N} x_{i}$ is Hamming weight.

Facts & Assumptions

Given: A finite Boolean cube of dimension $N$ , a permutation-invariant domain $D$ , a permutation-invariant function $f$ , and a total-degree-at-most- $d$ approximant $p$ .

[F1]

Acceptance polynomials and approximate degree on Boolean domains: an $ϵ$ -approximant satisfies $∣ p (x) - f (x) ∣ \leq ϵ$ on each point of $D$ .

[F2]

$\tilde{f}$ is multilinear, agrees with $f$ at every point of ${0, 1}^{n}$ , is degree-nonincreasing when nonzero, and is the unique multilinear polynomial with that agreement: the multilinear reduction agrees with $p$ on the Boolean cube and does not increase total degree.

[F3]

Monomials, coefficients, degree in each variable and total degree in $F [x_{1}, \dots, x_{n}]$ : a multilinear polynomial is a finite sum of squarefree monomials, and a monomial indexed by $S \subseteq {0, \dots, N - 1}$ has degree $∣ S ∣$ .

[F4]

The reals form a totally ordered field: finite sums and averages use the ordered field structure of $R$ , including division by the positive integer $N!$ and by $(\binom{N}{s})$ for $s \leq N$ .

[F5]

The triangle inequality: absolute value is subadditive on $R$ .

Proof

1.1givenF2F3construct

Replace $p$ by its multilinear reduction $\tilde{p}$ from [F2]. It agrees at every Boolean point and has no monomial of degree greater than $d$ . Write $\tilde{p} (X) = \sum_{S \subseteq [N], ∣ S ∣ \leq d} c_{S} X_{S}$ , where $X_{S} : = \prod_{i \in S} X_{i}$ and $X_{\emptyset} = 1$ .

2.1givenF1F4F5step 1.1algebra

Define $\overset{ˉ}{p} (x) : = \frac{1}{N!} \sum_{π \in S_{N}} \tilde{p} (x_{π (0)}, \dots, x_{π (N - 1)})$ . For $x \in D$ , each permuted point is in $D$ and has $f (π x) = f (x)$ , so [F1] gives $∣ \tilde{p} (π x) - f (x) ∣ \leq ϵ$ for every $π$ . Repeated [F5] and division by the positive average factor from [F4] give $∣ \overset{ˉ}{p} (x) - f (x) ∣ \leq \frac{1}{N!} \sum_{π \in S_{N}} ∣ \tilde{p} (π x) - f (x) ∣ \leq ϵ$ .

2.2step 1.1F4algebra

Fix a set $S$ of size $s$ . Under the average over $S_{N}$ , each subset $R$ of size $s$ occurs as the permuted image of $S$ exactly $s! (N - s)!$ times. Hence the average of $X_{S}$ is ${(\binom{N}{s})}^{- 1} \sum_{∣ R ∣ = s} X_{R}$ , a polynomial of degree at most $s$ . Summing with coefficients $c_{S}$ shows that $\overset{ˉ}{p}$ has degree at most $d$ and is invariant under all coordinate permutations.

3.1step 2.1step 2.2F4algebra∎

If $x$ has Hamming weight $t$ , exactly $(\binom{t}{s})$ of the squarefree monomials $x_{R}$ with $∣ R ∣ = s$ equal $1$ (their index sets must lie inside the $t$ coordinates equal to $1$ ); all others equal $0$ . Therefore the average of each degree- $s$ monomial at $x$ is $(\binom{t}{s}) / (\binom{N}{s}) = (t)_{s} / (N)_{s}$ , where $(t)_{s} = t (t - 1) \dots (t - s + 1)$ and $(t)_{0} = 1$ . The denominator $(N)_{s}$ is nonzero for $s \leq N$ by [F4]. Thus $\overset{ˉ}{p} (x) = q (∣ x ∣)$ for the univariate polynomial $q (t) = \sum_{S} c_{S} (t)_{∣ S ∣} / (N)_{∣ S ∣}$ , with the $s = 0$ term interpreted as $1$ . Each summand has degree $∣ S ∣ \leq d$ , so $\deg q \leq d$ . By step 2.1 it retains the approximation bound on $D$ .

Depends on

Used by

Dependency tree · two levels

28 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

Andrew M. Childs, Lecture Notes on Quantum Algorithms (2025), §21.4 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes (arXiv:1907.09415), §11.2 (standard reference, not scraped)