A.12 Two exact information-loss statements
On this page · Permalink · Source line 616
The formal development isolates distinct obstructions. First, the initial histogram cannot be inverted on both states by any reconstruction function. Second, the projector itself is noninjective because it annihilates the nonzero normalized state \(\chi\).
Literal source. Publication.lean, physical lines 39–50.
/-- No state reconstruction function can invert the initial probability histogram on both states. -/
theorem no_reconstruction_from_initial_probabilities :
¬ ∃ R : (Index → ℝ) → (Index → ℂ),
R (fun i => Complex.normSq (psi i)) = psi ∧
R (fun i => Complex.normSq (chi i)) = chi := by
rintro ⟨R, hpsi, hchi⟩
have heq : (fun i => Complex.normSq (psi i)) =
(fun i => Complex.normSq (chi i)) := funext same_initial_probabilities
have hstate : psi = chi := by rw [← hpsi, ← hchi, heq]
have h := signed_state_recovers_arithmetic
rw [hstate, unsigned_state_erases_arithmetic] at h
norm_num at hLiteral source. Publication.lean, physical lines 52–57.
/-- Exact probabilities in the recovered basis, connected to the normalized state. -/
theorem recovered_probability_at (i : Index) :
Complex.normSq (Fᴴ.mulVec psi i) =
if Nat.gcd i.val 12 = 1 then (1/4 : ℝ) else 0 := by
rw [state_recovery, unitState_entry_formula]
by_cases h : Nat.gcd i.val 12 = 1 <;> norm_num [h, Complex.normSq_apply]Literal source. Publication.lean, physical lines 59–65.
/-- The operator is not injective. Its nonzero normalized kernel state is explicit. -/
theorem projector_not_injective : ¬ Function.Injective P.mulVec := by
intro h
have hz : chi = 0 := h (by simp [projector_kills_chi])
have hp := chi_normalized
rw [hz] at hp
norm_num [totalProbability] at hpThe nonreconstruction theorem quantifies over every function from real-valued histograms to complex-valued vectors. It uses equality of the two histograms and the incompatible transformed probabilities. This is a mathematical obstruction to a specified inverse, not a statistical claim about estimating a state from many measurements in several bases.
The traditional paper also proves that the two states cannot both be recovered up to an overall phase from this histogram. That strengthening is a prose corollary of their orthogonality and normalization. It is not separately exported as a quotient-by-global-phase Lean theorem.
Projection becomes reconstructive when its residual is retained. The next identity holds for every twelve-dimensional complex vector, including vectors outside the arithmetic signal subspace.
Literal source. Publication.lean, physical lines 33–37.
/-- Every signal is reconstructible from the retained and discarded components together. -/
theorem projector_residual_reconstructs (v : Index → ℂ) :
P.mulVec v + (1 - P).mulVec v = v := by
rw [Matrix.sub_mulVec, Matrix.one_mulVec]
exact add_sub_cancel _ _Its proof is algebraic. The identity \(Pv+(I-P)v=v\) itself does not require idempotence. Hermitian idempotence supplies the stronger interpretation as orthogonal retained and discarded components. This separates the reconstruction identity from the additional geometric structure.