Angle Approximation

Exercise LA-015

intermediate · proof · test_public

nl bridge from inspected source. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

Finite-dimensional complex Hilbert spaces unless real amplitudes are explicitly specified
All basis/register permutations are fixed and applied to both input and output

Column-vector action; Euclidean induced operator norm for norm claims
Source inspection only; no fresh formal verification

Question

Define R(theta)=[[cos(theta/2),-sin(theta/2)],[sin(theta/2),cos(theta/2)]]. Derive the exact operator distance between R(a) and R(b), and prove it is at most |a-b|/2. Why does adding any number of untouched spectator qubits not multiply the distance by a dimension factor?

Hint: mathematical route

Use sum-difference identities to factor the difference by a unitary.
Take scalar-times-unitary norm to obtain the exact sine expression.
Apply sine Lipschitz bound; spectator lift remains unitary.

Reference solution

Trigonometric sum-difference formulas factor R(a)-R(b)=2 sin((a-b)/4) R((a+b)/2+pi). The second factor is unitary, so its induced Euclidean operator norm is1, giving exactly 2|sin((a-b)/4)|. Since |sin x|<=|x|, the distance is <=|a-b|/2. Adding identity spectators, with any fixed wire placement, tensors the difference with an identity and conjugates by a permutation. The identity has norm1 and unitary conjugation preserves the norm; hence the same scalar-times-unitary factorization has no dimension multiplier. This is uniform operator error, not entrywise error or a finite-bit synthesis algorithm.

Assessment rubric

Exact quarter-angle sine formula (1 weight)
Correct linear bound factor1/2 (1 weight)
Explain dimension independence in induced norm (1 weight)

Graph-grounded prerequisites

These are support/source anchors, not an automatically extracted theorem-dependency proof.

Download the shared core registry

Lean view and evidence boundary

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

Sources and provenance

QuantumBlockEncoding/PrimitiveRyPerturbation.lean
difference_factor28-37; liftedRy factor54-59; distance61-79
Source SHA-256: 57ad888af7a81ac5067f6655160fecf1f197a91b0414bc5e510786b9eed27e32 · MIT (repository LICENSE)

Contract: bc4e15074deae045466bc02c4ce3414069aec77ee27c77e71a0bee2be453b5df

Item digest: 4ac0d74781d50ead023fd5830a7e8e5cda93b4580d32f2f4ef85299e32890567

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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