QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Quantum Scientific Computing / Polynomial Signals

Polynomial Signals

Exercise PLAN-503

intermediate · boundary · test_public

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

Assumptions and conventions

    • T_k(cos p) = cos(k p) and U_{k-1}(cos p) = sin(k p)/sin p
    • sqrt(1-t^2) is taken nonnegative, matching p in [0, pi]

    Question

    On the invariant plane attached to a value t in the closed interval from minus one to one, the qubitization iterate acts as the plane rotation M = [[t, -sqrt(1-t^2)],[sqrt(1-t^2), t]]. Prove that the k-th power of M has diagonal entries equal to the first-kind Chebyshev value T_k(t) and off-diagonal entries equal to plus or minus sqrt(1-t^2) times the second-kind Chebyshev value U_{k-1}(t). Make explicit the trigonometric definitions you use and verify the degenerate behavior at t = 1 and t = -1.

    Hint: mathematical route

    Powering the plane rotation produces first-kind Chebyshev on the diagonal and second-kind Chebyshev times sqrt(1-t^2) off-diagonal; the prefactor forces the off-diagonal to vanish at the spectral endpoints.

    1. Set t = cos p so sqrt(1-t^2) = sin p and M is the rotation by p.
    2. Rotation powers add angles: M^k rotates by k p.
    3. Diagonal cos(k p) equals T_k(t).
    4. Off-diagonal sin(k p) equals sin p times U_{k-1}(t), i.e. sqrt(1-t^2) U_{k-1}(t).
    5. At t = 1 the prefactor sin p = 0 kills the finite U_{k-1}(1) = k, giving the identity.
    6. At t = -1 the power is (-1)^k identity, consistent with T_k(-1) = (-1)^k and zero off-diagonal.
    Reference solution

    Write t = cos(p) with p = arccos(t) in [0, pi], so sqrt(1-t^2) = sin(p) (nonnegative on this range). Then M = [[cos p, -sin p],[sin p, cos p]] is exactly the rotation by angle p. Powers of a rotation add angles: M^k = [[cos(k p), -sin(k p)],[sin(k p), cos(k p)]]. By the definitions T_k(cos p) = cos(k p) and U_{k-1}(cos p) = sin(k p)/sin(p), the diagonal entries are cos(k p) = T_k(t) and the off-diagonal entries are minus sin(k p) = minus sin(p) [sin(k p)/sin(p)] = minus sqrt(1-t^2) U_{k-1}(t) (upper right) and plus sqrt(1-t^2) U_{k-1}(t) (lower left). Degenerate cases: at t = 1, p = 0, so M = identity and M^k = identity; indeed T_k(1) = 1 and sqrt(1-t^2) U_{k-1}(1) = 0 since the prefactor sin(p) vanishes even though U_{k-1}(1) = k is finite. At t = -1, p = pi, so M^k = diag(cos(k pi), cos(k pi)) = (-1)^k identity; consistently T_k(-1) = (-1)^k and the off-diagonal prefactor sqrt(1-t^2) = 0 kills the U term. Thus the off-diagonal genuinely carries the second-kind polynomial, but always multiplied by sqrt(1-t^2), which is why it vanishes exactly at the spectral endpoints.

    Assessment rubric
    1. Substitutes t = cos p and identifies M as a rotation by p with sin p = sqrt(1-t^2) (1 weight)
    2. Uses the angle-addition / rotation-power identity to get M^k with cos(kp), sin(kp) (1 weight)
    3. Matches diagonal to T_k(t) and off-diagonal to plus/minus sqrt(1-t^2) U_{k-1}(t) via the standard Chebyshev definitions (1 weight)
    4. Checks t = 1 and t = -1, noting the sqrt(1-t^2) prefactor annihilates the finite U_{k-1} at the endpoints (1 weight)

    Graph-grounded prerequisites

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

    • Matrix analysis (frozen curriculum anchor; see graph registry)
    • Approximation theory (frozen curriculum anchor; see graph registry)
    • Harmonic analysis (frozen curriculum anchor; see graph registry)

    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

    Contract: b5f4f6be5686b4f0b01a01d2a3f07f68e5e6cac9b602dbe290e6d84f3269132b

    Item digest: b6107ce9db2ef5b7186113a0124865a058dbf3c5319ce52791949fccae0d6d19

    Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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