State Preparation
Exercise SP-001
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- a and b are arbitrary real sibling amplitudes; the claim concerns one binary split, not the whole recursive loader
- the real Y-rotation convention is the standard orthogonal rotation used by the library backend
- wires are little-endian; the split acts on one new highest wire
- the pair norm is the Euclidean length sqrt(a^2 + b^2) and the all-zero pair is assigned angle zero
Question
In the low-wire-first recursive loader for a finite real amplitude table, each binary split of a sibling pair of real amplitudes (a, b) is realised by a single uniformly-controlled real Y-rotation. The rotation angle is twice a signed polar angle: its magnitude is the inverse cosine of a divided by the pair norm sqrt(a^2 + b^2), and its sign is taken from the sign of b (with the all-zero pair assigned angle zero). Explain the role of the sign branch, and why using the bare inverse-cosine magnitude alone would fail for a general real amplitude table.
Hint: mathematical route
Why the per-split rotation angle carries the sign of the second sibling amplitude, so negative real amplitudes are reproduced exactly rather than as magnitudes.
- A real Y-rotation by phi sends the zero column to (r*cos(phi/2), r*sin(phi/2)); with phi/2 = arccos(a/r) the first entry times r is exactly a.
- The second entry equals r*sin(arccos(a/r)) = |b|, nonnegative because arccos lands in [0, pi]; a bare magnitude angle therefore mis-signs negative children.
- Negating the half-angle when b < 0 flips the lower entry to -|b| = b, so the signed pair is recovered exactly for all real a, b, with the zero pair carrying angle zero.
Reference solution
The sibling pair (a, b) lies on a circle of radius r = sqrt(a^2 + b^2). A real Y-rotation by angle phi sends the all-zero column to (r*cos(phi/2), r*sin(phi/2)). Choosing phi/2 = arccos(a/r) reproduces the first child exactly, since r*cos(arccos(a/r)) = a (valid because a/r lies in [-1, 1] when r > 0). The second entry is then r*sin(arccos(a/r)) = sqrt(r^2 - a^2) = sqrt(b^2) = |b|, which is nonnegative because arccos lands in [0, pi] where sine is nonnegative. So the bare magnitude reproduces b only when b >= 0; for a table with a negative amplitude below a split it would emit |b| and silently drop the sign. The sign branch repairs this: when b < 0 the half-angle is negated, flipping the lower entry to r*sin(-arccos(a/r)) = -|b| = b. The all-zero pair (r = 0) carries no direction and is assigned angle zero. Thus the signed polar angle recovers the full signed real pair with exact real angles, avoiding a numerically unverified atan2 primitive.
Assessment rubric
- States that a real Y-rotation sends the zero column to (r*cos(phi/2), r*sin(phi/2)) with r the pair norm, and that the inverse-cosine magnitude recovers the first child a exactly. (1 weight)
- Explains that the bare inverse-cosine magnitude yields only |b| (nonnegative) for the second child, because arccos ranges over [0, pi] with nonnegative sine. (1 weight)
- Identifies the sign branch (negating the half-angle when b < 0) as the mechanism that flips the lower entry to the correct negative value, so general signed tables are handled. (1 weight)
- Notes the zero-pair angle-zero convention and that the angles are exact real expressions (no atan2), without claiming a gate-count or whole-circuit result. (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
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.
Sources and provenance
- QuantumBlockEncoding/RealAmplitudePreparation.lean
lines 150-201: noncomputable def splitAngle (a b : R) : ExactAngle := if pairNorm a b = 0 then .rational 0 else .real (2 * if b < 0 then -Real.arccos (a / pairNorm a b) else Real.arccos (a / pairNorm a b)); and theorem splitAngle_firstColumn (a b : R) (v : Fin 2) : standardRyMatrix (splitAngle a b).eval v 0 * (pairNorm a b : C) = if v = 0 then (a : C) else (b : C)
Source SHA-256:a6ded7e65a7e42d5724529befb48eefc9505814136206dd96248fb59b3c45efa· MIT (repository LICENSE)
Contract: 3aa3ae1877e9622fa4b4104d9778f05b18878079aa9728d7e81624002f02d1ba
Item digest: 0131ad1ec8cff86035bb3b2ac0369a3fda6efe1bb41e47ed0f2a41355733e4ce
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.