Section 2.2: product and split-middle equality cases

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.productSSAEquality

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

prove2quantum

For a faithful trace-one tripartite state, the SSA entropy gap and the logarithm condition vanish whenever

\rho_{123}=\rho_1\otimes\rho_{23}\quad\text{or}\quad\rho_{123}=\rho_{12}\otimes\rho_3.

In particular this includes a product of three marginal states. More generally, if subsystem $2$ is $2'\otimes2''$ , any faithful trace-one states $\alpha_{12'}$ and $\beta_{2''3}$ give equality for

\rho_{123}=\alpha_{12'}\otimes\beta_{2''3},

with canonical regrouping of the four factors. These are sufficient cases and are not claimed to exhaust equality.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P51

Formal statement

noncomputable section

open scoped Matrix ComplexOrder ComplexConjugate Matrix.Norms.L2Operator

open MeasureTheory

namespace QAlgorithms.Papers.Independent.Intakethird100.P51

attribute [local instance] Classical.propDecidable Classical.decEq

-- Exact interfaces from the frozen accepted library; no local redeclarations.

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

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

open QAlgorithms.Papers.Independent.Information100.P27 (average)

open QAlgorithms.Papers.Independent.Dependency50.P21 (relativeEntropy marginalAB channelAdjoint)

open QAlgorithms.Papers.Independent.Dependency50.P35 (marginalAC)

open QAlgorithms.Papers.Independent.Gap48.P19 (shannonNats)

open QAlgorithms.Papers.Independent.Gap48.P33 (measurementInformation)

section Statements

variable {A B C D J K O : Type}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D] [Fintype J] [Fintype K] [Fintype O]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

variable [DecidableEq J] [DecidableEq K] [DecidableEq O]

/-- Section 2.2, PDF p.7: all product and split-middle sufficient cases.
No tensor decomposition is asserted necessary. -/
theorem productSSAEquality [Nonempty A] [Nonempty B] [Nonempty C] [Nonempty D] :
    (∀ rho : Mat (A × (B × C)), FaithfulDensity rho →
      (rho = Matrix.kronecker (traceRight (marginalAB rho)) (traceLeft rho) ∨
       rho = liftAB (marginalAB rho) * liftBC (Matrix.kronecker (1 : Mat B)
         (traceLeft (traceLeft rho)))) → ssaGap rho = 0 ∧ SSAlogCondition rho) ∧
    (∀ X : Mat (A × B), ∀ Y : Mat (D × C), FaithfulDensity X → FaithfulDensity Y →
      ssaGap (splitProduct X Y) = 0 ∧ SSAlogCondition (splitProduct X Y)) := by sorry

end Statements

end QAlgorithms.Papers.Independent.Intakethird100.P51

end

Source

Inequalities for Quantum Entropy: A Review with Conditions for Equality, arXiv:quant-ph/0205064v2, PDF p. 7, Section 2.2: product and split-middle equality cases

Read-back

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

For finite nonempty index types $A,B,C,D$ , each with decidable equality, write $S(M)=-\operatorname{Re}\operatorname{tr}(f(M))$ , where $f(x)=x\log x$ is applied by continuous functional calculus and $\log$ is the natural logarithm, with its total-function value $\log 0=0$ . A faithful density matrix means a positive definite complex matrix of trace $1$ . For a matrix $\rho$ on $A\times(B\times C)$ , let $\rho_{AB},\rho_{BC},\rho_A,\rho_B,\rho_C$ denote the corresponding partial traces, and put $G(\rho)=S(\rho_{AB})+S(\rho_{BC})-S(\rho)-S(\rho_B)$ . Lift an $AB$ -matrix by tensoring with $I_C$ , a $BC$ -matrix by tensoring with $I_A$ , and a $B$ -matrix by inserting identities on $A,C$ . The assertion is the conjunction of two statements: every faithful density matrix $\rho$ satisfying either $\rho=\rho_A\otimes\rho_{BC}$ or $\rho=(\rho_{AB}\otimes I_C)(I_A\otimes I_B\otimes\rho_C)$ satisfies $G(\rho)=0$ and

\log\rho-\log\rho_{AB}\otimes I_C =I_A\otimes\log\rho_{BC}-I_A\otimes\log\rho_B\otimes I_C;

and, for every faithful density matrix $X$ on $A\times B$ and every faithful density matrix $Y$ on $D\times C$ , the matrix $Z$ on $A\times((B\times D)\times C)$ defined by $Z_{(a,(b,d),c),(a',(b',d'),c')}=X_{(a,b),(a',b')}Y_{(d,c),(d',c')}$ satisfies the same zero-gap and logarithmic identity, with $B\times D$ as its middle register. All these index types may have cardinality $1$ .

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