II: effective state and conditional measurement distribution, (1)–(2)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.postselectionState

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

prove2quantum

Let $n\ge1$ , $0\le Q\le\tfrac12$ , and let $C=(C_k)_{k\in K}$ be a nonempty family of distinct binary words of length $n$ , where $m=|K|$ . Write $\rho_Q=(1-2Q)|\Phi^+\rangle\langle\Phi^+|+(Q/2)I_4$ , with $|\Phi^+\rangle=(|00\rangle+|11\rangle)/\sqrt2$ . Regroup its independent copies as $A^nB^n$ . Define $K_C=\sum_k|k\rangle\langle C_k|$ and $P_C=(I\otimes K_C)\rho_Q^{\otimes n}(I\otimes K_C)^\dagger$ . The input has trace one and is positive, and $P_C$ is positive. If $p_Q(a,b)$ is the diagonal measurement law of the input, then

\operatorname{Tr}P_C=\Pr(B^n\in C)=\frac{m}{2^n}>0,\qquad \frac{\langle a,k|P_C|a,k\rangle}{\operatorname{Tr}P_C} =\frac{p_Q(a,C_k)}{\Pr(B^n\in C)}.

Thus filtering preserves the complete conditional joint distribution, including Bob's codeword label. The filtered operator itself is unnormalized.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P30

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P30

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

variable {I J K L A B : Type}

variable [Fintype I] [Fintype J] [Fintype K] [Fintype L]

variable [Fintype A] [Fintype B]

/-- PDF pp.2–3, (1)–(2): actual filtering, positive acceptance mass m/2^n,
and the complete conditional joint law, rather than only a yes/no event. -/
theorem postselectionState {n : ℕ} (hn : 1 ≤ n) [Nonempty K]
    (C : K → Qubits n) (hC : Function.Injective C) (Q : ℝ)
    (hQ0 : 0 ≤ Q) (hQ1 : Q ≤ 1 / 2) :
    IsDensityMatrix (sixStateCopies (Fin n) Q) ∧ (bobState C Q).PosSemidef ∧
    (bobState C Q).trace = ((Fintype.card K : ℂ) / 2 ^ n) ∧
    acceptanceMass C Q = (Fintype.card K : ℝ) / 2 ^ n ∧
    0 < acceptanceMass C Q ∧
    ∀ (a : Qubits n) (k : K),
      diagonalLaw (bobState C Q) a k =
        (sixStateCopies (Fin n) Q (a, C k) (a, C k)).re / acceptanceMass C Q := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P30

end

Source

Numerical evidence for bound secrecy from two-way post-processing in quantum key distribution, arXiv:1612.07734v2, PDF p. 3, II: effective state and conditional measurement distribution, (1)–(2)

Read-back

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

Let $n\ge1$ , let $K$ be a finite nonempty label type with the required decidable equality, let $C:K\to\{0,1\}^{n}$ be injective, and let $0\le Q\le1/2$ . Define

s_Q(u,v;u',v') =\frac{1-2Q}{2}\mathbf1_{u=v}\mathbf1_{u'=v'} +\frac Q2\mathbf1_{u=u'}\mathbf1_{v=v'},\qquad \rho_Q((a,b),(a',b'))=\prod_{i=0}^{n-1}s_Q(a_i,b_i;a'_i,b'_i),

with real entries regarded as complex numbers, and define $B_{C,Q}((a,k),(a',l))=\rho_Q((a,C(k)),(a',C(l)))$ and $A_C(Q)=\sum_a\sum_k\operatorname{Re}\rho_Q((a,C(k)),(a,C(k)))$ . The theorem asserts that $\rho_Q$ is positive semidefinite with trace $1$ , that $B_{C,Q}$ is positive semidefinite, and that

\operatorname{tr}B_{C,Q}=\frac{|K|}{2^n}\quad\text{in }\mathbb C,\qquad A_C(Q)=\frac{|K|}{2^n}\quad\text{in }\mathbb R,\qquad A_C(Q)>0.

It further asserts, for every string $a$ and label $k$ , that the diagonal entry normalized by the real trace satisfies

\frac{\operatorname{Re}B_{C,Q}((a,k),(a,k))} {\operatorname{Re}\operatorname{tr}B_{C,Q}} = \frac{\operatorname{Re}\rho_Q((a,C(k)),(a,C(k)))}{A_C(Q)}.

Both endpoints $Q=0$ and $Q=1/2$ are included.

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