Operational parametrization and success probability of 1W-LOCC

Open

QAlgorithms.Papers.Independent.Intakethird100.P36.operational_parametrization

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

prove2quantum

Let $\rho_{a|x}$ be a positive, no-signaling finite-dimensional assemblage of common trace $t\le1$ . Bob first applies rectangular Kraus operators $K_w$ with $\sum_w K_w^\dagger K_w\le I$ . He communicates $w$ to Alice, who samples $x$ from a normalized law $P(x|x_f,w)$ , obtains the original output $a$ , and samples $a_f$ from a normalized law $P(a_f|a,x,w,x_f)$ . The resulting protocol has exactly the action

(M\rho)_{a_f|x_f}=\sum_{w,a,x}P(x|x_f,w)P(a_f|a,x,w,x_f)K_w\rho_{a|x}K_w^\dagger.

Its output is an assemblage. For each branch, the trace is $p_w=\operatorname{Tr}(K_w\rho_BK_w^\dagger)$ , independently of $x_f$ , where $\rho_B=\sum_a\rho_{a|x}$ . Consequently $\operatorname{Tr}M(\rho)=\sum_wp_w\le t$ ; equality holds for a complete Kraus family. The data specify the sequential protocol as well as its closed formula, providing the operational meaning of the parametrization.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P36

Formal statement

noncomputable section

open scoped BigOperators ENNReal ComplexConjugate ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P36

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

attribute [local instance] Classical.propDecidable

variable {d r s df rf sf m : ℕ}

/-- Section III and Appendix A, PDF pp.3–4,9–10, (9)–(12),(A6): the sequential
protocol has exactly the parametrized action and the stated success probability. -/
theorem operational_parametrization (P : SteeringProtocol d r s df rf sf m)
    (rho : AssemblageBlocks d r s) (hrho : IsAssemblage rho) :
    protocolAction P rho = oneWayFormula P rho ∧
    IsAssemblage (protocolAction P rho) ∧
    (∀ w xf, (∑ af, protocolBranch P rho w af xf).trace.re = steeringBranchProbability P rho w) ∧
    assemblageMass (protocolAction P rho) = ∑ w, steeringBranchProbability P rho w ∧
    assemblageMass (protocolAction P rho) ≤ assemblageMass rho ∧
    (P.Complete → assemblageMass (protocolAction P rho) = assemblageMass rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P36

end

Source

The resource theory of steering, arXiv:1409.5804v3, PDF p. 3, Section III, (9)–(12); Appendix A

Read-back

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

Let $d,r,s,d_f,r_f,s_f,m$ be natural numbers, and let $P$ have strictly positive $d,r,s,d_f,r_f,s_f$ , matrices $K_w\in\mathbb C^{d_f\times d}$ satisfying $I_d-\sum_{w<m}K_w^\dagger K_w\succeq0$ , probability distributions $\alpha_w(\,\cdot\mid x_f)$ on the $s$ input settings, and probability distributions $\beta_w(\,\cdot\mid a,x,x_f)$ on the $r_f$ output outcomes. Suppose the complex $d\times d$ matrix family $\rho_{a,x}$ has positive semidefinite blocks, setting-independent sums $\sum_a\rho_{a,x}$ , and mass $\mu=\operatorname{Re}\operatorname{tr}B\in[0,1]$ , where $B=s^{-1}\sum_x\sum_a\rho_{a,x}$ . Define

R^{(w)}_{a_f,x_f} =\sum_{x<s}\sum_{a<r} \beta_w(a_f\mid a,x,x_f)\alpha_w(x\mid x_f) K_w\rho_{a,x}K_w^\dagger,\qquad R=\sum_{w<m}R^{(w)},\qquad p_w=\operatorname{Re}\operatorname{tr}(K_wBK_w^\dagger).

Then $R$ equals the family whose $(a_f,x_f)$ block is $\sum_w\sum_a\sum_x\alpha_w(x\mid x_f)\beta_w(a_f\mid a,x,x_f)K_w\rho_{a,x}K_w^\dagger$ ; $R$ has positive semidefinite blocks, setting-independent outcome sums, and mass $\mu(R)\in[0,1]$ ; for every $w<m$ and $x_f<s_f$ , $\operatorname{Re}\operatorname{tr}(\sum_{a_f}R^{(w)}_{a_f,x_f})=p_w$ ; and $\mu(R)=\sum_wp_w\leq\mu$ . If additionally $\sum_wK_w^\dagger K_w=I_d$ , then $\mu(R)=\mu$ . Zero input mass is allowed, and $m=0$ gives zero output and empty branch sums.

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