LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generated

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.

Discarding the hiding register yields a coset-state mixture

Statement

Let $G$ be finite abelian, $H \leq G$ , $N = ∣ G ∣$ , and $h = ∣ H ∣$ . Write $C_{H} : = {g + H : g \in G}$ for the set of distinct additive cosets, where $g + H : = {g + h^{'} : h^{'} \in H}$ . Start with the uniform group state, evaluate an exact hiding oracle into a fresh output register, then discard that register. On the group register the resulting density matrix is $ρ_{G} = \frac{h}{N} \sum_{C \in C_{H}} ∣ C ⟩ ⟨ C ∣, ∣ C ⟩ : = h^{- 1 / 2} \sum_{g \in C} ∣ g ⟩ .$ Thus it is the uniform mixture of one normalized coset state for each distinct coset.

Facts & Assumptions

Given: A finite abelian group $G$ , a subgroup $H \leq G$ , an exact hiding function $F$ satisfying the promise in Finite abelian hidden-subgroup promise and output encoding, and the coherent XOR action in Coherent XOR function oracle.

[F1]

The hiding promise is $F (g) = F (g^{'})$ exactly when $g - g^{'} \in H$ . (Finite abelian hidden-subgroup promise and output encoding)

[F2]

On a valid group code $x = {code}_{G} (g)$ , the total Boolean extension equals $η (F (g))$ ; its XOR oracle maps $∣ x, y ⟩$ to $∣ x, y \oplus η (F (g)) ⟩$ . (Finite abelian hidden-subgroup promise and output encoding, Coherent XOR function oracle)

[L1]

The partial trace over the output register contracts equal output-basis indices and sums them, in the declared register order. (Partial trace over a finite tensor factor)

[F3]

The group and output registers are ordered tensor products of $Q_{2}$ factors (Finite registers and their ordered computational bases). Each factor's computational basis is orthonormal (The computational basis is orthonormal); the tensor-register inner product is the product of the factor inner products (Ordered tensor registers, their inner product, and wire permutations), so the lexicographic product computational basis is orthonormal by the factor-basis theorem (The product basis is orthonormal and tensor dimensions multiply). This includes either empty register.

[F4]

A density operator is a nonnegative endomorphism of trace one, and nonnegativity requires self-adjointness and a nonnegative quadratic form. (Density operator, Non-negative and positive operators)

[F5]

In a fixed ordered basis, the endomorphism trace is the finite sum of diagonal entries of its coordinate matrix; the coordinate matrix of a finite sum is the corresponding sum of matrices, so matrix-trace linearity gives trace linearity for the finite sums used here. (The basis-independent trace of an endomorphism of a finite-dimensional vector space, Trace is a linear functional on $M_{n} (F)$ )

[F6]

The rank-one operator $∣ x ⟩ ⟨ y ∣$ sends $v$ to $⟨ v, y ⟩_{r o o t} x$ . (Dirac Notation Conversion)

Proof

1.1givenF1F2F3L1algebra

Write $N = ∣ G ∣$ and $h = ∣ H ∣$ . The oracle output on the initial state is $∣ Ψ ⟩ = N^{- 1 / 2} \sum_{g \in G} ∣ {code}_{G} (g) ⟩ ∣ η (F (g)) ⟩$ . The unreduced density matrix has terms $N^{- 1} ∣ {code}_{G} (g) ⟩ ⟨ {code}_{G} (g^{'}) ∣ \otimes ∣ η (F (g)) ⟩ ⟨ η (F (g^{'})) ∣$ . By [L1] and output-register orthonormality [F3], tracing out the second register retains exactly the pairs with $η (F (g)) = η (F (g^{'}))$ . Injectivity of $η$ in [F2] makes this equivalent to $F (g) = F (g^{'})$ .

2.1F1F3F5F6step 1.1construct

By [F1], the retained pairs are exactly those lying in a common coset $C \in G / H$ . Translation gives $∣ C ∣ = h$ . By [F3], the vectors $∣ g ⟩$ are orthonormal, so $⟨ C, C ⟩ = h^{- 1} \sum_{g, g^{'} \in C} ⟨ g, g^{'} ⟩ = 1$ for $∣ C ⟩ : = h^{- 1 / 2} \sum_{g \in C} ∣ g ⟩$ . Hence $ρ_{G} = N^{- 1} \sum_{C \in G / H} \sum_{g, g^{'} \in C} ∣ g ⟩ ⟨ g^{'} ∣$ . The rank-one matrix $∣ C ⟩ ⟨ C ∣$ has diagonal entries $1 / h$ on the $h$ labels in $C$ and zero elsewhere, so its trace is $1$ by [F5]. Put $P_{C} : = ∣ C ⟩ ⟨ C ∣$ . By [F6], $P_{C} v = ⟨ v, C ⟩_{r o o t} ∣ C ⟩$ , and for all $u, v$ the root pairing gives $⟨ P_{C} u, v ⟩_{r o o t} = ⟨ u, C ⟩_{r o o t} ⟨ C, v ⟩_{r o o t} = ⟨ u, P_{C} v ⟩_{r o o t}$ . Thus $P_{C}$ is self-adjoint. Also $⟨ ∣ C ⟩ ⟨ C ∣ v, v ⟩_{r o o t} = ∣ ⟨ v, C ⟩_{r o o t} ∣^{2} \geq 0$ . Therefore $∣ C ⟩ ⟨ C ∣ = h^{- 1} \sum_{g, g^{'} \in C} ∣ g ⟩ ⟨ g^{'} ∣$ .

3.1F4F5step 2.1algebra∎

Substitution gives $ρ_{G} = (h / N) \sum_{C \in G / H} ∣ C ⟩ ⟨ C ∣$ . The real positive weighted sum of the self-adjoint summands in step 2.1 is self-adjoint, and its quadratic form is the corresponding weighted sum of nonnegative quadratic forms. Thus $ρ_{G}$ is nonnegative by [F4]. The cosets partition the $N$ group elements into blocks of size $h$ , so there are $N / h$ distinct cosets and the weights sum to $(h / N) (N / h) = 1$ . By trace linearity [F5] and the unit trace of each summand, $tr (ρ_{G}) = 1$ . Thus [F4] makes $ρ_{G}$ a density operator, and the formula is the uniform mixture over distinct cosets.

Remarks

The proof uses discard/partial trace. It does not replace discarding by a measured output; a separate measurement branch is unnecessary for this reduced-state identity.

Depends on

Used by

Fourier samples are uniform in the annihilator Theorem

Dependency tree · two levels

56 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 (17 April 2025) (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)