TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Simon query and output measurement produce a coset pair

Statement

For a Simon oracle with hidden nonzero string $s$ , immediately after its one standard query the joint state is

$2^{- n / 2} \sum_{x \in {0, 1}^{n}} ∣ x ⟩ ∣ f (x) ⟩ .$

For each output value $v$ in the image of $f$ , the target Lüders instrument has probability $2^{1 - n}$ and its conditional joint state factors as

$\frac{∣ x_{0} ⟩ + ∣ x_{0} \oplus s ⟩}{\sqrt{2}} \otimes ∣ v ⟩,$

where $x_{0}$ is either preimage of $v$ . Outcomes outside the image have probability zero. Hence the address register conditional state is the normalized coset-pair vector shown above.

Facts & Assumptions

Given: A Simon oracle with $n \geq 1$ , $m \geq n - 1$ , and unique nonzero hidden string $s$ .

[F1]

Simon hidden-XOR-period promise: every fiber is exactly one pair ${x, x \oplus s}$ , and $s \neq 0$ .

[F2]

Standard bit-flip query convention: the ordinary oracle acts by $U_{f} ∣ x ⟩ ∣ z ⟩ = ∣ x ⟩ ∣ z \oplus f (x) ⟩$ on the ordered address and target bases.

[F3]

One Simon Fourier-sampling sample: the address is prepared uniformly by $H^{\otimes n}$ , queried once, and the target is measured with the branch maps $X \mapsto P_{v} X P_{v}$ for $P_{v} = I \otimes ∣ v ⟩ ⟨ v ∣$ .

[F4]

Finite projective measurements: a projective measurement is a finite family of pairwise orthogonal self-adjoint idempotents summing to the identity.

[F5]

Finite POVMs and their outcome law: a POVM is a finite family of nonnegative effects summing to the identity.

[F6]

A non-negative operator has a unique non-negative square root: every nonnegative operator has a unique nonnegative square root.

[F7]

The square-root Lüders maps form an instrument: for a finite POVM $(E_{v})$ , the square-root maps $X \mapsto E_{v}^{1 / 2} X E_{v}^{1 / 2}$ form a finite instrument.

[F8]

Finite instruments and conditional states: an instrument assigns branch probability $tr (I_{v} (ρ))$ and, on a positive branch, conditional state $I_{v} (ρ) / tr (I_{v} (ρ))$ .

[F9]

Instrument outcome weights normalize: for an input density operator, the branch weights of a finite instrument are nonnegative and sum to one.

[F10]

Ordered tensor registers, their inner product, and wire permutations: elementary tensor products use the displayed factor order and product inner product.

[F11]

The computational basis is orthonormal: each computational register basis is orthonormal.

[F12]

Dirac Notation Conversion: $∣ w ⟩ ⟨ w ∣$ sends $z$ to $⟨ z, w ⟩_{r o o t} w$ .

[F13]

The basis-independent trace of an endomorphism of a finite-dimensional vector space: trace is the sum of diagonal entries in any finite-dimensional basis.

[F14]

Hadamard character sum on F_2^n: the tensor Hadamard sends $∣ 0^{n} ⟩$ to the uniform vector $2^{- n / 2} \sum_{x} ∣ x ⟩$ .

[F15]

A unit-vector outer product is a density operator: the outer product of a unit vector is a density operator.

Proof

1.1givenF2F3F10F11F14F15algebra

The Hadamard-character formula [F14] gives $H^{\otimes n} ∣ 0^{n} ⟩ = 2^{- n / 2} \sum_{x} ∣ x ⟩$ . Applying [F2] to this vector and the zero target produces the displayed joint vector $Ψ$ . Its $2^{n}$ orthogonal terms all have squared coefficient $2^{- n}$ by [F10]–[F11], so $∥ Ψ ∥ = 1$ and $∣ Ψ ⟩ ⟨ Ψ ∣$ is a density operator by [F15].

1.2givenF3F4F5F6F7F8

For each $v$ , the maps in [F3] have projectors $P_{v}$ . By [F10]–[F11], computational basis vectors are orthonormal, so the $P_{v}$ are self-adjoint idempotents, pairwise orthogonal, and sum to the identity. Also $⟨ P_{v} z, z ⟩ = ⟨ P_{v} z, P_{v} z ⟩ \geq 0$ , so these projectors form a POVM by [F4]–[F5]. The nonnegative square root of each projector is itself by [F6]; hence [F7] makes the branch maps a valid instrument with the probabilities and conditional states of [F8].

1.3givenF1F3F11constructalgebra

Fix $v$ in the image and let $x_{0}$ be one preimage. Set $w_{v} : = 2^{- n / 2} (∣ x_{0} ⟩ + ∣ x_{0} \oplus s ⟩) \otimes ∣ v ⟩$ . The post-query vector projected into branch $v$ is $2^{- n / 2} \sum_{x : f (x) = v} ∣ x ⟩ ∣ v ⟩ = w_{v}$ by [F1]. The two address basis vectors are distinct and orthonormal by [F1] and [F11].

2.1givenF3F12F13step 1.3algebra

The branch operator is the rank-one map $∣ w_{v} ⟩ ⟨ w_{v} ∣$ for the projected vector $w_{v}$ in step 1.3. In the product basis its only nonzero diagonal entries are the two squared coefficients $2^{- n}$ , by [F12]–[F13]. Thus the branch probability is $tr (∣ w_{v} ⟩ ⟨ w_{v} ∣) = 2^{1 - n}$ . An output outside the image has zero projected vector and therefore zero trace.

3.1givenF1F8F9F15step 1.3step 2.1algebra∎

Dividing the projected vector in step 1.3 by its norm $2^{(1 - n) / 2}$ gives the normalized conditional state in the Statement; it factors into an address vector and the fixed output basis vector $∣ v ⟩$ . Its rank-one outer product is a density operator by [F15], and its probability is positive, so it is the conditional state in [F8]. There are exactly $2^{n - 1}$ image values by the fiber partition in [F1], and their probabilities sum to one as required by [F9].

Depends on

Used by

Finite Simon rank and sampling examples Example
Simon samples uniformly from s-perp Theorem

Dependency tree · two levels

62 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) (standard reference, not scraped)
John Preskill, Quantum Information, Chapter 6: Quantum Algorithms (updated November 2020) (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms (17 April 2025) (standard reference, not scraped)