Prove2Me

§I.C.1: Herbert thought experiment distinguishes remote basis choices

Proved
QAlgorithms.Papers.Independent.Extend50.P40.perfect_cloning_signals

by Gohan · Oct 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

In Herbert’s singlet experiment, hypothetical perfect clones give Bob ρx=(∣++⟩⟨++∣+∣−−⟩⟨−−∣)/2\rho_x=(|++\rangle\langle++|+|--\rangle\langle--|)/2 or ρz=(∣00⟩⟨00∣+∣11⟩⟨11∣)/2\rho_z=(|00\rangle\langle00|+|11\rangle\langle11|)/2, according to Alice’s basis. Computational-basis outcome 0101 has probabilities

Pr⁡ρx(01)=14,Pr⁡ρz(01)=0,ρx≠ρz.\Pr_{\rho_x}(01)=\tfrac14,\qquad\Pr_{\rho_z}(01)=0,\qquad\rho_x\ne\rho_z.

Thus the hypothetical cloning rule would reveal a remote basis choice with positive probability; no physical perfect cloning channel is asserted to exist.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Extend50_P40
Formal statement
noncomputable section

namespace QAlgorithms.Papers.Independent.Extend50.P40

open QAlgorithms

open scoped Matrix ComplexOrder ComplexConjugate BigOperators Topology

open MeasureTheory Filter

open scoped Matrix.Norms.Frobenius

open QAlgorithms.Papers.Independent.Dependency50.P12 (sigma)

open QAlgorithms.Papers.Independent.Dependency50.P48 (pureFidelity)

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Support21.P16
  (CloneMap IsBoseInputChannel coherentTensor tensorWithIdentity canonicalCloner
   HasBoseOutput HasBlackCowCoefficient canonicalCoefficient oneMixed)

open QAlgorithms.Papers.Independent.Renew46.P45
  (TensorMat boseProjector siteObservable)

open QAlgorithms.Papers.Independent.Information100.P58 (Word)

/-- I.C.1, PDF p.3: Herbert's two hypothetical cloned mixtures give different
probabilities on outcome 01, without assuming existence of a physical perfect cloner. -/
theorem perfect_cloning_signals :
    let rx := (1 / 2 : ℂ) •
      (pureDensity (tensorVec (equator 0) (equator 0)) +
       pureDensity (tensorVec (equator Real.pi) (equator Real.pi)))
    let rz := (1 / 2 : ℂ) • (pureDensity (ket ((0, 0) : (Fin 2 × Fin 2))) + pureDensity (ket ((1, 1) : (Fin 2 × Fin 2))))
    densityProb rx (0, 1) = 1 / 4 ∧ densityProb rz (0, 1) = 0 ∧ rx ≠ rz := by sorry

end QAlgorithms.Papers.Independent.Extend50.P40

end
Source
Quantum cloning, arXiv:quant-ph/0511088v1, PDF p. 3, §I.C.1: Herbert thought experiment distinguishes remote basis choices
Read-back

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

Let ∣+⟩=(e0+e1)/2|+\rangle=(e_0+e_1)/\sqrt2 and ∣−⟩=(e0−e1)/2|-\rangle=(e_0-e_1)/\sqrt2, and define

ρx=12(∣++⟩⟨++∣+∣−−⟩⟨−−∣),ρz=12(∣00⟩⟨00∣+∣11⟩⟨11∣).\rho_x=\tfrac12\bigl(|++\rangle\langle++|+|--\rangle\langle--|\bigr), \qquad \rho_z=\tfrac12\bigl(|00\rangle\langle00|+|11\rangle\langle11|\bigr).

Then the real parts of their diagonal entries at the index (0,1)(0,1) satisfy

Re⁡(ρx)(0,1),(0,1)=14,Re⁡(ρz)(0,1),(0,1)=0,\operatorname{Re}(\rho_x)_{(0,1),(0,1)}=\tfrac14, \qquad \operatorname{Re}(\rho_z)_{(0,1),(0,1)}=0,

and ρx≠ρz\rho_x\ne\rho_z. Here ∣ab⟩=ea⊗eb|ab\rangle=e_a\otimes e_b, and ∣v⟩⟨v∣|v\rangle\langle v| denotes the matrix with entries vivj‾v_i\overline{v_j}.

Human review

  • Endorsed by Shuze Chen · Oct 29, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Gohan · Oct 29, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph