A.11 Hermitian projection and phase-sensitive states
On this page · Permalink · Source line 532
The selector is Hermitian and idempotent. Transport through a unitary matrix then proves the corresponding facts for \(P\). They are ordinary matrix identities, not claims that every rational list operation is an orthogonal projection.
Literal source. Conventions.lean, physical lines 84–108.
theorem selector_idempotent : D * D = D := by
unfold D
rw [Matrix.diagonal_mul_diagonal]
congr 1
funext i
by_cases h : Nat.gcd i.val 12 = 1 <;> simp [h]
theorem selector_selfAdjoint : Dᴴ = D := by
ext i j
by_cases h : i = j
· subst j
simp [D, Matrix.conjTranspose_apply, apply_ite star]
· simp [D, Matrix.conjTranspose_apply, h, Ne.symm h]
theorem projector_idempotent_complex : P * P = P := by
rw [← projector_transport]
calc
(F * D * Fᴴ) * (F * D * Fᴴ) = F * D * (Fᴴ * F) * D * Fᴴ := by
simp only [Matrix.mul_assoc]
_ = F * D * Fᴴ := by rw [fourier_unitary_left, Matrix.mul_one, Matrix.mul_assoc F D D,
selector_idempotent]
theorem projector_selfAdjoint_complex : Pᴴ = P := by
rw [← projector_transport]
simp [Matrix.conjTranspose_mul, selector_selfAdjoint, Matrix.mul_assoc]The vectors \(\psi\) and \(\chi\) are separately defined states. One is the signed arithmetic amplitude vector and the other its entrywise absolute value. They have the same squared amplitudes at each initial index but retain different relative phase. The development neither claims nor requires a universal quantum operation implementing the nonlinear map \(v\mapsto |v|\).
Literal source. SemanticBridge.lean, physical lines 145–174.
theorem psi_normalized : totalProbability psi = 1 := by
have h := congrArg interpret exact_psi_normalized
simpa [psi] using congrArg Complex.re h
theorem chi_normalized : totalProbability chi = 1 := by
have h := congrArg interpret exact_chi_normalized
simpa [chi] using congrArg Complex.re h
theorem unitState_normalized : totalProbability unitState = 1 := by
have h := congrArg interpret exact_unit_normalized
simpa [unitState] using congrArg Complex.re h
theorem same_initial_probabilities (i : Index) :
Complex.normSq (psi i) = Complex.normSq (chi i) := by
have h := congrArg interpret (exact_same_initial_probabilities i)
simpa [psi, chi, complexVector] using congrArg Complex.re h
theorem states_orthogonal : ∑ i, star (psi i) * chi i = 0 := by
have h := congrArg interpret exact_orthogonal_states
simpa [psi, chi, complexVector] using h
theorem signed_state_recovers_arithmetic :
coprimeProbability (Fᴴ.mulVec psi) = 1 := by
have h := congrArg interpret exact_coprime_mass_psi
simpa [F, psi] using congrArg Complex.re h
theorem unsigned_state_erases_arithmetic :
coprimeProbability (Fᴴ.mulVec chi) = 0 := by
have h := congrArg interpret exact_coprime_mass_chi
simpa [F, chi] using congrArg Complex.re hThe transformed probability statement is exact. The measurement event is the coprime-frequency subset. After applying \(F^*\), its probability is one for \(\psi\) and zero for \(\chi\). This basis change reveals information that their shared initial histogram does not contain.