Corollary 3: strict Renyi entropy increase below one half

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.renyi_canIncrease

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

prove2quantum

All Hilbert spaces are finite-dimensional complex spaces with fixed product bases and positive local dimensions. States are positive semidefinite operators of trace one; pure kets have norm one. A non-entangling map is completely positive and preserves the full separable positive cone. A channel is also trace preserving. For every $0\le\alpha<1/2$ , there exist bipartite pure states $\psi,\varphi$ and a non-entangling channel $\Lambda$ between their registers such that

\Lambda(\psi)=\varphi,\qquad E_\alpha(\varphi)>E_\alpha(\psi).

Here $E_\alpha$ is the base-two Renyi entropy of the squared Schmidt coefficients; $E_0$ is the logarithm of Schmidt rank.

This is deterministic pure-to-pure nonmonotonicity.

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)

/-- Corollary 3, PDF pp.9-10: deterministic pure-state Renyi nonmonotonicity
below one half. No average or stochastic interpretation is asserted. -/
theorem renyi_canIncrease (alpha : ℝ) (h0 : 0 ≤ alpha) (hhalf : alpha < 1 / 2) :
    ∃ a b c d : ℕ, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧
      ∃ psi : UnitBipartiteKet a b, ∃ phi : UnitBipartiteKet c d,
      ∃ L : Superop (Fin a × Fin b) (Fin c × Fin d),
        IsChannel L ∧ NE L ∧ L psi.rho = phi.rho ∧
        schmidtRenyi (ENNReal.ofReal alpha) psi.ket < schmidtRenyi (ENNReal.ofReal alpha) phi.ket := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 9, Corollary 3

Read-back

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

For every real $\alpha$ with $0\le\alpha<\frac12$ , there exist positive natural numbers $a,b,c,d$ , unit complex Euclidean vectors $\psi$ on the $a\times b$ bipartite system and $\phi$ on the $c\times d$ system, and a map $L$ between their matrix spaces that is a channel, has a finite Kraus representation, preserves every separable positive matrix, and satisfies

L(\psi\psi^\dagger)=\phi\phi^\dagger,\qquad H_\alpha(\psi)<H_\alpha(\phi).

Here a channel means $L(X)=\sum_jK_jXK_j^\dagger$ for a finite family with $\sum_jK_j^\dagger K_j=I$ ; a separable positive matrix means a finite sum of tensor products of positive semidefinite trace-one matrices with nonnegative weights, without requiring total weight one. For a vector $v$ on an $r\times s$ system, let $\lambda_0,\ldots,\lambda_{r-1}$ be the descending eigenvalues, with multiplicity, of the matrix $(\sum_{j<s}v(i,j)\overline{v(i',j)})_{i,i'}$ . The quantity in the displayed inequality is

H_\alpha(v)= \begin{cases} \log_2\#\{i:\lambda_i>0\},&\alpha=0,\\[1mm] \dfrac{\log_2\!\left(\sum_{i<r}\lambda_i^\alpha\right)}{1-\alpha}, &0<\alpha<\frac12, \end{cases}

using the total real logarithm and real-power operations of the code. In particular, the existential assertion includes the order $\alpha=0$ .

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