Strong subadditivity (K1-C): the conditional reduction and the isolated wall

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

Strong subadditivity (SSA, Lieb–Ruskai) is the inequality

S(ρ_ABC) + S(ρ_B) ≤ S(ρ_AB) + S(ρ_BC)

for a tripartite density operator ρ_ABC on (a × b × c). Every standard proof rests on a deep operator-convexity input — Lieb's concavity theorem, joint convexity of the quantum relative entropy (ρ,σ) ↦ D(ρ‖σ), or, equivalently, monotonicity of relative entropy under partial trace (DPI) D(Tr_C ρ ‖ Tr_C σ) ≤ D(ρ ‖ σ). Mathlib does not have any of these (see the scout note at the end of this docstring).

What this file delivers (honest scope)

This is the LF3-bundle pattern applied at the K1 layer: everything is proved except one named deep hypothesis, which is genuinely the standard Lieb/DPI input.

1. Tripartite marginals (rhoAB, rhoBC, rhoB, rhoA, rhoC) via the bipartite partialTraceRight/partialTraceLeft of PartialTrace.lean, with the consistency identities rhoB_eq_traceA_AB, rhoB_eq_traceC_BC, partialTraceLeft_rhoAB_eq etc. proved by direct index computation (the auditor's reindexing probe).

2. The mutual-information identity relEntropy_kronecker_eq_entropy_sub: for a bipartite density ρ on x × y with both marginals positive-definite,

   D(ρ ‖ ρ_X ⊗ ρ_Y) = S(ρ_X) + S(ρ_Y) − S(ρ).

   This is the genuine algebraic content — cfc_log_kronecker (the Kronecker-log split) plus the reduced-trace identities trace_mul_kronecker_one_right/_left — extracted into a reusable lemma. Proved unconditionally (no deep input).

3. The conditional reduction strong_subadditivity_of_relEntropy_monotone: SSA derived from DPI stated as an explicit hypothesis hDPI. The reduction is genuine — SSA really follows, in the correct direction, non-vacuously for correlated ρ_ABC — via I(A:BC) ≥ I(A:B) ⟺ D(ρ_ABC ‖ ρ_A⊗ρ_BC) ≥ D(ρ_AB ‖ ρ_A⊗ρ_B), which is exactly DPI applied to tracing out C from the second party (ρ_ABC ↦ ρ_AB, ρ_A⊗ρ_BC ↦ ρ_A⊗ρ_B). Both relative entropies are rewritten by the mutual-information identity into the four von Neumann entropies.

The precise wall (the deep input we did NOT discharge)

The hypothesis hDPI is the data-processing inequality for quantum relative entropy under the partial trace — equivalently joint convexity of D(·‖·) or Lieb's concavity of (A,B) ↦ Tr exp(log A + log B). A scout of Mathlib HEAD (2026-06-17) finds:

• Operator MONOTONICITY (single-variable Löwner order) IS present: CFC.log_monotoneOn / CFC.log_le_log (log is operator monotone), CFC.monotone_rpow / CFC.monotone_nnrpow / CFC.sqrt_le_sqrt (x^p operator monotone for p ∈ [0,1]), and the integral-representation scaffold …/Rpow/IntegralRepresentation.lean.
• Operator CONCAVITY of log and x^p IS present (re-probed 2026-08-30 at the pin; the 2026-06-17 scout above predates it): CFC.concaveOn_log and CFC.concaveOn_nnrpow / CFC.concaveOn_rpow (p ∈ [0,1]) are proved upstream in Analysis/SpecialFunctions/ContinuousFunctionalCalculus/{ExpLog,Rpow}/Order.lean. They are stated for [CStarAlgebra A], which Matrix n n ℂ satisfies under the scoped instance Matrix.instCStarAlgebra (open scoped Matrix.Norms.L2Operator) — not the default one. Upstream's remaining TODO there is x ↦ x log x operator convex.
• What is still absent: no OperatorConvex/OperatorMonotone predicate, no Lieb / Ando / Epstein / Effros perspective / Wigner–Yanase, no joint convexity of any trace functional, and no DPI / monotonicity of relative entropy anywhere in Mathlib (its only DPI is classical, InformationTheory/KullbackLeibler/DataProcessing.lean).

So the minimal missing Mathlib lemma is joint convexity of (ρ,σ) ↦ D(ρ‖σ) (or its DPI form). The realistic build is the operator-convexity stratum: an OperatorConvexOn predicate on the Löwner order, the integral / Löwner-matrix route to operator convexity of −log and x ↦ x log x, the perspective-function joint-convexity lift, and the partial-trace DPI corollary. That is a genuine multi-week infrastructure build (the Rpow/IntegralRepresentation scaffold already in Mathlib is the template, but it only handles p ∈ (0,1) monotonicity, not convexity and not the two-variable perspective). The fork (build Lieb vs. axiom-state SSA) is the user's; this file isolates the wall as hDPI and does not paper it.

No axiom, no sorry. Foundational-triple-only on everything that lands. See specs/k1-plan.md §K1-C for the ledger.

The mutual-information identity (the genuine algebraic content, unconditional)

For a bipartite density ρ on x × y whose marginals ρ_X = Tr_Y ρ, ρ_Y = Tr_X ρ are positive-definite, the relative entropy against the product of marginals is the mutual information:

D(ρ ‖ ρ_X ⊗ ρ_Y) = S(ρ_X) + S(ρ_Y) − S(ρ).

This is the cfc_log_kronecker split + reduced-trace identities, the same machinery as vonNeumannEntropy_subadditive, extracted as a reusable identity (not an inequality).

theorem QuantumInfo.relEntropy_kronecker_eq_entropy_sub {x : Type u_4} {y : Type u_5} [Fintype x] [Fintype y] [DecidableEq x] [DecidableEq y] {ρ : Matrix (x × y) (x × y) ℂ} (hpsd : ρ.PosSemidef) (hpdX : (partialTraceRight ρ).PosDef) (hpdY : (partialTraceLeft ρ).PosDef) : relEntropy ⋯ ⋯ = vonNeumannEntropy ⋯ + vonNeumannEntropy ⋯ - vonNeumannEntropy ⋯

Mutual-information identity. For a bipartite density ρ on x × y with both marginals ρ_X = partialTraceRight ρ and ρ_Y = partialTraceLeft ρ positive-definite,

D(ρ ‖ ρ_X ⊗ ρ_Y) = S(ρ_X) + S(ρ_Y) − S(ρ).

Proof: D = Re Tr(ρ log ρ) − Re Tr(ρ · log(ρ_X⊗ρ_Y)). The first term is −S(ρ) (vonNeumannEntropy_eq_neg_re_trace_mul_log + cfc_id_mul_log). The second is split by the Kronecker-log operator identity cfc_log_kronecker (log(ρ_X⊗ρ_Y) = logρ_X ⊗ I + I ⊗ logρ_Y, both factors PD) and collapsed by the reduced-trace identities trace_mul_kronecker_one_right/ _left to Tr(ρ_X logρ_X) + Tr(ρ_Y logρ_Y) = −S(ρ_X) − S(ρ_Y). Unconditional — no deep operator-convexity input.

Tripartite marginals

With Lean's right-associated a × b × c = a × (b × c), the three two-party marginals are read off the bipartite partial traces, modulo one reindexing for the AB | C cut. We work with the convention that ρ : Matrix (a × b × c) (a × b × c) ℂ. Then:

• rhoBC := partialTraceLeft ρ (trace out A, the first a-factor) — a Matrix (b × c) (b × c);
• rhoAB := partialTraceRight (reindexAssoc ρ) (regroup to (a × b) × c, trace out C) — a Matrix (a × b) (a × b);
• rhoB := partialTraceLeft rhoAB = partialTraceRight rhoBC (the two readings agree, rhoB_consistency);
• rhoA := partialTraceRight ρ (trace out BC), rhoC := partialTraceLeft rhoBC.

The reassociation e : (a × b × c) ≃ ((a × b) × c) is Equiv.prodAssoc-inverse; entropy is invariant under it (vonNeumannEntropy_reindex) and trace/PD transfer by reindex.

def QuantumInfo.assocE {a : Type u_1} {b : Type u_2} {c : Type u_3} : a × b × c ≃ (a × b) × c

The reassociation equivalence (a × b × c) ≃ ((a × b) × c) (Lean's a × b × c is a × (b × c)). The AB | C cut needs the left-associated grouping.

Equations

• QuantumInfo.assocE = (Equiv.prodAssoc a b c).symm

noncomputable def QuantumInfo.reassocABC {a : Type u_1} {b : Type u_2} {c : Type u_3} (ρ : Matrix (a × b × c) (a × b × c) ℂ) : Matrix ((a × b) × c) ((a × b) × c) ℂ

The AB | C regrouping of ρ_ABC as a matrix on (a × b) × c.

Equations

• QuantumInfo.reassocABC ρ = (Matrix.reindex QuantumInfo.assocE QuantumInfo.assocE) ρ

noncomputable def QuantumInfo.rhoAB {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) : Matrix (a × b) (a × b) ℂ

ρ_AB := Tr_C ρ_ABC, the A,B marginal (trace out the c-factor after regrouping).

Equations

• QuantumInfo.rhoAB ρ = QuantumInfo.partialTraceRight (QuantumInfo.reassocABC ρ)

noncomputable def QuantumInfo.rhoBC {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] (ρ : Matrix (a × b × c) (a × b × c) ℂ) : Matrix (b × c) (b × c) ℂ

ρ_BC := Tr_A ρ_ABC, the B,C marginal (trace out the leading a-factor).

Equations

• QuantumInfo.rhoBC ρ = QuantumInfo.partialTraceLeft ρ

noncomputable def QuantumInfo.rhoA {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype b] [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) : Matrix a a ℂ

ρ_A := Tr_{BC} ρ_ABC (trace out the (b × c) factor).

Equations

• QuantumInfo.rhoA ρ = QuantumInfo.partialTraceRight ρ

noncomputable def QuantumInfo.rhoB {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) : Matrix b b ℂ

ρ_B := Tr_{AC} ρ_ABC, read as Tr_A (Tr_C ρ) = Tr_A ρ_AB.

Equations

• QuantumInfo.rhoB ρ = QuantumInfo.partialTraceLeft (QuantumInfo.rhoAB ρ)

Marginal index identities (the reindexing the auditor probes)

theorem QuantumInfo.rhoAB_apply {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) (i j : a × b) : rhoAB ρ i j = ∑ k : c, ρ (i.1, i.2, k) (j.1, j.2, k)

ρ_AB i j = ∑_c ρ ((i.1, i.2, k)) ((j.1, j.2, k)): explicit entry of the AB-marginal.

theorem QuantumInfo.rhoBC_apply {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] (ρ : Matrix (a × b × c) (a × b × c) ℂ) (i j : b × c) : rhoBC ρ i j = ∑ k : a, ρ (k, i.1, i.2) (k, j.1, j.2)

ρ_BC (b,c) (b',c') = ∑_a ρ (a,b,c) (a,b',c'): explicit entry of the BC-marginal.

theorem QuantumInfo.rhoA_apply {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype b] [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) (i j : a) : rhoA ρ i j = ∑ k : b × c, ρ (i, k.1, k.2) (j, k.1, k.2)

ρ_A consistency: Tr_C ρ_BC = ρ_A (= Tr_{BC} ρ). partialTraceRight (partialTraceLeft ρ) ((on b)) = partialTraceRight ρ. Both equal (i,j) ↦ ∑_{k:a} ∑_{l:b} ρ (k, ?, ?) …; here ρ_A i j = ∑_{(b,c)} ρ (i,b,c) (j,b,c). We instead record the Tr_{BC} reading directly used downstream.

theorem QuantumInfo.rhoB_consistency {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) : rhoB ρ = partialTraceRight (rhoBC ρ)

ρ_B consistency (B via AB vs via BC). Tr_A (Tr_C ρ) = Tr_C (Tr_A ρ), i.e. rhoB ρ = partialTraceRight (rhoBC ρ): the B-marginal computed by tracing A then C (partialTraceLeft (rhoAB ρ), which is rhoB ρ by definition) equals the B-marginal of ρ_BC computed by tracing C (partialTraceRight (rhoBC ρ)). Both equal (i,j) ↦ ∑_{k:a} ∑_{l:c} ρ (k, i, l) (k, j, l).

Marginal density / positivity transfer

The AB-marginal is a density (PSD + unit trace) when ρ_ABC is; likewise BC. The reassociation preserves PSD/trace. The B-marginal is then a density. PD of the various sub-marginals is carried as a hypothesis at the SSA statement (it is the standard support condition; see Subadditivity.lean honesty notes).

theorem QuantumInfo.reassocABC_trace {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] [Fintype b] [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) : (reassocABC ρ).trace = ρ.trace

The reassociation preserves the trace.

theorem QuantumInfo.reassocABC_posSemidef {a : Type u_1} {b : Type u_2} {c : Type u_3} {ρ : Matrix (a × b × c) (a × b × c) ℂ} (hpsd : ρ.PosSemidef) : (reassocABC ρ).PosSemidef

The reassociation preserves PosSemidef (it is a permutation similarity).

theorem QuantumInfo.rhoAB_trace {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] [Fintype b] [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) : (rhoAB ρ).trace = ρ.trace

Tr ρ_AB = Tr ρ_ABC.

theorem QuantumInfo.rhoBC_trace {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] [Fintype b] [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) : (rhoBC ρ).trace = ρ.trace

Tr ρ_BC = Tr ρ_ABC.

theorem QuantumInfo.rhoAB_posSemidef {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] [Fintype b] [Fintype c] [DecidableEq c] {ρ : Matrix (a × b × c) (a × b × c) ℂ} (hpsd : ρ.PosSemidef) : (rhoAB ρ).PosSemidef

ρ_AB is PSD when ρ_ABC is.

theorem QuantumInfo.rhoBC_posSemidef {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] [Fintype b] [Fintype c] [DecidableEq a] {ρ : Matrix (a × b × c) (a × b × c) ℂ} (hpsd : ρ.PosSemidef) : (rhoBC ρ).PosSemidef

ρ_BC is PSD when ρ_ABC is.

Entropy-consistency of the two S(ρ_A), S(ρ_B) readings

The mutual-information identity is applied on the A | BC cut of ρ_ABC and on the A | B cut of ρ_AB. Both produce S(ρ_A) and S(ρ_B); we record that the marginals match so the two S(ρ_A), S(ρ_B) cancel in the SSA telescoping.

theorem QuantumInfo.rhoA_eq_traceB_AB {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype b] [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) : partialTraceRight ρ = partialTraceRight (rhoAB ρ)

The A-marginal of ρ_ABC (via the A | BC cut, partialTraceRight ρ) equals the A-marginal of ρ_AB (via the A | B cut, partialTraceRight (rhoAB ρ)). Both are ρ_A.

theorem QuantumInfo.rhoB_eq_traceC_BC {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] [Fintype c] (ρ : Matrix (a × b × c) (a × b × c) ℂ) : partialTraceLeft (rhoAB ρ) = partialTraceRight (rhoBC ρ)

The B-marginal of ρ_BC (via B | C, partialTraceRight (rhoBC ρ)) equals the B-marginal of ρ_AB (via A | B, partialTraceLeft (rhoAB ρ)). Both are ρ_B.

The conditional reduction: SSA from DPI

The hypothesis hDPI is the data-processing inequality for quantum relative entropy under the partial trace (= joint convexity of D(·‖·) = Lieb's concavity), stated abstractly so it is the genuine deep input and not a restatement of SSA. We apply it to the single tracing-out step ρ_ABC ↦ ρ_AB (trace C from the joint A,BC system) with σ = ρ_A ⊗ ρ_BC ↦ ρ_A ⊗ ρ_B.

★ hDPI is discharged UPSTREAM — cited, not imported (2026-07-31)

[LeanQIT2026] (QuAIR/Lean-QIT, Apache-2.0) proves DPI and SSA:

• QIT.State.relativeEntropy_dataProcessing_channel_ge — .../Entropy/RelativeEntropyDPI.lean ∀ (rho sigma : State a) (Phi : Channel a b), D(rho‖sigma) ≥ D(Phi rho ‖ Phi sigma)
• QIT.State.condMutualInfo_nonneg — .../Entropy/StrongSubadditivity.lean ∀ (ρ : State ((a × b) × c)), 0 ≤ ρ.condMutualInfo

Independently verified 2026-07-31: cloned at commit 48d4515, built standalone on its own toolchain, and #print axioms run on both — each depends on exactly [propext, Classical.choice, Quot.sound], the same footprint this corpus holds itself to. Their DPI is stated for an arbitrary channel, i.e. strictly stronger than hDPI, which needs only the partial-trace instance.

⚠️ What that verification does NOT establish: that their relativeEntropy / State / Channel agree with this corpus's relEntropy / Matrix + PosSemidef / partialTraceRight under the intended correspondence. The theorem is verified; the translation is not. Establishing it is precisely the bridge's job, and until it exists the citation is a pointer, not a discharge.

⚠️ This changes nothing about what THIS file proves. SSA here remains conditional on hDPI, and that is the correct reading of the corpus today. The citation records that the wall is known to be climbed elsewhere, with a precise pointer — not that we have climbed it. Do not restate SSA as unconditional on the strength of this note.

Why it is cited rather than imported. Lean-QIT targets Lean v4.30.0 with Mathlib pinned to tag v4.30.0 (2026-05-26); this corpus is on Lean v4.33.0-rc1 with Mathlib master c732b96d (2026-07-20). Lake resolves a single version per dependency, so the two cannot coexist until the toolchains reconcile.

How it will be discharged, when they do. hDPI is stated entirely in this corpus's vocabulary (relEntropy, Matrix (a × b × c), partialTraceRight), so discharging it means producing a term of that Prop — which can be done outside this repository. The plan is a separate csd-qit-bridge package depending on both projects by tag, holding the adapter and the unconditional SSA. Neither project merges into the other, and CsdLean4 keeps its Mathlib-only dependency footprint. See specs/BACKLOG.md (the operator-convexity L-row) and REFERENCES.json.

theorem QuantumInfo.strong_subadditivity_of_relEntropy_monotone {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] [Fintype b] [Fintype c] [DecidableEq a] [DecidableEq b] [DecidableEq c] {ρ : Matrix (a × b × c) (a × b × c) ℂ} (hpsd : ρ.PosSemidef) (_htr : ρ.trace = 1) (hpdA : (rhoA ρ).PosDef) (hpdB : (rhoB ρ).PosDef) (hpdBC : (rhoBC ρ).PosDef) (hDPI : ∀ (hpdA' : (partialTraceRight (rhoAB ρ)).PosDef), relEntropy ⋯ ⋯ ≤ relEntropy ⋯ ⋯) : vonNeumannEntropy ⋯ + vonNeumannEntropy ⋯ ≤ vonNeumannEntropy ⋯ + vonNeumannEntropy ⋯

Strong subadditivity from DPI (the conditional reduction — the K1-C deliverable).

S(ρ_ABC) + S(ρ_B) ≤ S(ρ_AB) + S(ρ_BC), derived from the data-processing hypothesis hDPI: relative entropy does not increase under the partial trace that maps the BC-system to its B-marginal,

D(ρ_AB ‖ ρ_A ⊗ ρ_B) ≤ D(ρ_ABC ‖ ρ_A ⊗ ρ_BC).

hDPI is the standard deep input (= DPI / joint convexity of relative entropy / Lieb concavity); Mathlib does not have it (see the module docstring's scout). The reduction is genuine:

• D(ρ_ABC ‖ ρ_A ⊗ ρ_BC) = S(ρ_A) + S(ρ_BC) − S(ρ_ABC) (mutual information I(A:BC)), and
• D(ρ_AB ‖ ρ_A ⊗ ρ_B) = S(ρ_A) + S(ρ_B) − S(ρ_AB) (mutual information I(A:B)),

both by relEntropy_kronecker_eq_entropy_sub. Substituting into hDPI and cancelling the common S(ρ_A) gives S(ρ_AB) + S(ρ_BC) − S(ρ_B) ≥ S(ρ_ABC), i.e. SSA. The direction is correct (I(A:BC) ≥ I(A:B), mutual information is monotone under discarding C); the bound is a genuine inequality on correlated ρ_ABC (equality iff ρ_ABC is a quantum Markov chain A−B−C), not a product identity.

Marginals positive-definite (hpdA, hpdB, hpdBC) is the standard support condition the relEntropy_kronecker_eq_entropy_sub step needs (it routes through Klein-style PD-σ machinery, Subadditivity.lean). The global ρ_ABC is only PosSemidef — pure / correlated states are covered. The unit-trace hypothesis _htr documents that ρ_ABC is a genuine density operator; it is not consumed by this trace-free identity reduction, hence the leading-underscore name.