Exercise PLAN-207

Compute-rotate-uncompute gives an exact coherent oracle for the stored-angle cosine. Discarding the angle record dephases joint signal/index classes, not the signal marginal; basis inputs and equal records are exceptions to a blanket decoherence claim.

1. B loads the actual finite-bit angle q_t on work while preserving indices; exactness is for the declared cosine-rounded entry, not arbitrary real angle equality.
2. Bit-controlled y rotations give v_t=a_t|0>+sqrt(1-a_t²)|1> with relative signs retained, leaving work/index unchanged.
3. B-dagger restores the whole advertised work state coherently across both signal branches, yielding clean blocks D_a and D_b and their success probabilities.
4. Skipping the inverse and tracing work applies angle-class dephasing to joint signal/index coherence; the signal-only marginal and a single basis input's pure signal are unchanged.
5. An explicit two-angle sign witness distinguishes the coherent oracle from trace-out and from the wrong same-flag block; any replacement cleanup needs its own coherent-interface and resource proof.

The exact target is the declared rounded-angle entry a_t=A~_ij=cos(pi q_t), not necessarily A_ij or the original d'-bit fixed-point matrix datum. A generic theta_t=arccos(A_ij)/pi need not have an exact finite-d-bit expansion: for example A_ij=1/2 gives theta_t=1/3, not a finite binary fraction. Thus the predecessor's displayed finite-bit equality must be assessed, not made a new exact-representability premise. The source rounds theta and then redefines A~ by its cosine. Once the actual q_t and reversible B are specified, the following clean-oracle law is EXACT for a_t, irrespective of approximation quality to A. If |q_t-theta_t|<=epsilon_theta then |a_t-A_ij|<=pi epsilon_theta and ||v(q_t)-v(theta_t)||<=pi epsilon_theta; deriving epsilon_theta from the input-bit approximation and arithmetic is a separate error contract, especially near arccos endpoints.

Use order(S,W,T). For q=(.q_(d-1)...q_0)=sum_(r=1)^d q_(d-r)2^(-r), apply Ry(2pi*2^(-r)) to S controlled on bit q_(d-r). All rotations are about y, so their product is Ry(2pi q)=[[cos(pi q),-sin(pi q)],[sin(pi q),cos(pi q)]]. The work bits and index are not changed. Hence |0,0^d,t> goes under B to |0,q_t,t>, under CR to |v_t,q_t,t>, and under B-dagger on W,T to |v_t,0^d,t>. Since0<=q_t<1, sin(pi q_t)>=0 and equals b_t=sqrt(1-a_t²). B-dagger acts identically on S and restores W in BOTH signal branches; no inverse on the output signal is performed. For coherent coefficients c_t the final state is sum_t c_t|v_t,0^d,t>, with every relative phase retained. The basis rule extends to an isometry V:T->S tensor T, V|t>=|v_t,t>, because different t remain orthogonal. With clean embeddings the S=0,W=0 block is D_a=sum_t a_t|t><t|, not the full matrix A on a different register; the S=1,W=0 block is D_b=sum_t b_t|t><t|. For density rho on T, signal0 success is p_0=tr(D_a rho D_a†)=sum_t rho_tt a_t², and its conditional index state is D_a rho D_a†/p_0 only if p_0>0. A zero success supplies no normalized conditional output.

If the inverse is skipped, the full density is sigma_SWT=sum_(t,s)rho_ts |v_t><v_s| tensor |q_t><q_s| tensor |t><s|. Tracing W gives rho_dirty_ST=sum_(t,s)rho_ts delta_(q_t,q_s)|v_t><v_s| tensor |t><s|. In contrast rho_clean_ST=V rho V† has no delta. Equivalently trace-out implements the index-class dephasing sum_q (I_S tensor Q_q)rho_clean_ST(I_S tensor Q_q), Q_q=sum_(t:q_t=q)|t><t|. It kills cross terms only between populated DIFFERENT stored bit strings; equal rounded records preserve their coherence. In both cases tracing the index gives the identical signal marginal rho_S=sum_t rho_tt|v_t><v_t|. Dephasing or discarding the index cannot alter that marginal either. A single basis input has product v_t tensor q_t tensor t, so discarding W leaves the signal PURE and unchanged. It is false that this operation invariably destroys the signal's |0>,|1> superposition. Multiple populated angle classes generally make the joint S,T output mixed; this is a different claim from the signal-only state, which may already have been mixed before cleanup.

For an exact witness take d=2 and two distinct indices t,s with q_t=1/4, q_s=3/4, from real entries A_t=1/sqrt2,A_s=-1/sqrt2; complete any other entries by0 so ||A||_max<1. For input(|t>+|s>)/sqrt2, v_t=(|0>+|1>)/sqrt2 and v_s=(-|0>+|1>)/sqrt2. The clean joint state is their coherent indexed superposition; tracing the two orthogonal angle records instead leaves the equal mixture of |v_t,t> and |v_s,s>. The signal marginal is I/2 in BOTH. After signal0, however, the clean index is(|t>-|s>)/sqrt2, while the trace-out version is the incoherent equal mixture. The joint test S=0 and index-minus has probabilities1/2 versus1/4. Thus unchanged signal statistics do not certify the intended coherent oracle or its relative phase.

If instead of tracing one omits B-dagger and projects the original clean S=0,W=0 flag, the actual block is D_(a*1_(q=0)), not D_a, because <0^d|q_t>=delta_(q_t,0). It is ZERO on both witness indices. Trace-out has no single retained-unitary block to read: its signal0 subchannel is D_a (sum_q Q_q rho Q_q) D_a†, with the same signal0 probability but generally different coherent output from D_a rho D_a†. Therefore neither tracing nor merely projecting the original flag substitutes for the specified clean oracle. The given B-dagger is a sufficient coherent cleanup using the retained index; it is not uniquely necessary as a circuit. Any alternative must prove the same clean interface. A W-only unitary cannot map two orthogonal q records to the same |0> while leaving everything else unchanged, by inner-product preservation. Known constant records, a single basis input, or one populated record class are exceptions to the decoherence claim, not automatic clean-register reuse guarantees.

This construction uses one B and one B-dagger plus d ideal bit-controlled y rotations; the composite B may require the original bit oracle, reversible arithmetic and additional clean scratch, all of which must be restored by its actual inverse. Those are not free from a d-bit output-length statement. There is no generic finite-bit exact-real or elementary-gate complexity certificate here. q=0 gives a_t=1,b_t=0, allowed for a rounded entry even though the original A has strict max norm below1; q<1 excludes an exact q=1. For d=0 there is only the empty record q=0 and no distinct-record dephasing. The proof requires no assumption that every angle differs or every index is populated, and the inverse is not a cleanup of the intentional amplitude signal itself.

1. Distinguishes stored q and cosine-redefined A~ from arbitrary exact A/d'-bit input; exposes nonrepresentable theta=1/3 without adding a premise, and states exact rounded-law versus separate precision guarantees. (1 weight)
2. Tracks S,W,T through B, bit-controlled Ry rotations and B-dagger for basis/coherent inputs, derives D_a/D_b clean blocks and success/conditioning, and preserves negative amplitudes and phases. (1 weight)
3. Derives the full skipped-inverse density, work-trace angle-class dephasing and unchanged signal marginal; includes basis-input and equal-record exceptions instead of universal signal-decoherence rhetoric. (1 weight)
4. Supplies the exact q=1/4,3/4 sign/interference witness, compares same-flag projection with trace-out, and states coherent-interface cleanup/non-unique-inverse and resource/workspace boundaries without a W-only erasure claim. (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: a2990190157e0445347d0897271b81649ccc15e8872d3c5e01b3e39a92c26d6f

Item digest: abd4e555dca2b13af8188d3475ae5858a8b7503b4ecf137abd698c38bd5d5246

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "question_version": 2, "predecessor_key": "qcb-core-plan-207-amplitude-oracle-from-bit-oracle-uncompute", "predecessor_item_digest": "fca254be303c5fff08fa40bf0e0ed738cf6ee210ff0c6946190c4380d09c2874", "predecessor_contract_hash": "7d2f9cde13aacc1e0b0bc6861255c55ac6c5054d724b259cef6b33fb79326f44", "current_contract_hash": "a2990190157e0445347d0897271b81649ccc15e8872d3c5e01b3e39a92c26d6f", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/plan-207-rounded-angle-joint-coherence-question-successor.json", "repair_record_digest": "d98af1a91282588fcbf06bd1c8a5d05d8572286cb4cefbb51792dc76ac4b1410", "review_record": "reports/textbook-v1/repairs/plan-207-rounded-angle-joint-coherence-question-successor-review.json", "review_digest": "f1ea989fa20eb8821374aaa644df642235e458d3714a32dbe73f2203c9684949", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }