feat(Analysis/Entropy): add quantum relative entropy

[LionSR]

Motivation

• Issue Entropy: remaining von Neumann entropy and SSA core #784 requires a von Neumann entropy and SSA core beyond the existing axiomatised bootstrap (Entropy: bootstrap entropy namespace with axiomatized strong subadditivity #613); the quantum relative entropy $D(\rho | \sigma) = \operatorname{Re} \operatorname{tr}(\rho(\log \rho - \log \sigma))$ is a prerequisite for the Klein inequality, data-processing, and strong-subadditivity route.
• Continues the entropy infrastructure tracked in Tracking: entropy infrastructure: von Neumann entropy, strong subadditivity, mutual information #239.

Description

• TNLean/Analysis/Entropy.lean: introduces quantumRelativeEntropy as the finite-dimensional trace-log expression $\operatorname{Re}\operatorname{tr}(\rho(\log\rho - \log\sigma))$, totalized via CFC.log; adds lemmas quantumRelativeEntropy_eq_trace_mul_log_sub, quantumRelativeEntropy_self, quantumRelativeEntropy_zero_left, and quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log (using the bridge vonNeumannEntropy_eq_neg_trace_mul_log).
• TNLean/Entropy/VonNeumann.lean: exposes the new declarations through the Entropy namespace.
• TNLean/Entropy/StrongSubadditivity.lean: minor update for the new API.
• blueprint/src/chapter/ch19_entropy.tex: adds blueprint entries with \lean{...} and \leanok tags for the new declarations.
• This PR does not prove Klein's inequality, data processing, or strong subadditivity, and does not remove any sanctioned axiom by itself.

Testing

• lake build TNLean.Analysis.Entropy
• lake build TNLean.Entropy.VonNeumann
• lake build TNLean.Entropy.StrongSubadditivity
• lake build TNLean
• cd blueprint && leanblueprint checkdecls
• python3 scripts/check_reader_facing_prose.py --root . --diff-base origin/main --ci
• Added-line proof-integrity scan: no sorry, admit, native_decide, unsafeCast, or axiom.

---

Addresses #784

---

Note

Low Risk
Pure additive entropy infrastructure (definitions and elementary lemmas); sanctioned SSA axioms and proof obligations are unchanged.

Overview
Adds quantum relative entropy (D(\rho\Vert\sigma) = \operatorname{Re}\operatorname{tr}(\rho(\log\rho-\log\sigma))) as a totalized trace-log definition using CFC.log, plus lemmas for trace splitting, (D(\rho\Vert\rho)=0), (D(0\Vert\sigma)=0), and rewriting (D) as (-S(\rho)-\operatorname{Re}\operatorname{tr}(\rho\log\sigma)) for Hermitian (\rho) via the existing von Neumann trace-log bridge.

The Entropy namespace re-exports the definition and lemmas; the strong-subadditivity module TODO now points at Entropy.quantumRelativeEntropy as step one toward Klein/Lieb instead of an informal definition. Blueprint chapter 19 documents the new declarations with \leanok tags. No Klein inequality, data processing, or axiom removal in this PR.

^{Reviewed by Cursor Bugbot for commit c4a8661. Bugbot is set up for automated code reviews on this repo. Configure here.}

[claude]

PR cleanup

Field	Before	After
Title	feat(Analysis/Entropy): add quantum relative entropy	unchanged
Body	## Summary / ## Scope / ## Validation headings; no Addresses footer	restructured to ### Motivation / ### Description / ### Testing + Addresses #784 footer; Cursor Bugbot block preserved
Labels	(none)	added: formalization, infrastructure, follow-up, auto-fix-claude, documentation
Issue	linked to #784 (branch codex/entropy-relative-784); #239 referenced as tracking umbrella

Conventions: CONTRIBUTING.md

[claude]

Review: feat(Analysis/Entropy): add quantum relative entropy

Verdict: APPROVE. No 🔴 or 🟡 issues found.

This is a tightly-scoped infrastructure PR introducing quantumRelativeEntropy and four supporting results. I verified the mathematics of each declaration.

Proof integrity 🔴 — clean

No sorry, admit, axiom, native_decide, unsafeCast, or kernel bypasses on any added line. The PR introduces no axiom and removes none.

Proof correctness 🔴 — sound

• quantumRelativeEntropy (Analysis/Entropy.lean:161): D(ρ‖σ) = Re tr(ρ·(log ρ − log σ)) with CFC.log. Well-formed.
• quantumRelativeEntropy_eq_trace_mul_log_sub: the simp [..., Matrix.mul_sub, Matrix.trace_sub] reduces via mul_sub → trace_sub → Complex.sub_re to Re tr(ρ log ρ) − Re tr(ρ log σ). Correct.
• quantumRelativeEntropy_self and quantumRelativeEntropy_zero_left: collapse through sub_self/mul_zero and zero_mul to Re(tr 0) = 0. Correct, and legitimate @[simp] lemmas.
• quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log: invokes vonNeumannEntropy_eq_neg_trace_mul_log (S(ρ) = −(tr(ρ log ρ)).re), so (tr(ρ log ρ)).re = −S(ρ); the linarith bridge and final rw [htrace] close the goal correctly. The Hermitian hypothesis is exactly what the cited bridge lemma requires — no extraneous hypotheses.

Faithfulness

quantumRelativeEntropy is documented as a standard, totalized trace-log expression (built on the total CFC.log), and the docstring at Analysis/Entropy.lean:148-159 correctly states it coincides with the physical Umegaki relative entropy only on the domain where ρ is a density matrix and σ is positive definite. The Re wrapper makes the definition total without changing its value on the physical domain. No source theorem is being claimed with a hypothesis set, so the faithfulness rule is satisfied. The blueprint def:quantum_relative_entropy statement matches the Lean definition.

Style, type safety, documentation 🟡 — satisfied

• Naming: camelCase definition, snake_case lemmas — conforms to docs/MATHLIB_naming.md.
• All five declarations carry mathematical docstrings explaining meaning, not just syntax.
• [Fintype n] [DecidableEq n] is in scope (Analysis/Entropy.lean:76); no missing instances or coercion concerns.
• The repeated open scoped Matrix.Norms.L2Operator in before each CFC.log-using declaration matches the existing pattern already in the file (line 108) and is required to bring the matrix CFC scope into view.

Out of scope

Blueprint ↔ Lean tag sync and prose quality in ch19_entropy.tex are deferred to the dedicated Blueprint Sync & Prose Review workflow. No docs/paper-gaps/ files were touched.

Note: I was unable to run lake build in this environment (no cached oleans), so correctness above is established by proof-term analysis rather than a local compile. The PR description reports successful lake build TNLean and leanblueprint checkdecls.

[claude]

Review Summary

All 8 review categories checked. No 🔴 or 🟡 issues found.

Category-by-category findings:

1. 🔴 Proof integrity — Clean. No sorry, admit, axiom, native_decide, or unsafeCast. All proofs are fully closed.

2. 🔴 Proof correctness — All 4 proofs (quantumRelativeEntropy_eq_trace_mul_log_sub, quantumRelativeEntropy_self, quantumRelativeEntropy_zero_left, quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log) are mathematically correct. The linarith call correctly bridges from vonNeumannEntropy_eq_neg_trace_mul_log. The simp proofs are targeted and correct.

3. 🟡 Mathlib style — Consistent with existing code. Naming follows conventions (camelCase def, snake_case lemmas). open scoped Matrix.Norms.L2Operator in pattern follows existing usage at line 108. @[simp] attributes are appropriate and non-cyclic.

4. 🔴 Type safety — Correct typing: quantumRelativeEntropy : Matrix n n ℂ → Matrix n n ℂ → ℝ. CFC.log has required C⋆-algebra instances via Matrix.Norms.L2Operator. [Fintype n] [DecidableEq n] from section variables.

5. 🟡 Performance — Trivial rw/simp/linarith proofs with no timeout risk.

6. 🟡 Modularity & duplication — Good design: definition in Analysis/Entropy.lean, aliased into Entropy namespace in Entropy/VonNeumann.lean following existing patterns. No duplicated Mathlib lemmas.

7. 🟡 Documentation — All new declarations have thorough docstrings with mathematical meaning, domain restrictions, and blueprint references. Module docstring updated.

8. 🟡 Paper-gap notes — None changed in this PR.

Verdict: APPROVE ✅

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ba002711a9

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[claude]

Review summary

1 dependency gap (A.4), 1 prose issue (B). Two inline comments posted.

Category A — Blueprint ↔ Lean equivalence

All five \lean{...} tags resolve to correct Lean declarations. Statement-level \leanok tags are valid on all entries; proof-level \leanok tags are valid (no sorry in any added proof body). All statements match on quantifiers, hypotheses, and conclusion:

Blueprint label	Lean declaration	A.1 match	\leanok
def:quantum_relative_entropy	quantumRelativeEntropy	✓	✓
lem:quantum_relative_entropy_trace_split	quantumRelativeEntropy_eq_trace_mul_log_sub	✓	✓
lem:quantum_relative_entropy_self	quantumRelativeEntropy_self	✓	✓
lem:quantum_relative_entropy_zero_left	quantumRelativeEntropy_zero_left	✓	✓
thm:quantum_relative_entropy_entropy_form	quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log	✓	✓

A.4 flag (line 244): The \uses for thm:quantum_relative_entropy_entropy_form omits lem:quantum_relative_entropy_trace_split, which the Lean proof invokes directly via rw [quantumRelativeEntropy_eq_trace_mul_log_sub]. The dependency graph is incomplete.

Category B — Prose quality

B flag (lines 252–256): The proof sketch for thm:quantum_relative_entropy_entropy_form describes the substitution step only in words — "replace the first term by $-S(\rho)$". The identity $\operatorname{Re}\operatorname{tr}(\rho\log\rho) = -S(\rho)$ (from thm:entropy_eq_neg_trace_mul_log) must be displayed for the argument to be formula-driven, as required by docs/prose_style.md.

[claude]

Review summary (synchronize)

Both issues from the previous round are fixed. 0 equivalence mismatches, 0 stale \leanok tags, 0 prose issues.

Category A — Blueprint ↔ Lean equivalence ✓

Blueprint label	Lean declaration	A.1 match	\leanok
def:quantum_relative_entropy	quantumRelativeEntropy	✓	✓
lem:quantum_relative_entropy_trace_split	quantumRelativeEntropy_eq_trace_mul_log_sub	✓	✓
lem:quantum_relative_entropy_self	quantumRelativeEntropy_self	✓	✓
lem:quantum_relative_entropy_zero_left	quantumRelativeEntropy_zero_left	✓	✓
thm:quantum_relative_entropy_entropy_form	quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log	✓	✓

A.4 (previously flagged): \uses for thm:quantum_relative_entropy_entropy_form now includes lem:quantum_relative_entropy_trace_split. Fixed ✓

Category B — Prose quality ✓

B (previously flagged): The proof sketch for thm:quantum_relative_entropy_entropy_form now displays both the trace-split application and the identity $\operatorname{Re}\operatorname{tr}(\rho\log\rho)=-S(\rho)$ in explicit display equations. Fixed ✓

The updated StrongSubadditivity.lean roadmap (item 2) now correctly restricts Klein's inequality to the positive-definite reference state case, addressing the codex-connector observation. Fixed ✓

No new issues found in the synchronize diff.

[claude]

PR #3387 Review — APPROVE

PR: feat(Analysis/Entropy): add quantum relative entropy by @LionSR

Summary

This PR adds the quantum relative entropy definition D(ρ‖σ) = Re tr(ρ(log ρ − log σ)) and four elementary lemmas to TNLean/Analysis/Entropy.lean, exposes them via alias in the Entropy namespace (TNLean/Entropy/VonNeumann.lean), updates the StrongSubadditivity TODO to reference the new API, and adds corresponding blueprint entries with \lean{…} / \leanok tags. The PR is purely additive — it introduces no new sorry, axiom, or proof obligations, and does not remove the sanctioned SSA axiom.

Review by category

Category	Verdict
🔴 Proof integrity	Clean — no sorry, admit, axiom, native_decide, or unsafeCast in added lines.
🔴 Proof correctness	Clean — all proofs are mathematically sound. The simp rewrites correctly expand the definition and use Matrix.mul_sub, Matrix.trace_sub, and sub_self. The linarith step in quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log correctly rearranges vonNeumannEntropy_eq_neg_trace_mul_log.
🟡 Mathlib style	Clean — naming follows camelCase/snake_case conventions; @[simp] tags are well-judged; alias declarations follow existing patterns in Entropy/VonNeumann.lean.
🔴 Type safety	Clean — quantumRelativeEntropy is typed Matrix n n ℂ → Matrix n n ℂ → ℝ with n under the existing [Fintype n] [DecidableEq n] variables; CFC.log instances are correctly provided via open scoped Matrix.Norms.L2Operator.
🟡 Performance	Clean — all proofs use small, focused simp calls and a single linarith on one equation; no risk of timeouts.
🟡 Modularity	Clean — definition placed in Analysis/Entropy.lean (the core entropy file); aliases follow the existing Entropy namespace pattern without duplication.
🟡 Documentation	Clean — all new definitions and theorems have docstrings explaining mathematical meaning; module docstrings updated; blueprint entries carry proper \lean{…}, \leanok, and \uses{…} tags.

Resolved from previous review

• \uses dependency (PRRT_kwDORK8b986LXMtJ): lem:quantum_relative_entropy_trace_split is now correctly listed in the \uses of thm:quantum_relative_entropy_entropy_form. ✅
• Proof sketch (PRRT_kwDORK8b986LXM9K): The blueprint proof now displays the key identity Re tr(ρ log ρ) = −S(ρ) explicitly. ✅

Blueprint check

The new blueprint entries in ch19_entropy.tex (def def:quantum_relative_entropy, lemmas lem:quantum_relative_entropy_trace_split, lem:quantum_relative_entropy_self, lem:quantum_relative_entropy_zero_left, theorem thm:quantum_relative_entropy_entropy_form) are faithful to the Lean declarations — each \lean{…} tag points to the correct Lean name, and the \leanok tags are warranted.

No 🔴 or 🟡 issues found. This PR is ready to merge.

[claude]

Review summary — APPROVE

Pure additive entropy infrastructure: introduces quantumRelativeEntropy ρ σ := (Matrix.trace (ρ * (CFC.log ρ - CFC.log σ))).re and four supporting lemmas, re-exports them in the Entropy namespace, and documents them in blueprint/src/chapter/ch19_entropy.tex. I reviewed against the project's proof-integrity, correctness, type-safety, and documentation criteria.

Proof integrity 🔴 — clean

No sorry, admit, native_decide, unsafeCast, or axiom on added lines. No sanctioned axiom removed.

Proof correctness 🔴 — verified

• quantumRelativeEntropy_eq_trace_mul_log_sub: simp [quantumRelativeEntropy, Matrix.mul_sub, Matrix.trace_sub] correctly distributes the product over log ρ - log σ, splits the trace, and pushes Complex.sub_re through the real part.
• quantumRelativeEntropy_self / quantumRelativeEntropy_zero_left: trivial via log ρ - log ρ = 0 and 0 * X = 0 respectively; both are honest @[simp] candidates.
• quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log: the bridge step (trace (ρ * CFC.log ρ)).re = -vonNeumannEntropy ρ hρ is obtained from vonNeumannEntropy_eq_neg_trace_mul_log hρ via linarith, then rewritten — a logical, non-brute-forced chain. The Hermitian hypothesis is the genuine requirement (it is what makes the trace-log term equal -S(ρ)), matching thm:quantum_relative_entropy_entropy_form.

Faithfulness — consistent

The definition is the totalized trace-log expression; the docstring correctly scopes the physical (Umegaki) interpretation to density ρ with positive-definite σ, and def:quantum_relative_entropy in the blueprint states the same totalization. No hidden hypotheses are introduced.

Type safety 🔴, performance 🟡, documentation 🟡 — no issues

n carries [Fintype n] [DecidableEq n]; open scoped Matrix.Norms.L2Operator in supplies the normed structure that CFC.log requires, matching the established pattern at the adjacent vonNeumannEntropy_eq_neg_trace_mul_log. All proofs are constant-cost. Every new declaration has a mathematical docstring.

Previous review threads

All three prior bot threads are addressed by commit c4a866 and have been resolved:

• The Klein-route correctness note (chatgpt-codex-connector) — the StrongSubadditivity.lean roadmap now requires σ positive definite / the support condition for singular σ.
• \uses dependency and proof-identity prose notes (claude) — addressed in ch19_entropy.tex. (Blueprint \uses/\leanok and prose are handled by the dedicated Blueprint Sync workflow and are out of scope here.)

No outstanding 🔴 or 🟡 issues. Note build and Check blueprint compiles CI checks were still pending at review time; merge should await them.