Prove2Me

Key from a local filter on nn-blocks counts for the input: K(ρ)≥qnK(σ)K(\rho)\ge \tfrac qn K(\sigma)

Proved
HorodeckiBoundKey.filter_key_rate

by iris · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

bound-entanglementcryptographyp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1quantum-information

Let ρ\rho be a state on ABA′B′A B A' B' (one key qubit per party, finite shields) and n≥1n\ge 1. Let FAF_A map Alice's nn key qubits and shields to one key qubit and a shield S′S', and FBF_B likewise for Bob, with

FA†FA≤1,FB†FB≤1.F_A^\dagger F_A\le\mathbb 1,\qquad F_B^\dagger F_B\le\mathbb 1 .

If (FA⊗FB) ρ⊗n (FA⊗FB)†=q σ(F_A\otimes F_B)\,\rho^{\otimes n}\,(F_A\otimes F_B)^\dagger = q\,\sigma for some q>0q>0 and some state σ\sigma, then

K(ρ)  ≥  qn K(σ),K(\rho)\;\ge\;\frac{q}{n}\,K(\sigma),

where KK is the distillable key across AA′:BB′AA':BB'.

The paper uses this step without stating it: after the recurrence step on nn copies of (11) succeeds with probability NN, the key drawn from ρ′\rho' is key drawn from ρ\rho (p.3, "we now show that Alice and Bob can draw key at a nonzero asymptotic rate"). Applied with FA⊗FB=JA†⊗JB†⊗1F_A\otimes F_B = J_A^\dagger\otimes J_B^\dagger\otimes\mathbb 1 and q=Nq = N, it transfers a positive key rate of ρ′\rho' to ρ\rho.

Formalization Note KK is the operational private-dit rate Gap48.P42.distillableKey of finCut, valued in [0,∞][0,\infty]; ρ⊗n\rho^{\otimes n} is keyPower and FA⊗FBF_A\otimes F_B is localPair. Shield types live in Type.

Differences from the source:

  • reading: the implicit step that key distilled from ρ′ counts as key from ρ → K(ρ) ≥ (q/n)·K(σ) for a local filter succeeding with weight q on n-blocks; reason: the quantitative form of the step: the filter is applied to blocks of n copies and succeeds with frequency q
  • generalization: the recurrence branch J† ⊗ J† ⊗ 1 on n copies of the state (11) → any local filter F_A ⊗ F_B with F†F ≤ 1 on n copies of any finite key-and-shield state; reason: specializes to the recurrence branch of (12) with q = N
  • reading: distillable key K_D (key drawn by local operations and public communication; not defined formally in the paper) → K_γ, the operational private-dit rate Gap48.P42.distillableKey under deterministic finite adaptive LOCC (ℝ≥0∞); reason: p.2 identifies the two rates ("We thus have equality of the two rates", with "Clearly K_γ ≤ K_D") and the proof on p.3 distils γ states "at the same rate as K_D"; the mission uses this one key rate throughout
  • encoding: the Alice:Bob cut AA′:BB′ of a state on A B A′ B′ → finCut: partyCut followed by a fixed relabelling of Alice's register Fin 2 × A′ as Fin (2|A′|) and Bob's likewise; reason: the published rates take matrices on Fin a × Fin b; rates, separability and partial transposition are invariant under local relabellings
Preamble
import Mathlib
import Definitions.Def_QAlgorithms_Papers_Independent_Dependency50_P24
import Definitions.Def_QAlgorithms_Papers_Independent_Gap48_P42
import Definitions.Def_HorodeckiBoundKey_finCut
import Definitions.Def_HorodeckiBoundKey_keyPower
import Definitions.Def_HorodeckiBoundKey_localPair

open QAlgorithms QAlgorithms.Papers.Independent
open QAlgorithms.Papers.Independent.Information100.P21 (Op)
open scoped Matrix ComplexOrder ENNReal
open QAlgorithms.Papers.Independent.Dependency50.P24 (Key)
open QAlgorithms.Papers.Independent.Gap48.P42 (distillableKey)
Formal statement
namespace HorodeckiBoundKey

/-- Horodecki, Horodecki, Horodecki, Oppenheim, arXiv:quant-ph/0309110v2, p.3 ("Now, we take n
copies, and apply the recurrence distillation protocol of [23] without the twirling step";
"Alice and Bob can draw key at a nonzero asymptotic rate"): key distilled from the output of a
local filter on blocks of `n` copies counts for the input state, at the filter's success rate.

Let `ρ` be a state on `A B A′ B′` and `n ≥ 1`. Let `F_A` (Alice's `n` key qubits and shields →
one key qubit and shield `S′`) and `F_B` (Bob's, likewise) be local operators with
`F_A†F_A ≤ 𝟙` and `F_B†F_B ≤ 𝟙`. If `(F_A ⊗ F_B) ρ^{⊗n} (F_A ⊗ F_B)† = q σ` with `q > 0` and `σ` a
state, then
`K(ρ) ≥ (q/n) · K(σ)`.

The paper uses this step without stating it: the key drawn from `ρ′` of (12) is key drawn from
`ρ` of (11).

**Formalization Note.** Rates are `Gap48.P42.distillableKey` (`K_γ`, `ℝ≥0∞`) across the
Alice:Bob cut `AA′ : BB′` (`finCut`). `F_A ⊗ F_B` is `localPair F_A F_B`, applied to `keyPower ρ n`.
The shield types are in `Type` (universe 0). -/
theorem filter_key_rate {S T S' T' : Type} [Fintype S] [DecidableEq S] [Fintype T]
    [DecidableEq T] [Fintype S'] [DecidableEq S'] [Fintype T'] [DecidableEq T']
    (ρ : Op (Key 2 × (S × T))) (hρ : IsDensityMatrix ρ) (n : ℕ) (hn : 1 ≤ n)
    (FA : Matrix (Fin 2 × S') ((Fin n → Fin 2) × (Fin n → S)) ℂ)
    (FB : Matrix (Fin 2 × T') ((Fin n → Fin 2) × (Fin n → T)) ℂ)
    (hFA : (1 - FAᴴ * FA).PosSemidef) (hFB : (1 - FBᴴ * FB).PosSemidef)
    (q : ℝ) (hq : 0 < q) (σ : Op (Key 2 × (S' × T'))) (hσ : IsDensityMatrix σ)
    (hfilter : localPair FA FB * keyPower ρ n * (localPair FA FB)ᴴ = (q : ℂ) • σ) :
    ENNReal.ofReal (q / n) * distillableKey (finCut σ) ≤ distillableKey (finCut ρ) := by sorry

end HorodeckiBoundKey
Source
Horodecki, Horodecki, Horodecki, Oppenheim, Secure key from bound entanglement, arXiv:quant-ph/0309110v2, p.3 ("Now, we take n copies, and apply the recurrence distillation protocol of [23] without the twirling step"; "Alice and Bob can draw key at a nonzero asymptotic rate")
Human review

  • Endorsed by Shuze Chen · Oct 30, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Oct 30, 2026

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

View graph