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-513

intermediate · proof · test_public

primary source nl only. Explicit question version 2 with distinct contract-change review; the predecessor question is not equivalent current gold. Core, family and split are retained. No new Lean verification is claimed for this NL view.

Assumptions and conventions

  • Exactly one marked element among N basis states
  • Sine of the half-angle equals the overlap 1/sqrt(N) of the uniform state with the marked state
  • A product of two planar reflections with axes differing by phi is a rotation by 2 phi

This question explicitly revises its historical contract. A Lean companion must bind the current contract hash, not the predecessor hash. This is one reserved core, not two exercises.

Question

Keep the original promise of exactly one marked basis state among N states, with no exclusion of the positive endpoint N=1. Put g=|marked>, psi=N^(-1/2) sum_x |x>, R_g=I-2|g><g| and R_psi=2|psi><psi|-I, with Grover iterate G=R_psi R_g (marked flip first). Assess the predecessor's request to work in a two-dimensional real plane containing a normalized uniform superposition of all unmarked states for every allowed N: is that object defined at N=1? For N>1 construct the normalized unmarked state b and derive the exact matrix of G in the ordered basis (g,b). Define phi in (0,pi/2] by sin(phi)=1/sqrt(N), call 2phi the full iteration angle, distinguish its signed Cartesian orientation in (g,b) from the angle measured from b toward g, and prove the signed marked coefficient after k>=0 iterations is sin((2k+1)phi). Treat N=1 directly at the operator/state level without inventing a bad vector or a two-dimensional plane; say precisely which scalar formula survives and which geometric assertion fails. Do not infer that ordinary integer pi-phase iterations achieve arbitrarily near-unit success for every N.

Hint: mathematical route

The Grover plane exists only when the bad component is nonzero. For N>1 the exact oriented rotation yields the odd-multiple sine; at N=1 G=-I preserves success while the two-dimensional construction is undefined.

  1. Set sin(phi)=1/sqrt(N). For N>1 construct the normalized bad vector and decompose psi; at N=1 that vector is undefined, not a new hypothesis.
  2. On the nontrivial plane the marked flip is diag(-1,1); at N=1 it is the scalar -I.
  3. The uniform reflection fixes psi and negates its orthogonal line; at N=1 it is I on the sole line.
  4. The two nontrivial mirror axes differ by phi, yielding angle magnitude2phi, with orientation measured explicitly rather than inferred.
  5. The ordered(g,b) product is [[cos2phi,sin2phi],[-sin2phi,cos2phi]]; the endpoint instead has G=-I.
  6. All k>=0 give signed marked coefficient sin((2k+1)phi), including (-1)^k at N=1, without a universal near-unit success claim.
Reference solution

The old universal two-dimensional-plane request is not defined at the allowed endpoint N=1: the unmarked sum is zero, and a zero vector cannot be normalized. This must be assessed, not silently removed by assuming N>=2. For N>1 define b=(N-1)^(-1/2) sum_{x unmarked}|x>. Then g,b are orthonormal and psi=s g+c b with s=sin(phi)=1/sqrt(N), c=cos(phi)=sqrt((N-1)/N). Both reflections preserve this real plane. In the ordered basis (g,b), R_g=diag(-1,1), and R_psi=[[2s^2-1,2sc],[2sc,2c^2-1]]. Multiplying in the stipulated order gives G=[[1-2s^2,2sc],[-2sc,2c^2-1]]=[[cos(2phi),sin(2phi)],[-sin(2phi),cos(2phi)]]. It is the Cartesian rotation by -2phi in this ordered basis. Equivalently, parameterizing a vector as sin(alpha)g+cos(alpha)b measures alpha from b toward g; multiplication advances alpha to alpha+2phi. The mirror axes are b for R_g and psi for R_psi and differ by phi, giving the same magnitude 2phi with this orientation. Thus Gg=cos(2phi)g-sin(2phi)b and Gb=sin(2phi)g+cos(2phi)b. The addition formulas, or induction starting at alpha=phi, give G^k psi=sin((2k+1)phi)g+cos((2k+1)phi)b for every integer k>=0. The marked coefficient is signed; its measurement probability is sin^2((2k+1)phi), and its absolute amplitude magnitude is the absolute value of that sine. At N=1, psi=g, R_psi=I on the one-dimensional space and R_g=-I, so G=-I and G^k psi=(-1)^k g exactly. Taking phi=pi/2, sin((2k+1)phi)=(-1)^k still matches the exact signed coefficient, but there is no bad component, mirror-axis comparison or planar rotation to prove. The mark is already found with probability one at k=0. N=0 is incompatible with the unique-mark promise, not an extra excluded search case. Ordinary integer iterations do not guarantee arbitrarily high success for all nontrivial sizes: N=2 has phi=pi/4 and success exactly1/2 for every integer k. Efficient implementation, finite-bit synthesis and any extra cleanup or success boosting are outside this algebraic question. This is an explicit endpoint-corrected question, not proof of the original universal plane assertion.

Assessment rubric
  1. Explicitly identifies/refutes the nonexistent normalized unmarked vector and two-dimensional plane at N=1, without adding N>=2 as a standing premise. (1 weight)
  2. For N>1 constructs orthonormal g,b and psi=sin(phi)g+cos(phi)b; obtains both reflection matrices and their stipulated product with correct signs. (1 weight)
  3. Distinguishes Cartesian angle -2phi in basis(g,b) from advancement +2phi measured from b toward g, and derives the all-k signed sine/cosine action. (1 weight)
  4. Treats N=1 as G=-I with exact (-1)^k coefficient, distinguishes signed coefficient/magnitude/probability, and rejects a universal near-unit integer-iteration guarantee using N=2. (1 weight)

Graph-grounded prerequisites

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

  • Operator and semigroup theory (frozen curriculum anchor; see graph registry)
  • Matrix analysis (frozen curriculum anchor; see graph registry)
  • Approximation theory (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: f4b50cd4ee83f991c95c99e67653cc21fb47d221b7e2c687258c45a5fb328dfc

Item digest: 6e9a443f8f2f5e5f4fb275d98fee4257f8ebfcc5af8cf08e1da6d52ad95b82a3

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

Question revision lineage

{ "question_version": 2, "predecessor_key": "qcb-core-plan-513-grover-two-reflection-rotation", "predecessor_item_digest": "cd8b6f0ad2579a7da387e77474953610eafc452d26ac9809572e224383c47544", "predecessor_contract_hash": "223283ae1e418ed41b108cf5cec5af739ef40b70d1bd30aa955b782c7f7f80a9", "current_contract_hash": "f4b50cd4ee83f991c95c99e67653cc21fb47d221b7e2c687258c45a5fb328dfc", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/plan-513-nontrivial-plane-endpoint-question-successor.json", "repair_record_digest": "7852abdac0ad37b8434b8dcbcc72b873c5e0a78e60b3e14505ed69f1305968c4", "review_record": "reports/textbook-v1/repairs/plan-513-nontrivial-plane-endpoint-question-successor-review.json", "review_digest": "faafe8108d1c06427ac7f21807b6d6c953835ff23adce45f1ef49e25514854b1", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }