Pure tripartite entropy balance

Open

QAlgorithms.Papers.Independent.Intakethird100.P64.pureStateEntropyBalance

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

prove2quantum

Let $|\psi\rangle$ be a unit pure state on finite nonzero registers $R,A,B$ . For each subsystem $X$ , let $H(X)_\psi$ be the von Neumann entropy in bits of its reduced density matrix, and put $I(X;Y)_\psi=H(X)_\psi+H(Y)_\psi-H(XY)_\psi$ . Then

H(A)_\psi=\tfrac12 I(R;A)_\psi+\tfrac12 I(A;B)_\psi.

This identity determines how Alice's residual entropy divides between the two mutual-information rates in the feedback father calculation. Complementary entropy equalities are consequences of purity, not additional hypotheses.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P64

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P64

open QAlgorithms

open QAlgorithms.Papers.Independent.Gap48.P20
  (Copies redistributionMarginal subsystemEntropy forwardApply)

open QAlgorithms.Papers.Independent.Dependency50.P48 (densityPower)

open scoped Matrix ComplexConjugate

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.2, (8): the entropy balance of every normalized finite tripartite pure
state. Purity and normalization are provided by the vector and IsState, rather
than by assuming complementary entropy equalities. -/
theorem pureStateEntropyBalance {R A B : Type}
    [Fintype R] [Fintype A] [Fintype B] [Nonempty R] [Nonempty A] [Nonempty B]
    (psi : EuclideanSpace ℂ (R × (A × B))) (hpsi : IsState psi) :
    feedbackEntropyA psi = (1 / 2 : ℝ) * mutualRA psi + (1 / 2 : ℝ) * mutualAB psi := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P64

end

Source

A triangle of dualities: reversibly decomposable quantum channels, source-channel duality, and time reversal, arXiv:quant-ph/0505138v1, PDF p. 2, Equation (8): pure-state entropy balance

Read-back

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

For types $R,A,B$ equipped with finite enumerations and each nonempty, and every vector $\psi\in\mathbb C^{R\times(A\times B)}$ satisfying $\|\psi\|=1$ , form the matrix $\omega_{x,y}=\psi(x)\overline{\psi(y)}$ . For any selection $T$ of these registers, let $\omega_T$ be its reduced matrix, with entries obtained by summing $\psi(t,u)\overline{\psi(t',u)}$ over the complementary register coordinates $u$ , and write

H(T)=-\operatorname{Re}\operatorname{tr}f(\omega_T), \qquad f(x)=x\log_2x,

where $f(\omega_T)$ is defined by continuous functional calculus and the real logarithm is total, with $\log_2 0=0$ . The theorem asserts

H(A)= \frac12\bigl(H(R)+H(A)-H(RA)\bigr) +\frac12\bigl(H(A)+H(B)-H(AB)\bigr).

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