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

Hadamard character sum on F_2^n

Statement

For $n \geq 1$ and $z \in {0, 1}^{n}$ , with the binary dot product of Binary dot product as parity,

\sum_{x \in {0, 1}^{n}} (- 1)^{x \cdot z} = {\begin{cases} 2^{n}, & z = 0^{n}, \\ 0, & z \neq 0^{n} . \end{cases}

Consequently, for every $x \in {0, 1}^{n}$ ,

H^{\otimes n} ∣ x ⟩ = 2^{- n / 2} \sum_{y \in {0, 1}^{n}} (- 1)^{x \cdot y} ∣ y ⟩,

where $H$ is the exact one-qubit gate of Exact one-qubit gates and rotations and tensor factors follow the ordered register convention of Ordered tensor registers, their inner product, and wire permutations.

Facts & Assumptions

Given: An integer $n \geq 1$ and binary strings $x, z \in {0, 1}^{n}$ .

[F1]

Binary dot product as parity: $x \cdot z$ is the parity $⨁_{i < n} (x_{i} \land z_{i})$ , a bit.

[F2]

Exact one-qubit gates and rotations: in the ordered basis $(∣ 0 ⟩, ∣ 1 ⟩)$ , $H = 2^{- 1 / 2} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array})$ .

[F3]

Finite registers and their ordered computational bases and Big-endian encoding of ordered bit strings: the $n$ -qubit basis is the ordered product basis indexed by bit strings in lexicographic order, with the first wire most significant.

[F4]

Ordered tensor registers, their inner product, and wire permutations: the tensor register keeps its displayed factor order and has the product inner product on elementary tensors.

[F5]

Tensor products of finitely many linear maps: $H^{\otimes n}$ sends an elementary tensor $v_{0} \otimes \dots \otimes v_{n - 1}$ to $H v_{0} \otimes \dots \otimes H v_{n - 1}$ .

[F6]

Dirac Notation Conversion: $∣ v ⟩$ denotes the vector $v$ in the finite-dimensional register.

Proof

1.1givenF1algebra

By [F1], $(- 1)^{x \cdot z} = \prod_{i < n} (- 1)^{x_{i} z_{i}}$ , since the exponent parity is the sum of the coordinate products modulo two. Distributivity over the finite Cartesian product gives $\sum_{x \in {0, 1}^{n}} (- 1)^{x \cdot z} = \prod_{i < n} (1 + (- 1)^{z_{i}}) .$ Each factor is $2$ when $z_{i} = 0$ and $0$ when $z_{i} = 1$ . Thus the product is $2^{n}$ when all coordinates of $z$ vanish and is $0$ otherwise.

2.1givenF1F2F3F4F5F6algebra∎

By [F2], on each factor $H ∣ x_{i} ⟩ = 2^{- 1 / 2} \sum_{y_{i} \in {0, 1}} (- 1)^{x_{i} y_{i}} ∣ y_{i} ⟩$ . Applying [F5] to the ordered product basis [F3] gives a coefficient $2^{- n / 2} \prod_{i < n} (- 1)^{x_{i} y_{i}} = 2^{- n / 2} (- 1)^{x \cdot y}$ at $∣ y ⟩$ , by [F1]. Summing these coefficients proves the tensor-Hadamard formula in the Statement.

Depends on

Used by

One Simon Fourier-sampling sample Algorithm
One-query Bernstein–Vazirani algorithm Algorithm
One-query Deutsch algorithm Algorithm
One-query Deutsch–Jozsa algorithm Algorithm
Deutsch, Deutsch–Jozsa and Bernstein–Vazirani examples Example
Bernstein–Vazirani algorithm returns the secret exactly Theorem
Deutsch–Jozsa algorithm is exact Theorem
Simon query and output measurement produce a coset pair Theorem
Simon samples uniformly from s-perp Theorem

Dependency tree · two levels

36 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 (2026-08-27) (standard reference, not scraped)
John Preskill, Quantum Information, Chapter 6: Quantum Algorithms (updated November 2020) (standard reference, not scraped)