Alphabeta Math
LemmaStatement: 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.

Fourier sample from a generalized-dihedral reflection coset state

Statement

Write A=Z/NZ additively, N≥2, and identify its generalized-dihedral group with A×Z/2Z under

(a,b)(a′,b′)=(a+(−1)ba′, b+b′ mod 2).

Let Hs={(0,0),(s,1)} and let a total encoded function F be constant on each left coset of Hs and distinct on different left cosets. Start in the uniform state on the 2N group elements, evaluate the coherent XOR oracle for F into a zero output register, discard that register, apply the positive-sign QFT⁡N to the first coordinate, and measure that coordinate. The measured k∈Z/NZ is uniform. Conditional on k, the remaining qubit is, up to a global phase,

∣ψk⟩=∣0⟩+exp⁡(2πiks/N)∣1⟩2.

The coordinate readout uses the Lüders projective instrument for the projections Πk=∣k⟩⟨k∣⊗I2. The stated conditional qubit is the post-measurement state after discarding the measured coordinate.

Facts & Assumptions

Given: N≥2, s∈Z/NZ, the displayed finite group law, the stated left-coset hiding promise, and the exact finite-register and Fourier operations above.

[F1]

The generalized dihedral group is the external semidirect product by the inversion action; its multiplication is (a,b)(a′,b′)=(a+(−1)ba′,b+b′), and this multiplication defines a group ( The generalized dihedral group Dih⁡(A)=A⋊C2 for an abelian group A, The external semidirect product N⋊αH, The semidirect-product multiplication makes N×H a group).

[F2]

A coherent XOR oracle acts on the ordered basis as ∣x,y⟩↦∣x,y⊕F(x)⟩ (Coherent XOR function oracle).

[F3]

Discarding the second factor is the partial trace, which contracts equal basis indices and sums them (Partial trace over a finite tensor factor).

[F4]

The finite computational bases are orthonormal and ordered tensor factors retain their declared order (The computational basis is orthonormal, Finite registers and their ordered computational bases, Ordered tensor registers, their inner product, and wire permutations).

[F5]

The cyclic Fourier transform has matrix action ∣a⟩↦N−1/2∑k=0N−1exp⁡(2πiak/N)∣k⟩ (Positive-sign cyclic quantum Fourier transform).

[F6]

A projective-measurement outcome has weight tr⁡(ρPk) (Finite projective measurements, Projective measurement outcome weights are probabilities).

[F7]

A rank-one operator ∣x⟩⟨y∣ acts by z↦⟨z,y⟩rootx (Dirac Notation Conversion).

[F8]

The circuit denotation composes the declared finite gates in chronological order (Denotational semantics of a finite layered circuit).

[F9]

The coordinate matrix of a rank-one Dirac operator is [x][y]† (Dirac Notation Coordinate Identity).

[F10]

Endomorphism trace is the sum of diagonal entries in an ordered basis (The basis-independent trace of an endomorphism of a finite-dimensional vector space).

[F12]

The complex exponential satisfies exp⁡(z+w)=exp⁡(z)exp⁡(w) (exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential).

[F13]

A finite projective measurement is implemented by the Lüders instrument of its projections: the outcome-k branch is Ik(ρ)=ΠkρΠk, and for pk=tr⁡(ρΠk)>0 its conditional state is ΠkρΠk/pk (Finite POVMs and their outcome law, Finite instruments and conditional states, The square-root Lüders maps form an instrument, A non-negative operator has a unique non-negative square root, Conditional state for a projective measurement, Non-negative and positive operators). The Πk are orthogonal projections summing to the identity, so the same projective-to-POVM and positive-square-root specialization applies to the coordinate-register PVM.

Proof

1.1givenF1algebra

By [F1], (s,1)2=(s−s,0)=(0,0), so Hs has the two displayed elements. Right multiplication gives (a,0)(s,1)=(a+s,1) and (a,1)(s,1)=(a−s,0). Hence the distinct left cosets are Ca={(a,0),(a+s,1)} for a∈A: every group element occurs in one such pair, and the first coordinate of its unique ( ⋅ ,0) representative identifies the pair.

2.1givenF2F3F4F7F8F9F10step 1.1algebra

The initial state has amplitude (2N)−1/2 on each group basis vector. After the oracle call in the declared circuit order [F8], the output basis label is constant on each Ca and distinct for different a. By [F2]–[F4], tracing out the output retains exactly pairs of group labels in the same Ca, so the group-register operator is ρ=12N∑a∈A∑z,z′∈Ca∣z⟩⟨z′∣=1N∑a∈A∣Ca⟩⟨Ca∣, where ∣Ca⟩=(∣a,0⟩+∣a+s,1⟩)/2. Each ∣Ca⟩ is normalized because its two distinct group basis vectors are orthonormal. The rank-one notation is the operator of [F7], with coordinate matrix and trace given by [F9]–[F10].

3.1givenF3F4F5F6F9F10F11F12F13step 2.1algebra∎

Applying [F5] to the first coordinate sends each coset vector to ∣ϕa′⟩=1N∑k=0N−1exp⁡(2πiak/N)∣k⟩⊗∣ψk⟩. The factorization uses [F12]. Let ρ′=1N∑a∣ϕa′⟩⟨ϕa′∣ be the transformed mixture from step 2.1. Under the Lüders branch [F13], Πkρ′Πk=1N2∑a∈A∣k⟩⟨k∣⊗∣ψk⟩⟨ψk∣=1N∣k⟩⟨k∣⊗∣ψk⟩⟨ψk∣. Its trace is 1/N by [F9]–[F11], so every k occurs with that probability. The normalized conditional state on the joint register is ∣k⟩⟨k∣⊗∣ψk⟩⟨ψk∣. Discarding the first coordinate contracts its matching basis index by [F3]; after reordering the factors if needed by [F4], the retained qubit density is ∣ψk⟩⟨ψk∣. Hence the conditional qubit ray is ∣ψk⟩, as claimed.

Depends on

Used by

Dependency tree · two levels

89 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