Appendix G2: sample density records cannot fix a controlled global phase

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.controlled_phase_obstruction

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let the ambient system be nonempty, $U$ unitary and $z$ a complex phase with $|z|=1$ and $z\ne1$ . Every density record is invariant under replacing $U$ by $zU$ :

U\rho U^\dagger=(zU)\rho(zU)^\dagger\quad\text{for every }\rho.

Nevertheless their controlled unitaries are not scalar-phase equivalent: no unit phase $w$ satisfies $(zU)^c=wU^c$ . The identity control branch forces $w=1$ , while the other branch retains $z$ . This is an identifiability obstruction when only sample density copies and no coherent phase reference are supplied.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P67

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix Matrix.Norms.L2Operator

attribute [local instance] Classical.propDecidable

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P67

variable {I J K L A : Type*} [Fintype I] [DecidableEq I]
  [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K]
  [Fintype L] [DecidableEq L] [Fintype A] [DecidableEq A]

/-- PDF p.28, G2 discussion: density records cannot distinguish global phases, but
nontrivial relative phase changes a systemControlled unitary. -/
theorem controlled_phase_obstruction [Nonempty I] (U : Matrix.unitaryGroup I ℂ)
    (z : ℂ) (hz : ‖z‖ = 1) (hne : z ≠ 1) :
    (∀ rho : Matrix I I ℂ, IsDensityMatrix rho →
      densityConjugation (z • (U : Matrix I I ℂ)) rho = densityConjugation (U : Matrix I I ℂ) rho) ∧
    ¬ ∃ w : ℂ, ‖w‖ = 1 ∧ systemControlled (z • (U : Matrix I I ℂ)) = w • systemControlled (U : Matrix I I ℂ) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 28, Appendix G2: sample density records cannot fix a controlled global phase

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $I$ be a finite nonempty index type with decidable equality, let $U$ be unitary on $\mathbb C^I$ , and let $z\in\mathbb C$ satisfy $|z|=1$ and $z\ne1$ . Define $C(V)=1_I\otimes|0\rangle\langle0|+V\otimes|1\rangle\langle1|$ . Then, for every positive semidefinite matrix $\rho$ of trace $1$ ,

(zU)\rho(zU)^\dagger=U\rho U^\dagger,

and there does not exist any $w\in\mathbb C$ with $|w|=1$ such that

C(zU)=w\,C(U).

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph