Relative entropy, Klein's inequality, subadditivity (K1-B.2) #
Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).
Glossary: https://glossary.constraintsurfacedynamics.com/entropy-subadditivity/
Plain-language, CSD-role and formal statements of entropy subadditivity, with
this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.
Glossary: https://glossary.constraintsurfacedynamics.com/von-neumann-entropy/
Plain-language, CSD-role and formal statements of the von Neumann entropy, with
this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.
On upstreaming: this is a Category 1 file. Strip this Glossary block before any
Mathlib or Physlib PR; a personal project link has no place in a canonical header.
This file delivers the quantum relative entropy D(ρ‖σ) = Tr(ρ log ρ) − Tr(ρ log σ),
Klein's inequality D(ρ‖σ) ≥ 0 (for positive-definite σ), the Kronecker-log operator
split log(ρ_A ⊗ ρ_B) = log ρ_A ⊗ I + I ⊗ log ρ_B (cfc_log_kronecker), and the von Neumann
subadditivity headline S(ρ_AB) ≤ S(ρ_A) + S(ρ_B) (vonNeumannEntropy_subadditive). This is
the K1-B.2 tranche of specs/k1-plan.md. It builds on the spectral von Neumann entropy of
Entropy.lean and the matrix partial trace of PartialTrace.lean.
The Kronecker-log operator split (the former K1-B.2 wall, now closed) #
The linchpin for subadditivity is cfc_log_kronecker:
log(ρ_A ⊗ ρ_B) = log ρ_A ⊗ I + I ⊗ log ρ_B (both factors positive-definite).
The proof routes through cfc_eq_conj_diagonal: if M = U · diagonal d · Uᴴ (U unitary, d
real) then hM.cfc f = U · diagonal (↑∘f∘d) · Uᴴ, proved via Lagrange interpolation of f
on the (finite) spectrum — hM.cfc f = aeval M q for an interpolating polynomial q, then aeval
conjugates through U and acts diagonally. This sidesteps the eigenvector-ambiguity / sorting
subtlety entirely (it holds for the W = U_A ⊗ U_B decomposition, not only the canonical
eigenvectorUnitary). Applied to ρ_A ⊗ ρ_B = W · diagonal(λ_A·λ_B) · Wᴴ
(kronecker_eq_conj_diagonal_eigenvalues), with the per-eigenvalue split
log(λ_A,i · λ_B,j) = log λ_A,i + log λ_B,j (positive-definite ⟹ all eigenvalues > 0) and
mul_kronecker_mul distribution, this gives the operator split. Subadditivity then follows
mechanically from klein_inequality at σ = ρ_A ⊗ ρ_B + the reduced-trace identities
trace_mul_kronecker_one_right/_left + re_trace_self_log.
The doubly-stochastic overlap matrix #
The technical core is the overlap matrix V = U_ρᴴ U_σ between the two eigenbases of ρ and
σ, with Dᵢⱼ = ‖Vᵢⱼ‖² doubly stochastic (overlapV_row_sum, overlapV_col_sum: rows and
columns of D sum to 1, from the unitarity Vᴴ V = V Vᴴ = 1). The cross-term spectral
expansion
Tr(ρ · cfc g σ) = ∑ᵢ ∑ⱼ pᵢ · g(qⱼ) · ‖Vᵢⱼ‖² (trace_mul_cfc_eq),
p/q the eigenvalues of ρ/σ, is the linchpin: it expresses the trace of a product of two
operators in different eigenbases through the doubly-stochastic overlap.
Klein's inequality (the positive-definite-σ form) #
Klein/relEntropy_nonneg is proved for σ positive-definite (all qⱼ > 0). Writing
∑ᵢ pᵢ log pᵢ = ∑ᵢⱼ ‖Vᵢⱼ‖² pᵢ log pᵢ (row stochasticity) and pairing against the cross term,
D(ρ‖σ) = ∑ᵢⱼ ‖Vᵢⱼ‖² · pᵢ · (log pᵢ − log qⱼ) ≥ ∑ᵢⱼ ‖Vᵢⱼ‖² (pᵢ − qⱼ) = 1 − 1 = 0,
where the entrywise bound pᵢ(log pᵢ − log qⱼ) ≥ pᵢ − qⱼ is the scalar Gibbs step
log(qⱼ/pᵢ) ≤ qⱼ/pᵢ − 1 (Real.log_le_sub_one_of_pos), and the final collapse uses both row
and column stochasticity. This route uses only the scalar log_le_sub_one, not a
concave-Jensen step, so it is robust at zero ‖Vᵢⱼ‖² weights and at pᵢ = 0.
Honest scope. The positive-definiteness of σ in Klein is load-bearing and not cosmetic:
with Mathlib's junk value Real.log 0 = 0, the finite expression Tr(ρ log ρ) − Tr(ρ log σ)
can be negative when supp ρ ⊄ supp σ (the genuine D(ρ‖σ) = +∞ case), so Klein's ≥ 0 is
false as stated without a support hypothesis; σ positive-definite is the standard clean
sufficient condition. Correspondingly vonNeumannEntropy_subadditive hypothesises the marginals
ρ_A = Tr_B ρ_AB, ρ_B = Tr_A ρ_AB positive-definite (so ρ_A ⊗ ρ_B is PD for the Klein
step), and only ρ_AB.PosSemidef + ρ_AB.trace = 1. It does NOT assume ρ_AB itself
positive-definite — that would exclude the physically important pure entangled states (where
S(ρ_AB) = 0 and the marginals are full-rank mixed), which the statement covers precisely when
the marginals are full-rank — a pure state has PD marginals iff its Schmidt rank equals BOTH
dimensions (equal-dimension, full-Schmidt-rank pure states in; rank-deficient or unequal-dimension
pure states out; scope sharpened 2026-08-06, CL-022 audit). The bound is genuinely an inequality on
correlated ρ_AB with PD marginals (equality only at product states), not a vacuous
product-state identity. The general singular-marginal case and Araki–Lieb
|S(ρ_A) − S(ρ_B)| ≤ S(ρ_AB) (which needs a purification construction) are deferred. See
specs/k1-plan.md for the ledger.
The overlap matrix and its double stochasticity #
The overlap matrix V = U_ρᴴ U_σ between the eigenvector unitaries of ρ and σ.
Its entries Vᵢⱼ = ⟨aᵢ, bⱼ⟩ are the inner products of the two eigenbases; ‖Vᵢⱼ‖² is the
doubly-stochastic overlap that mediates the cross term Tr(ρ log σ).
Equations
- QuantumInfo.overlapV hρ hσ = star ↑hρ.eigenvectorUnitary * ↑hσ.eigenvectorUnitary
Instances For
Vᴴ V = 1: the overlap matrix is unitary (left inverse).
V Vᴴ = 1: the overlap matrix is unitary (right inverse).
Row stochasticity: ∑ⱼ ‖Vᵢⱼ‖² = 1, from (V Vᴴ)ᵢᵢ = 1.
Column stochasticity: ∑ᵢ ‖Vᵢⱼ‖² = 1, from (Vᴴ V)ⱼⱼ = 1.
The cross-term spectral expansion #
Cyclic reduction: Tr(ρ · cfc g σ) = Tr(diag(p) · V · diag(g∘q) · Vᴴ), where
p/q are the eigenvalues of ρ/σ and V = overlapV. From the two spectral forms
ρ = U_ρ diag(p) U_ρᴴ, cfc g σ = U_σ diag(g∘q) U_σᴴ and trace cyclicity.
Diagonal expansion: Tr(diag(p) · V · diag(c) · Vᴴ) = ∑ᵢ ∑ⱼ pᵢ · cⱼ · ‖Vᵢⱼ‖².
The cross-term spectral expansion (headline):
Tr(ρ · cfc g σ) = ∑ᵢ ∑ⱼ pᵢ · g(qⱼ) · ‖Vᵢⱼ‖², combining the cyclic reduction and the diagonal
expansion.
The real part of the cross term: Re Tr(ρ · cfc g σ) = ∑ᵢ ∑ⱼ pᵢ · g(qⱼ) · ‖Vᵢⱼ‖².
Relative entropy and Klein's inequality #
The quantum relative entropy D(ρ‖σ) = Re Tr(ρ log ρ) − Re Tr(ρ log σ), defined on the
operator-trace form. With cfc Real.log σ = log σ, this is the standard
Tr(ρ log ρ − ρ log σ).
Equations
Instances For
The ρ log ρ self-term is the eigenvalue sum ∑ᵢ pᵢ log pᵢ (single eigenbasis):
Re Tr(ρ · cfc log ρ) = ∑ᵢ pᵢ log pᵢ. From re_trace_cfc at f = (x ↦ x log x) and
cfc_id_mul_log (the cfc ρ log ρ is cfc (x ↦ x log x) ρ).
Klein's inequality / relative-entropy non-negativity (positive-definite σ):
D(ρ‖σ) ≥ 0 for a density operator ρ and a positive-definite density σ.
σ positive-definite (qⱼ > 0) is load-bearing: see the file docstring — without a support
hypothesis the finite (junk-log 0) expression can be negative. The proof writes
D(ρ‖σ) = ∑ᵢⱼ ‖Vᵢⱼ‖² pᵢ (log pᵢ − log qⱼ) ≥ ∑ᵢⱼ ‖Vᵢⱼ‖² (pᵢ − qⱼ) = 0 via the scalar
Real.log_le_sub_one_of_pos and double stochasticity (both overlapV_row_sum and
overlapV_col_sum).
Klein's inequality (named form): Tr(ρ log ρ) ≥ Tr(ρ log σ) for a density ρ and a
positive-definite density σ. Equivalent to relEntropy_nonneg.
Partial-trace / Kronecker-identity trace lemmas (subadditivity prerequisites) #
The reduced-trace identities trace_mul_kronecker_one_right / trace_mul_one_kronecker_left
(Tr(M · (X ⊗ I)) = Tr(Tr_B(M) · X) and its mirror) were rehomed to PartialTrace.lean
(2026-08-20, the Q27 arc): the defining property of the partial trace lives beside the
definition, and the CV entangled-weights bridge consumes it without this module's entropy
stack. This module keeps consuming them through its public import of PartialTrace.
The Kronecker-log operator split (the former K1-B.2 wall) #
cfc_log_kronecker : log(ρ_A ⊗ ρ_B) = log ρ_A ⊗ I + I ⊗ log ρ_B, the operator identity that
turns subadditivity into a mechanical Klein-inequality application. The route is the
diagonalization-respecting cfc_eq_conj_diagonal helper (Lagrange-interpolation based) applied to
the Kronecker eigen-decomposition kronecker_eq_conj_diagonal_eigenvalues.
CFC of equal eigenvalue-actions agree. If f and g agree on every eigenvalue of ρ,
then hρ.cfc f = hρ.cfc g (the converse of cfc_eq_iff_on_eigenvalues). Trivial: the diagonals
↑∘f∘λ and ↑∘g∘λ coincide.
Each diagonal value of a unitary diagonalization is an eigenvalue. If
M = U · diagonal d · Uᴴ (U unitary, d real) then every d c equals some eigenvalue
hM.eigenvalues i. Via the charpoly root multiset: M.charpoly = ∏ (X − ↑(d c)) and the roots
are the eigenvalues, so each ↑(d c) is among them. The permutation-invariant route sidesteps
eigenvalue sorting.
aeval (↑r) q = ↑(eval r q) for a real polynomial q evaluated at (r : ℂ).
CFC respects a unitary diagonalization. If M = U · diagonal d · Uᴴ with U unitary
(star U * U = 1) and real d, then hM.cfc f = U · diagonal (↑∘f∘d) · Uᴴ. The proof routes
through Lagrange interpolation: a polynomial q matching f on the (finite) spectrum gives
hM.cfc f = aeval M q (cfc_polynomial), and aeval conjugates through U (aeval_algHom_apply
at the conjugation *-automorphism Unitary.conjStarAlgAut) and acts diagonally, so
aeval M q = U · diagonal (eval·q ∘ d) · Uᴴ = U · diagonal (↑∘f∘d) · Uᴴ since each d c is an
eigenvalue (eigenvalue_of_conj_diagonal ⟹ eval (d c) q = f (d c)). This holds for the
W = U_A ⊗ U_B decomposition, not only the canonical eigenvectorUnitary, which is what the
Kronecker split needs; it avoids the eigenvector-ambiguity / sorting subtlety entirely.
The Kronecker-log operator split: log(ρ_A ⊗ ρ_B) = log ρ_A ⊗ I + I ⊗ log ρ_B for two
positive-definite matrices. (log is the Hermitian functional calculus IsHermitian.cfc Real.log.) Genuinely the operator identity logρ_A ⊗ I + I ⊗ logρ_B, not a relabelling: it is
obtained from the eigen-decomposition ρ_A ⊗ ρ_B = W · diagonal(λ_A·λ_B) · Wᴴ
(W = U_A ⊗ U_B) via cfc_eq_conj_diagonal, the per-eigenvalue split
log(λ_A,i · λ_B,j) = log λ_A,i + log λ_B,j (positive-definite ⟹ λ > 0, Real.log_mul), and
mul_kronecker_mul distribution (with U_B · I · U_Bᴴ = I). The linchpin for subadditivity.
Von Neumann subadditivity: S(ρ_AB) ≤ S(ρ_A) + S(ρ_B) for a bipartite density operator
ρ_AB whose marginals ρ_A = Tr_B ρ_AB, ρ_B = Tr_A ρ_AB are positive-definite.
Hypotheses: ρ_AB.PosSemidef, ρ_AB.trace = 1, and (partialTraceRight ρ_AB).PosDef,
(partialTraceLeft ρ_AB).PosDef. ρ_AB is NOT assumed positive-definite — the statement
covers pure entangled states of full Schmidt rank (where S(ρ_AB) = 0, marginals full-rank mixed)
and every correlated ρ_AB whose marginals are PD (a correlated state with a singular marginal
is outside this form; scope sharpened 2026-08-06, CL-022 audit); the marginals-PD condition is what
the Klein step consumes (ρ_A ⊗ ρ_B PD). The bound
is a genuine inequality (equality only at product ρ_AB = ρ_A ⊗ ρ_B), not a product-state identity.
Proof: S(ρ_AB) = −Re Tr(ρ_AB log ρ_AB) ≤ −Re Tr(ρ_AB log(ρ_A⊗ρ_B)) by klein_inequality at
σ = ρ_A ⊗ ρ_B (PD via PosDef.kronecker); the Kronecker-log split cfc_log_kronecker rewrites
log(ρ_A⊗ρ_B) = logρ_A ⊗ I + I ⊗ logρ_B, and the reduced-trace identities
trace_mul_kronecker_one_right/_left collapse the two cross terms to Tr(ρ_A logρ_A),
Tr(ρ_B logρ_B), whose negatives are S(ρ_A), S(ρ_B).
Schmidt symmetry: equal marginal entropies of a pure bipartite state (Araki–Lieb 2a) #
The two reduced density operators of a pure bipartite state have equal von Neumann entropy.
The algebraic core is the cospectrum of M Mᴴ and Mᴴ M: they share the same nonzero
eigenvalues with multiplicity, so any spectral sum ∑ g(λ) with g 0 = 0 agrees across the two.
This is the entropy-side input to Araki–Lieb.
Cospectral spectral sums of M Mᴴ and Mᴴ M. For any rectangular M : Matrix n m ℂ and
any g : ℝ → ℝ with g 0 = 0, the spectral sums of g over the eigenvalues of M Mᴴ (size n)
and Mᴴ M (size m) coincide:
∑ᵢ g(λ(M Mᴴ)ᵢ) = ∑ⱼ g(λ(Mᴴ M)ⱼ).
Route (charpoly, multiset-of-roots, permutation-invariant): the rectangular charpoly identity
charpoly_mul_comm' gives X^|m| · (M Mᴴ).charpoly = X^|n| · (Mᴴ M).charpoly in ℂ[X]. Taking
roots of both (products of nonzero polynomials, roots_mul, roots_pow, roots_X) yields the
multiset identity replicate |m| 0 + roots((M Mᴴ).charpoly) = replicate |n| 0 + roots((Mᴴ M).charpoly).
Each roots(charpoly) = map (↑ ∘ eigenvalues) univ (roots_charpoly_eq_eigenvalues), so mapping by
g ∘ re and summing, the replicate _ 0 parts contribute g 0 = 0 and the eigenvalue sums equate.
Avoids matching Mathlib's sorted eigenvalues pointwise.
Equal charpoly ⟹ equal spectral sums. Two Hermitian matrices (of possibly different index
types) with the same characteristic polynomial have equal spectral sums ∑ g(λ). Via the root
multisets (roots_charpoly_eq_eigenvalues): equal charpoly ⟹ equal root multiset ⟹ equal mapped
sum. Used to transfer entropy across the transpose (Mᴴ M)ᵀ (charpoly_transpose).
PosDef transfers across equal charpoly. Two Hermitian matrices with the same charpoly: if
one is positive-definite (all eigenvalues > 0) so is the other. The eigenvalue multisets agree
(roots_charpoly_eq_eigenvalues); positivity of every element is a multiset property, so it
transfers. Used to derive ρ_R positive-definite from ρ_AB positive-definite (cospectral).
Entropy is independent of the Hermitian witness. Two IsHermitian proofs of the same
matrix give the same entropy (the eigenvalue values are matrix-determined; equal charpoly with
rfl).
Entropy is invariant under reindexing. S(reindex e e ρ) = S(ρ) for any e : n ≃ k:
reindexing is a permutation similarity, so charpoly_reindex + spectral_sum_eq_of_charpoly_eq.
The reassociation hinge for the Araki–Lieb tripartite cuts.
Schmidt symmetry of pure-state marginal entropies (Araki–Lieb 2a) #
The pure bipartite density ρψ = |ψ⟩⟨ψ| of ψ : (n × m) → ℂ, as a matrix:
ρψ p q = ψ p * conj (ψ q).
Equations
- QuantumInfo.pureDensity ψ = Matrix.vecMulVec ψ (star ψ)
Instances For
Right marginal of a pure state is M Mᴴ: Tr_B |ψ⟩⟨ψ| = M Mᴴ with M = pureMatrix ψ.
(Tr_B ρψ) i j = ∑ₖ ψ(i,k) conj(ψ(j,k)) = ∑ₖ M i k · conj(M j k) = (M Mᴴ) i j.
Left marginal of a pure state is (Mᴴ M)ᵀ: Tr_A |ψ⟩⟨ψ| = (Mᴴ M)ᵀ with M = pureMatrix ψ.
(Tr_A ρψ) k l = ∑ᵢ ψ(i,k) conj(ψ(i,l)) = ∑ᵢ M i k conj(M i l) = (Mᴴ M) l k = ((Mᴴ M)ᵀ) k l.
The pure density |ψ⟩⟨ψ| is Hermitian.
Schmidt symmetry (Araki–Lieb 2a): the two reduced density operators of a pure bipartite
state |ψ⟩⟨ψ| have equal von Neumann entropy:
S(Tr_B |ψ⟩⟨ψ|) = S(Tr_A |ψ⟩⟨ψ|).
Stated on the canonical Hermitian witnesses partialTrace{Right,Left}_isHermitian of the
Hermitian pure density (pureDensity_isHermitian). Genuine content: the right marginal is M Mᴴ,
the left marginal is (Mᴴ M)ᵀ (partialTraceRight_pureDensity / partialTraceLeft_pureDensity);
M Mᴴ and Mᴴ M are cospectral on their nonzero eigenvalues
(spectral_sum_mul_conjTranspose_comm, with negMulLog 0 = 0), and transpose preserves the
spectrum (charpoly_transpose via spectral_sum_eq_of_charpoly_eq). No unit-norm hypothesis is
needed for the entropy equality (it holds for every ψ); the unit condition only makes the
marginals genuine densities.
Purification of a density operator (Araki–Lieb 2b) #
The Hermitian square root √ρ := cfc Real.sqrt ρ of a Hermitian matrix. For PSD ρ
(eigenvalues ≥ 0) it satisfies √ρ · √ρ = ρ (sqrtMat_mul_self) and is itself Hermitian.
Equations
- QuantumInfo.sqrtMat hρ = hρ.cfc Real.sqrt
Instances For
√ρ is Hermitian (the cfc of a real function is Hermitian).
√ρ · √ρ = ρ for PSD ρ: √λ · √λ = λ on the (nonneg) spectrum, via cfc_mul + cfc_id.
Purification (Araki–Lieb 2b). Every density operator ρ : Matrix (n×m) (n×m) ℂ is the right
marginal of a pure state on (n×m) ⊗ (n×m) (a copy of the system as ancilla): there is a unit
ψ : ((n×m) × (n×m)) → ℂ with partialTraceRight (pureDensity ψ) = ρ. The purifying vector is
ψ = vec(√ρ) (pureMatrix ψ = √ρ); then partialTraceRight (pureDensity ψ) = √ρ · (√ρ)ᴴ = √ρ · √ρ = ρ, and ∑‖ψ‖² = Tr((√ρ)ᴴ √ρ) = Tr ρ = 1.
Araki–Lieb triangle inequality (2c) #
|S(ρ_A) − S(ρ_B)| ≤ S(ρ_AB). Route: purify ρ_AB to a pure Ψ on (AB) ⊗ R with R ≅ AB
(exists_purification); for the pure global state the A | (BR) cut gives S(ρ_A) = S(ρ_BR)
(Schmidt symmetry on the reshaped Ψ' : n × (m × R)); subadditivity on ρ_BR (split B | R)
gives S(ρ_BR) ≤ S(ρ_B) + S(ρ_R), and the AB | R cut gives S(ρ_R) = S(ρ_AB); hence
S(ρ_A) ≤ S(ρ_B) + S(ρ_AB). The symmetric A ↔ B swap closes the absolute value.
The reshape marginal identities are direct index computations (no abstract reassociation of the
partial trace). The subadditivity step requires the B- and R-marginals positive-definite;
ρ_R is cospectral with ρ_AB, so this routes through ρ_AB.PosDef.
A-marginal via the A | BR reshape = double right partial trace.
Tr_{BR} |Ψ'⟩⟨Ψ'| = Tr_B (Tr_R |Ψ⟩⟨Ψ|) = ρ_A. Direct index computation:
both equal (a, a') ↦ ∑_{b,r} Ψ((a,b),r) conj Ψ((a',b),r).
R-marginal of ρ_BR (trace out B) = ρ_R = Tr_A (Tr_B |Ψ⟩⟨Ψ|) reassociated. Here
ρ_R = Tr_{AB} |Ψ⟩⟨Ψ| is partialTraceLeft (pureDensity Ψ) (trace out the whole AB first
factor). Direct index computation: both equal (r, r') ↦ ∑_{a,b} Ψ((a,b),r) conj Ψ((a,b),r').
Cospectrum of the two pure marginals (charpoly form). For a pure state on (n×m) ⊗ (n×m)
(both factors equal-dimensional), the right and left marginals have equal characteristic
polynomial: partialTraceRight = M Mᴴ, partialTraceLeft = (Mᴴ M)ᵀ, and for square M,
(M Mᴴ).charpoly = (Mᴴ M).charpoly (charpoly_mul_comm), with charpoly_transpose. The
equal-dimension square case is the one purification produces (R ≅ AB).
Araki–Lieb, one side: S(ρ_A) ≤ S(ρ_B) + S(ρ_AB) for ρ_AB positive-definite with the
B-marginal positive-definite. Purify, use Schmidt symmetry on the A | BR cut
(S(ρ_A) = S(ρ_BR)), subadditivity on ρ_BR (S(ρ_BR) ≤ S(ρ_B) + S(ρ_R), needs ρ_B, ρ_R
PD), and S(ρ_R) = S(ρ_AB) (the AB | R cut). ρ_R PD is derived from ρ_AB PD by cospectrum
(posDef_of_charpoly_eq).
Araki–Lieb triangle inequality |S(ρ_A) − S(ρ_B)| ≤ S(ρ_AB) for a positive-definite
bipartite density ρ_AB with both marginals ρ_A = Tr_B ρ_AB, ρ_B = Tr_A ρ_AB
positive-definite. Genuine, non-vacuous content for correlated full-rank ρ_AB (equality
only at product states; S(ρ_A) − S(ρ_B) is generically nonzero). Two applications of
araki_lieb_one_side (the second to the index-swapped state ρ_BA, whose marginals are ρ_B,
ρ_A and whose entropy equals S(ρ_AB) by reindexing).
Honest scope. The ρ_AB positive-definite hypothesis is load-bearing: the purification route
runs subadditivity on the B | R bipartition, which (via vonNeumannEntropy_subadditive) needs
the ancilla marginal ρ_R positive-definite, and ρ_R is cospectral with ρ_AB. The
pure-entangled case (S(ρ_AB) = 0, marginals full-rank) is therefore not covered by this
form (it is the boundary S(ρ_A) = S(ρ_B) there); extending to singular ρ_AB needs a
limiting / support-restriction argument. The bound is nonetheless a true inequality on correlated
full-rank states, not a product-state identity.