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

Shared mathematical foundations / Phase Semantics

Phase Semantics

Exercise LA-016

intermediate · counterexample · test_public

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

  • Finite-dimensional complex Hilbert spaces unless real amplitudes are explicitly specified
  • All basis/register permutations are fixed and applied to both input and output
  • Column-vector action; Euclidean induced operator norm for norm claims
  • Source inspection only; no fresh formal verification

Question

For the real rotation R(theta)=[[cos(theta/2),-sin(theta/2)],[sin(theta/2),cos(theta/2)]], compare R(theta+2pi) and R(theta). A colleague claims the two full operators have distance0 because every output probability agrees. Refute or prove that claim, and distinguish bare-system global-phase equivalence from coherent branch use.

Hint: mathematical route

For the real rotation R(theta)=[[cos(theta/2),-sin(theta/2)],[sin(theta/2),cos(theta/2)]], compare R(theta+2pi) and R(theta). A colleague claims the two full operators have distance0 because every output probability agrees. Refute or prove that claim, and distinguish bare-system global-phase equivalence from coherent branch use.

  1. A2pi parameter shift negates both matrix sine/cosine entries.
  2. Unitary norm gives distance2 despite unchanged probabilities.
  3. A controlled branch sign is relative rather than globally shared.
Reference solution

Both sine and cosine change sign after adding pi to their arguments, so R(theta+2pi)=-R(theta). Their difference is -2R(theta), whose induced operator norm is2, not0. Bare-system output probabilities agree because the sign is a global phase. In a coherent controlled use, however, applying the minus sign only on the active control branch introduces a relative phase between control branches. Thus probabilities on one isolated output do not establish equality of operators; an error metric modulo global phase is different from the exact operator-norm contract. Equivalently the exact distance formula gives2|sin(2pi/4)|=2.

Assessment rubric
  1. Distance2 not0 (1 weight)
  2. Explain probability agreement without operator equality (1 weight)
  3. State exact-vs-phase-quotiented metric distinction (1 weight)

Graph-grounded prerequisites

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

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: fdd526493c11aaf1f3803de3c7e00ae7ecf3828571081cf35deca3d6295bbf1d

Item digest: 9c8a04ca1889fb0a56d3f452b52f5640741fb20e9f1d4e4962b89aef5642bc12

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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