LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Hadamard preparation of a uniform binary state

Statement

For an integer $n \geq 0$ , give each factor of the ordered register $V_{n} = (C^{2})^{\otimes n}$ the basis $(e_{0}, e_{1})$ and define the one-qubit matrix $H : = \frac{1}{\sqrt{2}} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array}) .$ Then $H$ is unitary and $H^{\otimes n} e_{0^{n}} = 2^{- n / 2} \sum_{x \in {0, 1}^{n}} e_{x} .$ For $n = 0$ , the tensor product is $C$ , the empty word is the sole basis label, and $H^{\otimes 0}$ is the identity. The preparation uses exactly $n$ one-qubit $H$ gates when $H$ is primitive in the declared circuit model; otherwise its implementation and synthesis costs must be supplied there.

Facts & Assumptions

Given: $n \geq 0$ , the ordered computational register, and the stated matrix $H$ .

[F1]

Finite registers and their ordered computational bases: a qubit has ordered basis $(e_{0}, e_{1})$ , and $e_{0^{n}}$ denotes the corresponding register basis vector.

[F2]

Ordered tensor registers, their inner product, and wire permutations: tensor-register basis vectors are ordered products of the factor bases; the empty tensor product is $C$ .

[F3]

The computational basis is orthonormal: the ordered computational basis is orthonormal.

[F4]

Circuit-family and computation cost model: a circuit gate count counts its finite one- and multi-qubit gate instances, separately from oracle-query and circuit-description costs.

[F5]

Tensor products of finitely many linear maps: the tensor map is the unique linear map that acts factorwise on elementary tensors, with the empty tensor map equal to the identity on $C$ .

Proof

technique · direct

1.1givenF1F3algebra

Direct multiplication gives $H^{*} H = I_{2}$ . Also $H e_{0} = (e_{0} + e_{1}) / \sqrt{2}$ , so $H$ is a unitary one-qubit operation in the specified basis.

1.2F1F2F3F5algebra

By the tensor-map rule [F5], $H^{\otimes n} e_{0^{n}} = (H e_{0})^{\otimes n} = 2^{- n / 2} (e_{0} + e_{1})^{\otimes n} = 2^{- n / 2} \sum_{x \in {0, 1}^{n}} e_{x} .$ The last equality distributes the finite tensor product over its two-term factors, choosing exactly one of $e_{0}, e_{1}$ at each position; the ordered product basis in [F2] identifies these choices with the binary words $x$ . For $n = 0$ , both sides are the scalar $1$ in $C$ , the empty sum-index set convention gives its single empty word, and [F5] makes the empty tensor map the identity. The basis vectors are distinct orthonormal vectors by [F3], so the right side has norm one.

2.1givenF4F5algebra∎

By [F5], the construction applies one copy of $H$ to each of the $n$ tensor factors and no oracle operation. It therefore has $n$ one-qubit gate instances when $H$ is primitive, as counted by [F4]; if it is not primitive, the declared synthesis cost is required. At $n = 0$ the circuit has no gates.

Depends on

Used by

Complete-graph continuous-time search Algorithm
Hypercube continuous-time state transfer Algorithm
Complete-graph search matrix and gap Example
Continuous-time walk resource accounting Theorem

Dependency tree · two levels

25 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

Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)