Exercise PLAN-516

Grover search is an odd Chebyshev singular value transformation of the scalar 1/sqrt(N): the flagged odd iterate is T_{2k+1}(a) times the uniform-to-marked map, equal to (-1)^k sine of (2k+1) half-angles, matching the Grover amplitude up to a global phase.

1. The uniform-marked overlap gives the encoded scalar a = 1/sqrt(N) = sine of the half-angle.
2. The flagged odd iterate equals T_{2k+1}(a) times (marked)(uniform adjoint).
3. The special-argument identity turns T_{2k+1}(a) into (-1)^k sine of (2k+1) half-angles.
4. The magnitude is the Grover success amplitude after k iterations.
5. Letting this sine approach one recovers k of order sqrt(N).
6. The qubitization iterate is minus the standard Grover iterate, giving a global phase (-1)^k.

The encoded operator is the one-by-one scalar a = sine of the half-angle = one over the square root of N, since the overlap of the uniform state with the marked state is a. The flagged odd iterate assembles, by the qubitization-beyond-the-basis construction, into the first-kind Chebyshev polynomial of odd order evaluated at the singular value a, acting as the rank-one operator sending the uniform state to the marked state: the output projector times the accessing unitary times the odd iterate between the two projectors equals T_{2k+1}(a) times (marked state)(uniform state adjoint). This is because the two-reflection iterate is a rotation whose (2k+1)-fold application produces, on the one-dimensional flagged overlap, exactly the odd Chebyshev amplitude, and the surrounding projectors extract the marked-from-uniform rank-one component. Now use the special-argument identity: for a in the interval from zero to one, the odd first-kind Chebyshev value T_{2k+1}(a) equals (minus one) to the k times the sine of (2k+1) times the arcsine of a. Since the arcsine of a is the half-angle, this is (minus one) to the k times the sine of (2k+1) half-angles. The magnitude of the flagged amplitude is therefore the absolute value of the sine of (2k+1) half-angles, which is exactly the Grover success amplitude for measuring the marked state after k iterations; letting the sine of (2k+1) half-angles approach one recovers the Grover query complexity (k of order the square root of N). The only difference from the standard Grover iterate is the sign (minus one) to the k: the qubitization iterate (reflection about uniform composed with the negated marked reflection) equals minus the standard Grover iterate, so its k-th power carries the global phase (minus one) to the k, which does not affect measurement probabilities. Hence Grover search is literally an odd Chebyshev singular value transformation of the scalar a, up to a measurement-irrelevant global phase.

1. States the encoded scalar is a = 1/sqrt(N) = sine of the half-angle, as the uniform-marked overlap (1 weight)
2. Establishes the flagged odd iterate equals T_{2k+1}(a) times the rank-one map from uniform to marked state (1 weight)
3. Applies the identity T_{2k+1}(a) = (-1)^k sine of (2k+1) arcsine(a) to recover the Grover success amplitude (1 weight)
4. Identifies the global phase (-1)^k relating this iterate to minus the standard Grover iterate, noting it is measurement-irrelevant (1 weight)

No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

Read the Lean track and existing diagnostic warmups

• website/research/sources.json

  lin-wiebe-2026-qasc

  Source SHA-256: 9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae · MIT metadata only
• Primary source

Contract: 8d28311cfe3fb9a671acd4693cf06c734bea72c058c9a50c349012ef138ca09f

Item digest: d16b9b79662aed1cc9a0d4dbaf86e932a72fa15e988bfa6581425efd1b448e4a

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 6. This is not measured graph distance or model difficulty.