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

Binary dot product as parity

Definition

For $n \geq 0$ and $a, x \in {0, 1}^{n}$ , define the one-bit binary dot product

a \cdot x : = ⨁_{i = 0}^{n - 1} (a_{i} \land x_{i}),

where $\land$ is Boolean conjunction and $⨁$ is the left-to-right fold of XOR, with empty fold $0$ . It is the parity of the number of coordinates where both bits are $1$ . Under the quotient operations of Binary residue carrier and operations, this bit represents the sum $\sum_{i = 0}^{n - 1} [a_{i}]_{2} [x_{i}]_{2}$ in $Z / 2 Z$ ; the equality uses only the operation definitions, not the field axioms.

Facts & Assumptions

Given: A length- $n$ pair of binary strings $a, x$ , where $n$ may be zero.

[F1]

Input encoding and size for algorithmic tasks: bit strings are the specified finite binary encodings, and their length fixes the width $n$ .

[F2]

Binary residue carrier and operations: the two classes $[0]_{2}, [1]_{2}$ have quotient addition and multiplication; their addition table is XOR and their multiplication table is Boolean conjunction.

[F3]

The congruence class $[a]_{n}$ and the quotient set $Z / n$ : the carrier $Z / 2 Z$ consists of the residue classes modulo $2$ .

[F4]

Addition and multiplication on $Z / n$ by $[a]_{n} + [b]_{n} = [a + b]_{n}$ and $[a]_{n} [b]_{n} = [a b]_{n}$ : the quotient operations are induced by integer addition and multiplication on representatives.

Verification

technique · induction on the number of processed coordinates

1.1givenF1F2F3F4algebra

For bits $u, v \in {0, 1}$ , the four cases give $u \land v = u v$ . Thus $[a_{i} \land x_{i}]_{2} = [a_{i}]_{2} [x_{i}]_{2}$ for each coordinate by [F2] and [F4].

2.1givenF2F4step 1.1baseihalgebra

Let $p_{0} = 0$ and $p_{k + 1} = p_{k} \oplus (a_{k} \land x_{k})$ for $0 \leq k < n$ . The base case has $[p_{0}]_{2} = [0]_{2}$ , the empty sum. If $[p_{k}]_{2}$ is the left-to-right sum of the first $k$ coordinate products, the addition table in [F2] and the coordinate identity in step 1.1 give $[p_{k + 1}]_{2} = [p_{k}]_{2} + [a_{k}]_{2} [x_{k}]_{2}$ . Hence the identity holds at every $k \leq n$ by finite induction, including $n = 0$ .

3.1givenF2step 2.1discharge-induction∎

At $k = n$ , $p_{n}$ is the defined XOR fold $a \cdot x$ , so step 2.1 proves that its residue class is the sum of the coordinate products in the quotient operations. No field axiom is used.

Depends on

Used by

Reversible binary dot-product query Algorithm
Bernstein–Vazirani no-offset promise Definition
Deutsch, Deutsch–Jozsa and Bernstein–Vazirani examples Example
Finite Simon rank and sampling examples Example
Oracle conversion and uncomputation examples Example
Hadamard character sum on F₂ⁿ Lemma
The Simon annihilator is an (n−1)-dimensional binary subspace Lemma
Bernstein–Vazirani algorithm returns the secret exactly Theorem
Classical Bernstein–Vazirani needs n queries for bounded error Theorem
F2 row reduction returns the unique Simon mask Theorem
Reversible binary dot product: correctness and exact cost Theorem
Simon samples uniformly from s-perp Theorem

Dependency tree · two levels

11 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)
Andrew M. Childs, Lecture Notes on Quantum Algorithms (17 April 2025) (standard reference, not scraped)