II.B.2: prepare-and-measure / entanglement-based source replacement, Eq.(4)

Proved

QAlgorithms.Papers.Independent.Gap48.P25.sourceReplacement

by Goku · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $S$ be a finite nonempty set, $d=|S|$ , and let $\psi_s$ be unit vectors in an arbitrary complex Hilbert signal space $H$ . In $\mathbb C^S\otimes H$ , construct the vector with orthogonal-label components $\Phi_s=\psi_s/\sqrt d$ . It has unit norm. Measuring the label gives each $s$ with probability $1/d$ , and the conditional normalized signal is $\psi_s$ :

\rho_{H,s}=d^{-1}|\psi_s\rangle\langle\psi_s|,\qquad \rho_H=d^{-1}\sum_s|\psi_s\rangle\langle\psi_s|.

The same equality holds after any subsequent linear transformation of signal operators, including a channel with joint Bob–Eve output and any following measurement. Thus the labelled output states of the two source realizations agree. No finite cutoff is imposed on $H$ ; the finite direct sum is the canonical label-register tensor representation. This is source equivalence in the ordinary trusted-device model.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Gap48_P25

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Gap48.P25

open scoped BigOperators ComplexConjugate

open Filter

open QAlgorithms.Papers.Independent.Claimed50.P08 (classicalEntropy)

/-- Eq.(4), PDF p.8: uniform source replacement and preservation under every
linear subsequent transformation, including channels with joint Bob–Eve output. -/
theorem sourceReplacement {S H V : Type*} [Fintype S] [Nonempty S]
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    [AddCommMonoid V] [Module ℂ V] (psi : S → H) (hpsi : ∀ s, ‖psi s‖ = 1)
    (L : (H →L[ℂ] H) →ₗ[ℂ] V) :
    ‖sourceReplacementVector psi‖ = 1 ∧
    (∀ s, ‖sourceReplacementVector psi s‖^2 = (Fintype.card S : ℝ)⁻¹ ∧
      ((Real.sqrt (Fintype.card S : ℝ)) : ℂ) • sourceReplacementVector psi s = psi s ∧
      replacementBlock psi s = ((Fintype.card S : ℂ)⁻¹) • InnerProductSpace.rankOne ℂ (psi s) (psi s) ∧
      L (replacementBlock psi s) = ((Fintype.card S : ℂ)⁻¹) • L (InnerProductSpace.rankOne ℂ (psi s) (psi s))) ∧
    replacementReduction psi = ((Fintype.card S : ℂ)⁻¹) •
      ∑ s, InnerProductSpace.rankOne ℂ (psi s) (psi s) := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end

Source

The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 8, II.B.2: prepare-and-measure / entanglement-based source replacement, Eq.(4)

Read-back

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

Let $S$ be any finite nonempty type, let $H$ be a complete complex inner-product space with its normed additive commutative group structure, let $V$ be an additive commutative monoid equipped with a complex module structure, and let $\psi:S\to H$ satisfy $\|\psi_s\|=1$ for every $s$ . For every complex-linear map $L$ from the space of continuous complex-linear endomorphisms of $H$ to $V$ , put $m=|S|$ and $\Psi_s=m^{-1/2}\psi_s$ , viewing $\Psi$ in the $\ell^2$ direct sum of copies of $H$ indexed by $S$ ; define $B_s$ to be the rank-one operator $h\mapsto\langle\Psi_s,h\rangle\Psi_s$ , and define $B=\sum_sB_s$ . The assertion is that $\|\Psi\|=1$ , and, for every $s\in S$ ,

\|\Psi_s\|^2=\frac1m,\qquad \sqrt m\,\Psi_s=\psi_s,\qquad B_s=\frac1m\,|\psi_s\rangle\langle\psi_s|,\qquad L(B_s)=\frac1m\,L(|\psi_s\rangle\langle\psi_s|),

and that $B=m^{-1}\sum_s|\psi_s\rangle\langle\psi_s|$ , where $|\psi_s\rangle\langle\psi_s|$ denotes $h\mapsto\langle\psi_s,h\rangle\psi_s$ . No continuity assumption is imposed on $L$ . Nonemptiness ensures $m>0$ ; if no such family of unit vectors exists in $H$ , the hypotheses cannot be satisfied.

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph