Exercise PLAN-517

The odd Chebyshev/sine formula has real-inverse domain[-1,1] but continues correctly through any complex inverse-sine value; signed reflected hyperbolic formulas describe both real exterior branches without creating unphysical normalized overlaps.

1. For real a in[-1,1], phi=arcsin(a) exists; endpoints/zero/k0 remain valid rather than requiring an interior overlap.
2. The Chebyshev/cosine recurrence holds for complex arguments as well, with beta=pi/2-z.
3. Odd order yields the exact(-1)^k sine relation for every complex z; any inverse value of a therefore recovers the same polynomial without a global branch claim.
4. T_3(2)=26 is exact, whereas the real-inverse expression at2 is undefined; a bounded real-sine extrapolation cannot produce26.
5. The complex choice z=pi/2-i arccosh2 gives sin(z)=2 and (-1)sin(3z)=26, so real-domain failure is not a refutation of complex continuation.
6. The real exterior formulas use cosh(j arccosh a) for a>=1 and(-1)^j cosh(j arccosh(-a)) for a<=-1; physical normalization and phase obligations remain separate.

As a REAL inverse-sine expression, the displayed formula is defined for a in[-1,1]. For those a let phi=arcsin(a) in[-pi/2,pi/2] and beta=pi/2-phi. Then cos beta=sin phi=a, and T_(2k+1)(a)=cos((2k+1)(pi/2-phi))=(-1)^k sin((2k+1)phi). The sign follows from cos((2k+1)pi/2)=0 and sin((2k+1)pi/2)=(-1)^k. This includes a0 (both sides0), a1 (both sides1), a-1 (both sides-1) and k0 (T_1(a)=a=sin(arcsin a)). The interval is the domain of the real inverse, not a maximal domain for the polynomial identity after analytic continuation.

For a>1 there is NO real phi with sin phi=a, so real arcsin(a), understood as an inverse, has no value. Consequently there is no defined real numerical equality there to falsify by substitution. For a2,k1, the recurrence gives T_3(x)=4x^3-3x and T_3(2)=26. This refutes any attempted extension that insists its right side remains (-1) times the sine of a REAL argument, hence lies in[-1,1]. It does NOT refute a complex inverse-sine interpretation. Assigning a totalized software function outside its inverse domain would be an extra convention, not the real-inverse identity under discussion. A complex sine is not bounded in modulus by1.

The continuation can be proved without postulating a global branch. The Chebyshev recurrence T_0=1,T_1=x,T_(j+1)=2x T_j-T_(j-1), together with cos((j+1)w)=2cos(w)cos(jw)-cos((j-1)w), proves T_j(cos w)=cos(jw) for every COMPLEX w by induction. Put w=pi/2-z and j=2k+1. The same entire trigonometric relations give T_(2k+1)(sin z)=cos((2k+1)(pi/2-z))=(-1)^k sin((2k+1)z) for all complex z. Therefore any complex number z satisfying sin z=a gives the SAME polynomial value T_(2k+1)(a), independently of which inverse value was chosen. Local inverse branches can be used on appropriate domains, but this does not define a single global holomorphic arcsine through the branch points±1. No branch-independence conclusion relies on applying a real bounded-sine estimate to complex arguments.

For the requested exact value, put eta=arccosh(2)=log(2+sqrt(3))>0 and choose z=pi/2-i*eta. From sin(x+i y)=sin x cosh y+i cos x sinh y, sin z=cosh eta=2. Moreover sin(3z)=sin(3pi/2)cosh(3eta)=-cosh(3eta). The hyperbolic triple-angle identity gives cosh(3eta)=4*cosh(eta)^3-3*cosh(eta)=26, so (-1)^1 sin(3z)=26=T_3(2). This explicitly refutes the predecessor ANSWER'S rejection of complex continuation. It is not a counterexample to the real inverse's domain restriction. In particular k0 also continues correctly to T_1(a)=sin z=a; no exceptional prohibition appears there.

For the real outside-interval representation, if a>=1 write a=cosh eta, eta=arccosh(a)>=0. The functions cosh(j eta) satisfy the same recurrence in j and initial values1,cosh eta as T_j(a), so T_j(a)=cosh(j arccosh a). For a<=-1, write b=-a>=1. The Chebyshev recurrence also proves T_j(-b)=(-1)^j T_j(b). Thus T_j(a)=(-1)^j cosh(j arccosh(-a)). The inverse hyperbolic cosine has a nonnegative REAL argument at least1 on each stated branch. The formula cosh(j arccosh(a)) without reflection is not a real formula for a<-1. At a±1 these formulas give1 and(-1)^j. For the odd order here the negative-side value is -cosh((2k+1)arccosh(-a)); for example T_3(-2)=-26. The original broad hyperbolic convention is retained with this mandatory reflected argument and parity sign, not treated as an unqualified positive-side formula.

Finally, |<u|v>|<=1 for unit vectors by Cauchy-Schwarz, and any clean compression J_out†U J_in of a unitary between isometries has norm<=1. Singular values of an exact unit-normalized encoded block therefore lie in[0,1]. An inner product between unnormalized vectors can exceed1, but calling it an overlap amplitude does not make it a normalized state's amplitude, success probability or valid unit-normalized scalar block. One must normalize or change the block factor and track that change; complex analytic continuation is mathematics, not a physical amplitude-amplification construction outside its normalized domain. In source Example11.4 the scalar a=1/sqrt(N) lies in[0,1] for N>=1, and the qubitization expression carries the exact factor(-1)^k relative to the conventional Grover expression. That factor has no effect on an isolated success probability, but becomes a relative phase under control unless tracked or corrected; it is not silently discarded in the scalar identity.

1. States[-1,1] as the real-inverse domain, proves the real identity with the correct(-1)^k sign and checks endpoints/zero/k0; does not mistake that domain statement for failure of complex continuation. (1 weight)
2. Proves the all-complex odd multiple-angle identity by a complete recurrence or equivalent argument; explains any inverse value recovers the polynomial and distinguishes this from existence of a global holomorphic inverse branch. (1 weight)
3. Computes T_3(2)=26 and separates an undefined real arcsine from a false bounded-real-sine extrapolation. Constructs z=pi/2-i arccosh2 and verifies (-1)sin(3z)=26 exactly rather than claiming complex sine bounded by1. (1 weight)
4. Derives both signed real hyperbolic branches, including a<-1 and endpoints; keeps normalized overlap/unitary-compression constraints and exact phase bookkeeping separate from analytic continuation and probabilities. (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: a7cd3d15c64e8ec16178faaa51a6e067064725220063b471bf6e1826851513fe

Item digest: 70cd1d0ed0ffc4439747cbcf81260969b18cff8679d89b37942a46e634fd3b8f

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "question_version": 2, "predecessor_key": "qcb-core-plan-517-chebyshev-identity-sine-domain-boundary", "predecessor_item_digest": "6ee75377e19be126a85a576b4e313b2e6b2f2c4d424a2f8740dfd32e1e6340ce", "predecessor_contract_hash": "fe6b370225ca42bd08b2aabe06434b9ffb89977c361b5ebd6a75fa01fb650f2e", "current_contract_hash": "a7cd3d15c64e8ec16178faaa51a6e067064725220063b471bf6e1826851513fe", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/plan-517-real-domain-complex-continuation-question-successor.json", "repair_record_digest": "b68bdff475347f2e2482728410afd647d72c28f1adfdf2cbcabd3575efd406dd", "review_record": "reports/textbook-v1/repairs/plan-517-real-domain-complex-continuation-question-successor-review.json", "review_digest": "adad0db13b5e2b971d6469251f8a9f859d937eedad104e803e1eaaf9db01ab3d", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }