LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Unnormalized branch density entries have degree at most twice the query count

Statement

Let $A$ be a local bit-query algorithm, allowing finite input-independent instrument branches, and let $h$ be any execution history containing $t (h)$ oracle calls. Write $σ_{h} (x) : = w_{h} (x) ρ_{h} (x)$ for the unnormalized branch operator: $w_{h}$ is the probability weight of the history and $ρ_{h}$ its conditional density operator when $w_{h} > 0$ ; set $σ_{h} = 0$ when $w_{h} = 0$ . In the fixed computational basis, every matrix entry of $σ_{h} (x)$ on $x \in {0, 1}^{N}$ is represented by a complex polynomial whose support has no monomial of total degree greater than $2 t (h)$ .

Facts & Assumptions

Given: A finite local bit-query execution tree, its fixed finite register, a history $h$ , and the input $x \in {0, 1}^{N}$ .

[F1]

Oracle-only bit-query algorithm: the root state is fixed independently of $x$ ; every non-oracle map is fixed and linear; query nodes use only the specified one-hot bit XOR oracle.

[F2]

Normalized output law for finite quantum query branches: unitary edges update conditional states by $ρ \mapsto U ρ U^{†}$ without changing weight; an instrument outcome $a$ has weight factor $q_{a} = tr (I_{a} (ρ))$ and conditional state $I_{a} (ρ) / q_{a}$ when $q_{a} > 0$ .

[F3]

Standard bit-flip query convention and Finite registers and their ordered computational bases: on basis states the query is the XOR permutation $(a, b, w) \mapsto (a, b \oplus g_{x} (a), w)$ ; a basis is fixed and finite.

[F4]

Polynomial rings in finitely many commuting indeterminates by iteration and Monomials, coefficients, degree in each variable and total degree in $F [x_{1}, \dots, x_{n}]$ : finite sums and products of polynomial entries have the usual coefficientwise degree bounds.

[F5]

$C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ : all matrix entries and the fixed linear maps use finite complex addition and multiplication.

[F6]

Finite instruments and conditional states and Completely positive maps: an instrument outcome is a complex-linear completely positive map and therefore sends a density operator to a nonnegative operator; The basis-independent trace of an endomorphism of a finite-dimensional vector space defines its trace, and A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S diagonalizes a nonnegative finite-dimensional operator with nonnegative eigenvalues.

Proof

1.1givenF1base

At the root, the branch weight is one and the state is the fixed all-zero basis-state projector, so every entry of $σ_{\emptyset}$ is constant and has no supported monomial above degree zero.

1.2ih

Induction hypothesis: at a history $h$ with $t (h)$ queries, each entry of $σ_{h} (x)$ has no supported monomial of degree greater than $2 t (h)$ .

2.1givenF1F2F5F6step 1.2algebra

On a fixed unitary edge, multiplying the branch weight into the conditional-state update gives $σ_{h^{'}} = U σ_{h} U^{†}$ , a fixed linear map on entries, so the support degree does not increase and the query count remains $t (h)$ . At instrument outcome $a$ of a positive-weight history, if $q_{a} > 0$ , then $σ_{h a} = w_{h} q_{a} (I_{a} (ρ_{h}) / q_{a}) = I_{a} (σ_{h})$ . If $q_{a} = 0$ , [F6] makes $I_{a} (ρ_{h})$ nonnegative with trace zero; its nonnegative eigenvalues sum to zero, so the operator is zero and $σ_{h a} = 0 = I_{a} (σ_{h})$ . A zero-weight parent also maps to zero by linearity. Since all non-oracle maps are fixed independently of $x$ by [F1], every such instrument branch is a fixed linear map on entries and preserves the support degree bound in [step 1.2].

2.2F3F4F5step 1.2algebra

At an oracle node, the matrix entries of $U_{g_{x}}$ in the computational basis are constants, $x_{i}$ , or $1 - x_{i}$ : a one-hot address $e_{i}$ toggles the target exactly when $x_{i} = 1$ , and every other address leaves it unchanged. The same holds for $U_{g_{x}}^{†}$ , which equals $U_{g_{x}}$ because an XOR query is an involution. Therefore each entry of $U_{g_{x}} σ_{h} U_{g_{x}}^{†}$ is a finite sum of products of one affine entry, one entry with support degree at most $2 t (h)$ from [step 1.2], and one affine entry. By [F4]–[F5] its support degree is at most $2 t (h) + 2$ , and the new history has $t (h) + 1$ queries.

3.1F1step 1.1step 1.2step 2.1step 2.2ihdischarge-induction∎

Induct on the finite execution-tree depth from [F1]. Step 1.1 proves the root case. At each successor edge, step 2.1 preserves the degree bound when the query count is unchanged, and step 2.2 raises its upper bound by exactly two when a query is added. Therefore every history $h$ satisfies the claimed support degree bound $2 t (h)$ ; zero-weight histories satisfy it because all their entries are zero.

Depends on

Used by

A T-query bit algorithm has an acceptance polynomial of degree at most 2T Theorem

Dependency tree · two levels

66 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.3 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes (arXiv:1907.09415), §11.2 (standard reference, not scraped)