Appendix A: explicit parameters for dually non-entangling conversion

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.appendix_parameters

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

prove2quantum

Let $k,d\ge2$ be integers and set $\delta=d^{-4}$ and $\epsilon=d^{-12}$ . Then $0<\delta,\epsilon<1$ , and both inequalities hold:

1-\delta\le\frac1{1+\frac{d^2}{\sqrt{d-1}}\sqrt{(1-\epsilon)\epsilon}},\qquad d^2(1-\epsilon)\le1+\frac{\sqrt{k-1}}{\sqrt{(1-\delta)\delta}}.

These are the explicit constructed parameter values in Theorem 9.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P19

Formal statement

noncomputable section

open QAlgorithms QAlgorithms.Entanglement Filter

open scoped Matrix ComplexOrder ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P19

open QAlgorithms.Papers.Independent.Information100.P21 (Op FiniteLOCC)

open QAlgorithms.Papers.Independent.Information100.P19 (Bip)

open QAlgorithms.Papers.Independent.Information100.P69 (CP)

open QAlgorithms.Papers.Independent.Information100.P71 (supportPower SupportIncluded)

open QAlgorithms.Papers.Independent.Dependency50.P19 (epr)

/-- Appendix A, PDF pp.33-34 (parameters used on p.12): the constructed
values delta=d^(-4), epsilon=d^(-12) satisfy both (10) and (11). -/
theorem appendix_parameters (k d : ℕ) (hk : 2 ≤ k) (hd : 2 ≤ d) :
    let delta := ((d : ℝ) ^ 4)⁻¹
    let epsilon := ((d : ℝ) ^ 12)⁻¹
    0 < delta ∧ delta < 1 ∧ 0 < epsilon ∧ epsilon < 1 ∧
      1 - delta ≤ 1 / (1 + (d : ℝ) ^ 2 / Real.sqrt ((d : ℝ) - 1) *
        Real.sqrt ((1 - epsilon) * epsilon)) ∧
      (d : ℝ) ^ 2 * (1 - epsilon) ≤
        1 + Real.sqrt ((k : ℝ) - 1) / Real.sqrt ((1 - delta) * delta) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 12, appendix-a-parameters

Read-back

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

For every pair of natural numbers $k,d$ satisfying $k\ge2$ and $d\ge2$ , set $\delta=d^{-4}$ and $\epsilon=d^{-12}$ , with these expressions evaluated in the real numbers. Then

0<\delta<1,\qquad 0<\epsilon<1,

and both inequalities

1-\delta \le \frac{1}{ 1+\dfrac{d^2}{\sqrt{d-1}}\sqrt{(1-\epsilon)\epsilon} }, \qquad d^2(1-\epsilon) \le 1+\frac{\sqrt{k-1}}{\sqrt{(1-\delta)\delta}}

hold. There is no assumed ordering between $k$ and $d$ , and the hypotheses make all displayed denominators positive.

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