Oracle Composition
Exercise BE-106
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
- The angle t(x) satisfies cos t(x) = x on -1 <= x <= 1 and is extended in some unspecified way elsewhere
- The clean entry is read as the top-left matrix element
- The amplitude gate is the planar rotation through an inverse-cosine branch of x
- The cosine of any real angle lies in the closed interval [-1, 1]
Question
An amplitude-loading gate is built from a planar rotation through an angle t(x), where t is any fixed real-valued function of the real parameter x chosen so that on the interval -1 <= x <= 1 the cosine of t(x) equals x (an inverse-cosine branch), and extended in some unspecified way to the rest of the real line. Two claims are on the table: (A) the gate is unitary for every real x, with no restriction and independent of how t is extended; (B) the top-left entry of the gate equals x. Decide for which values of x each claim holds. Prove the unconditional claim, prove that claim (B) holds for -1 <= x <= 1, and prove that claim (B) FAILS whenever |x| > 1 without using any particular value of the extension. Explain the asymmetry: why unitarity is free but the clean-entry readout needs -1 <= x <= 1.
Hint: mathematical route
The inverse-cosine amplitude gate is unitary for every real parameter and for any extension of the angle, but its clean-entry readout equals the parameter only on [-1,1]; for |x|>1 the readout cannot equal x because cosine is bounded in [-1,1], proved without guessing the extension.
- The amplitude gate is a planar rotation through the angle t(x) with top row (cos t(x), -sin t(x)).
- Every planar rotation is unitary since cos^2+sin^2=1 for any angle, so the gate is unitary for all real x independent of the extension of t.
- On -1 <= x <= 1 the angle is chosen so cos t(x) = x, so the top-left entry equals x.
- For |x|>1 the cosine of any angle lies in [-1,1] while x lies outside it, so cos t(x) cannot equal x for any extension value.
- Unitarity is structural and hypothesis-free, but the clean-entry readout is a semantic promise valid only where x is a possible cosine, so unitarity does not certify the right amplitude.
Reference solution
The gate is the planar rotation with top row (cos t(x), -sin t(x)) and bottom row (sin t(x), cos t(x)). Claim (A) holds unconditionally. For every real angle, cos^2 + sin^2 = 1, so this matrix is a planar rotation and hence unitary (its two entries lie on the unit circle); this is true whatever real number t(x) happens to be, so unitarity holds for all real x and does not depend on how t is extended outside [-1,1]. Claim (B): the top-left entry equals cos t(x). On the interval -1 <= x <= 1 the angle was chosen so that cos t(x) = x, so the top-left entry equals x exactly and the amplitude is loaded correctly. For |x| > 1 the claim fails, and this can be proved without knowing the extension value: the cosine of any real angle lies in the closed interval [-1, 1], so cos t(x) lies in [-1, 1] for every possible choice of t(x); but |x| > 1 means x lies outside [-1, 1], so cos t(x) cannot equal x. Thus the readout is wrong for every |x| > 1 regardless of how t is extended, and no guess about the extension is needed. The asymmetry is the key point: unitarity is a structural property of the rotation shape (two unit-circle entries for any angle), so it survives even a meaningless input; but the clean-entry readout is a semantic promise that the stored amplitude is exactly x, and a cosine can only ever equal numbers in [-1, 1]. A construction can therefore be perfectly unitary yet load the wrong number: a unitarity certificate must not be mistaken for a certificate that the intended coefficient was loaded.
Assessment rubric
- Prove unitarity holds for all real x because every planar rotation satisfies cos^2+sin^2=1 regardless of the angle, independent of how t is extended (1 weight)
- Prove the top-left entry cos t(x) equals x on -1 <= x <= 1 by the defining choice of the angle (1 weight)
- Prove claim (B) fails for every |x|>1 because the cosine of any angle lies in [-1,1] while x does not, with no appeal to a particular extension value (1 weight)
- Explain the asymmetry: unitarity is structural and free, but the clean-entry readout is a semantic promise a cosine can satisfy only for values in [-1,1] (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/Robin/ComplexLCU.lean
theorem amplitudeRotation_unitary (coefficient : Real) : amplitudeRotation coefficient ∈ _root_.Matrix.unitaryGroup (Fin 2) ℂ := realRotation_unitary _ (lines 93-96); theorem amplitudeRotation_cleanEntry (coefficient : Real) (lower : -1 ≤ coefficient) (upper : coefficient ≤ 1) : amplitudeRotation coefficient 0 0 = (coefficient : ℂ) := by simp [amplitudeRotation, Real.cos_arccos lower upper] (lines 99-102)
Source SHA-256:aa51d33a6ca788b17879e1d88030b525f4f035c97d74588636ccf25f8c04b843· MIT (repository LICENSE)
Contract: 81cd5bb7165056bf4baa82f6c121c439472b40062074111aab6a7c9d703c307f
Item digest: a01f8f5245eb84999d3a73584d8019263b296e87e308ca3a6b391d676bbcc2ea
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 5. This is not measured graph distance or model difficulty.