feat(Analysis): add Lorentz cone trace inequality

[LionSR]

Motivation

• Wolf Ch. 3, Proposition 3.9 (Notes/WolfNoteTexSource/ch03_positive_not_completely.tex, lines ~650–736) states: for Hermitian $A \in M_d$, $A \geq 0 \Rightarrow \operatorname{tr}[A]^2 \geq \operatorname{tr}[A^2]$. This PR formalizes the forward implication, as part of the open formalization task in Preservation of cones: automorphism/rank classification (Prop 3.8) and confining Lorentz cones (Prop 3.9) #3402.

Description

• Adds TNLean/Analysis/MatrixTraceInequalities.lean with Matrix.PosSemidef.trace_sq_re_le_trace_re_sq: for positive semidefinite A, Re(tr(A²)) ≤ (Re tr A)². The proof proceeds by diagonalizing A to nonneg eigenvalues and applying Finset.sum_sq_le_sq_sum_of_nonneg.
• Adds the new module to the root TNLean.lean import.
• Adds a blueprint theorem entry in blueprint/src/chapter/ch04_channels.tex for the forward Lorentz-cone trace inequality, with \leanok.
• The converse in Prop. 3.9, the automorphism/rank classification (Prop. 3.8), and the trace-preserving rescaling lemma remain open in Preservation of cones: automorphism/rank classification (Prop 3.8) and confining Lorentz cones (Prop 3.9) #3402.

Testing

• lake build TNLean.Analysis.MatrixTraceInequalities
• lake build TNLean
• python3 scripts/blueprint_lean_sync.py --root . --diff-base origin/main --ci
• python3 scripts/check_reader_facing_prose.py --root . --diff-base origin/main --ci
• chktex -q -l blueprint/.chktexrc blueprint/src/chapter/ch04_channels.tex
• git diff --check

---

Addresses #3402

Note

Low Risk
Small, self-contained analysis lemma with no changes to channels, auth, or core infrastructure; only a new module, one root import, and blueprint text.

Overview
Adds Matrix.PosSemidef.trace_sq_re_le_trace_re_sq, the forward half of Wolf Ch. 3 Prop. 3.9: for PSD A, Re(tr(A²)) ≤ (Re tr A)², proved by diagonalizing to nonneg eigenvalues and closing with Finset.sum_sq_le_sq_sum_of_nonneg.

Introduces TNLean.Analysis.MatrixTraceInequalities, wires it into the root TNLean import surface, and documents the result in ch04_channels.tex as the forward Lorentz-cone trace inequality (blueprint \leanok).

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

---

Note

Low Risk
Self-contained analysis lemma plus root import and blueprint text; no changes to channels, auth, or core infrastructure.

Overview
Formalizes the forward implication of Wolf Ch. 3, Prop. 3.9: for PSD A, Re(tr(A²)) ≤ (Re tr A)², as progress on #3402.

Adds TNLean.Analysis.MatrixTraceInequalities with Matrix.PosSemidef.trace_sq_re_le_trace_re_sq, proved by Hermitian diagonalization to nonnegative eigenvalues and Finset.sum_sq_le_sq_sum_of_nonneg. The module is imported from TNLean.lean, and ch04_channels.tex gains a \leanok blueprint theorem linking the forward Lorentz-cone trace inequality to that lemma.

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

[claude]

PR cleanup

Field	Before	After
Title	feat(Analysis): add Lorentz cone trace inequality	unchanged
Body	## Summary / ## Scope / ## Verification headings; Refs #3402 at top	restructured to ### Motivation / ### Description / ### Testing template; Addresses #3402 footer; Cursor Bugbot block preserved verbatim
Labels	(none)	added: formalization, wolf-ch3 (copied from #3402)
Issue	linked to #3402

Conventions: CONTRIBUTING.md

[claude]

Review summary — APPROVE

A small, self-contained PR adding Matrix.PosSemidef.trace_sq_re_le_trace_re_sq, the forward implication of Wolf Ch. 3, Proposition 3.9 (for PSD A, Re(tr(A²)) ≤ (Re tr A)²), with a matching blueprint theorem. I built TNLean.Analysis.MatrixTraceInequalities against the project (lake build) and it compiles cleanly with no warnings on the new file.

1. Proof integrity 🔴 — clean

No sorry, admit, axiom, native_decide, or kernel bypasses. No maxHeartbeats bumps or debug artifacts.

2. Proof correctness 🔴 — sound

PosSemidef.trace_sq_re_le_trace_re_sq is proved by diagonalization: htrace gives (tr A).re = ∑ λᵢ from IsHermitian.trace_eq_sum_eigenvalues; htrace2 gives (tr (A²)).re = ∑ λᵢ² from the project's IsHermitian.trace_sq_eq_sum_eigenvalues_sq (TNLean/Algebra/PerronFrobenius/RankOne.lean:161); the inequality closes with Finset.sum_sq_le_sq_sum_of_nonneg using PosSemidef.eigenvalues_nonneg. The change ... at h steps are valid (for 𝕜 = ℂ, RCLike.ofReal r is defeq to the (r : ℂ) coercion). All hypotheses are used; no dangling terms; no brute-force tactic chains.

Faithfulness

The Lean statement uses (tr ·).re, which for PSD matrices (real eigenvalues) is exactly Wolf's tr(A²) ≤ tr(A)². The PR scopes itself to the forward direction only, and the blueprint entry thm:psd_trace_square_le_square_trace is labelled as the forward implication — consistent with the source. No extra hypotheses beyond A.PosSemidef, so no faithfulness gap and no paper-gap note required.

4. Type safety 🔴 — fine

[Fintype n] [DecidableEq n] are present and sufficient; no universe or coercion problems.

5/6/7 (🟡) — no blocking issues

Performance is trivial (finite eigenvalue sums). Documentation is complete: module docstring with Wolf2012QChannels reference, theorem docstring giving the eigenvalue meaning. The lemma is a general Matrix result placed appropriately under Analysis/.

Advisory (ℹ️, non-blocking)

• The private helper ofReal_sq_re restates a trivial cast identity (norm_cast / Complex.ofReal_pow territory) and could be inlined.
• Redundant Finset. prefixes given open Finset.

Neither rises to a 🟡 requires-changes issue. Approving.

[claude]

ℹ️ Advisory (not blocking). The private helper ofReal_sq_re, proving Complex.re ((r : ℂ) ^ 2) = r ^ 2, restates a trivial cast identity that Mathlib already handles. The whole calc block can be replaced inline by a one-liner, e.g. by rw [← Complex.ofReal_pow]; exact Complex.ofReal_re _ or simply by norm_cast, removing the need for a named helper. Purely a simplification suggestion — the current proof is correct.

[claude]

ℹ️ Advisory (not blocking). Finset is already opened at the top of the file, so the explicit Finset. prefix on Finset.sum_sq_le_sq_sum_of_nonneg (line 57) and Finset.sum_congr (line 55) is redundant — sum_sq_le_sq_sum_of_nonneg / sum_congr would resolve. Minor consistency point with the open Matrix Finset declaration.

[claude]

Review Summary

This PR adds the forward implication of Wolf Chapter 3 Proposition 3.9: for PSD $, $\operatorname{Re}(\operatorname{tr}(A^2)) \le (\operatorname{Re} \operatorname{tr} A)^2$. The proof is mathematically correct, well-structured, and uses the eigenvalue decomposition via existing lemmas.

🟡 Must-fix issues (1)

Modularity — Import of TNLean.Algebra.PerronFrobenius.RankOne (file TNLean/Analysis/MatrixTraceInequalities.lean, line 6)

The new file imports TNLean.Algebra.PerronFrobenius.RankOne but uses none of the Perron-Frobenius rank-one lemmas defined there. Every lemma used in the proof (isHermitian, trace_eq_sum_eigenvalues, trace_sq_eq_sum_eigenvalues_sq, eigenvalues_nonneg, Finset.sum_sq_le_sq_sum_of_nonneg, Complex.re_sum, Complex.ofReal_pow, Complex.ofReal_re) is a Mathlib lemma transitively available from Mathlib.Analysis.Matrix.PosDef alone.

This creates a false conceptual dependency: a reader would reasonably conclude that the trace inequality depends on Perron-Frobenius theory. Compare with TNLean/Analysis/TraceCFC.lean and TNLean/Analysis/ProjectionGeometry.lean, which import only the Mathlib modules they actually use.

Fix: Replace import TNLean.Algebra.PerronFrobenius.RankOne with import Mathlib.Analysis.Matrix.PosDef.

ℹ️ Advisory

• Simplify ofReal_sq_re (line 28–33): This private lemma's 5-line proof can likely be replaced with by simp since both Complex.ofReal_pow and Complex.ofReal_re are @[simp] lemmas. Not a blocker since the lemma is private and correct.

✅ Passed checks

• Proof integrity: No sorry, axiom, admit, native_decide, or other prohibited patterns.
• Proof correctness: The proof diagonalizes via eigenvalues and applies Finset.sum_sq_le_sq_sum_of_nonneg. The use of .re on complex traces is correct since the trace of a PSD matrix is real. Each rewrite step is sound.
• Type safety: Types are correct — Fintype n, DecidableEq n are properly available, and the .re projection on ℂ is well-typed.
• Performance: No decide on large types, no heavy simp chains, no maxHeartbeats overrides. The proof is lightweight.
• Documentation: Module docstring, theorem docstring, and Wolf citation are present.
• Mathlib style: Naming follows camelCase (PosSemidef.trace_sq_re_le_trace_re_sq), uses open scoped, and the proof structure is idiomatic.

Verdict: REQUEST_CHANGES — the import modularity issue must be resolved before approval.

[claude]

Blueprint & Prose Review — REQUEST_CHANGES

1 equivalence mismatch, 0 stale \leanok, 0 prose issues.

Category A — Blueprint ↔ Lean equivalence

A.1 mismatch (blueprint/src/chapter/ch04_channels.tex line 60, inline).

The Lean theorem Matrix.PosSemidef.trace_sq_re_le_trace_re_sq concludes (trace (A^2)).re ≤ (trace A).re ^ 2 — a comparison of real numbers via .re extraction. The blueprint formula \tr(A^2) \le \tr(A)^2 suppresses this: it compares complex-valued traces with $\le$, which has no standard meaning without noting that the traces are real for PSD matrices. The fact that they are real (sum of nonneg eigenvalues) is true but not stated. The blueprint must either note that the traces are real and nonneg before the display, or write $\operatorname{Re}\,\tr(A^2) \le (\operatorname{Re}\,\tr(A))^2$.

A.2 — \leanok accuracy: both the statement tag and the proof \leanok are valid — the Lean proof contains no sorry or admit, and the declaration name resolves correctly.

A.3 / A.4: no stale \notready; \uses{} is correctly absent (no blueprint-level dependencies); no renamed or missing declarations.

Category B — Prose quality

No violations found. The proof sketch properly carries the argument with a displayed formula; no Lean jargon, banned software-engineering terms, or LLM writing patterns appear in the changed text.

[claude]

Blueprint & Prose Review — REQUEST_CHANGES

0 equivalence mismatches, 0 stale \leanok, 1 prose issue, 2 advisories.

Thread resolution

The A.1 mismatch from the previous review (blueprint formula \tr(A^2) \le \tr(A)^2 without real-part extraction) is fixed in this synchronize: the blueprint now correctly writes \operatorname{Re}\tr(A^2) \le \left(\operatorname{Re}\tr(A)\right)^2, matching the Lean conclusion (Matrix.trace (A ^ 2)).re ≤ (Matrix.trace A).re ^ 2. That thread has been resolved.

Category A — Blueprint ↔ Lean equivalence

A.1 — Statement equivalence: the blueprint theorem thm:psd_trace_square_le_square_trace now matches Matrix.PosSemidef.trace_sq_re_le_trace_re_sq on all axes (quantifiers, hypotheses, conclusion, Re extraction). Clean.

A.2 — \leanok accuracy: both the statement tag and the proof \leanok are valid. The Lean proof contains no sorry or admit; the declaration resolves correctly.

A.3 / A.4 — No stale \notready; \uses{} is correctly absent; no renamed or missing declarations.

Category B — Prose quality

B.1 (blocking) — Blueprint proof sketch, line 71: the final step "which follows because all mixed products are nonnegative" is a verbal phrase where an algebraic identity should appear. docs/prose_style.md: "For proof sketches, equations should carry the argument." See inline comment for suggested replacement displaying the cross-term expansion.

B.2, B.3 (advisory) — Lean module docstring (line 14) and theorem docstring (line 38) use backticks for mathematical expressions (A ≥ 0, tr(A^2) ≤ tr(A)^2, ∑ᵢ λᵢ^2 ≤ (∑ᵢ λᵢ)^2) rather than prose. Per the style guide, backticks are for genuine Lean references; plain mathematical prose is preferred here. Not blocking.

[claude]

B — Proof sketch: verbal final step should be a displayed identity.

The proof reduces the inequality to $\sum_i \lambda_i^2 \le \left(\sum_i \lambda_i\right)^2$, then closes with a prose gloss:

which follows because all mixed products are nonnegative.

Per docs/prose_style.md §"Source-faithful terminology and formulas": "For proof sketches, equations should carry the argument." The cross-term expansion is the load-bearing step and should be displayed. Suggested replacement:

Suggested change

	which follows because all mixed products are nonnegative.
	which follows from
	\[
	\left(\sum_i \lambda_i\right)^2
	= \sum_i \lambda_i^2 + 2\sum_{i < j} \lambda_i \lambda_j
	\ge \sum_i \lambda_i^2,
	\]
	since each product $\lambda_i \lambda_j \ge 0$.

[claude]

ℹ️ Advisory (not blocking). The module docstring uses backticks for the mathematical conditions `A ≥ 0` and `tr(A^2) ≤ tr(A)^2`. Per docs/prose_style.md §1: "Reserve backticks for genuine Lean references." Neither of these is a Lean identifier — they are mathematical expressions. Prefer plain prose: "if $A \ge 0$, then $\tr(A^2) \le \tr(A)^2$".

[claude]

ℹ️ Advisory (not blocking). `∑ᵢ λᵢ^2 ≤ (∑ᵢ λᵢ)^2` and `λᵢ ≥ 0` are in backticks but are mathematical expressions, not Lean identifiers. Per docs/prose_style.md §1: "Reserve backticks for genuine Lean references." Write these in plain prose: "In eigenvalues this is $\sum_i \lambda_i^2 \le (\sum_i \lambda_i)^2$, with all $\lambda_i \ge 0$."

[claude]

Review summary — APPROVE

Small, self-contained PR adding the forward implication of Wolf Ch. 3, Prop. 3.9 ("Confining Lorentz cones"). No blocking (🔴) or required-change (🟡) issues remain.

Proof integrity 🔴 — pass

No sorry, axiom, native_decide, decide, or other blockers in TNLean/Analysis/MatrixTraceInequalities.lean. The proof is closed by genuine lemmas.

Proof correctness 🔴 — pass

Matrix.PosSemidef.trace_sq_re_le_trace_re_sq is logically structured: diagonalize via IsHermitian.eigenvalues, rewrite both traces as eigenvalue sums, and close with Finset.sum_sq_le_sq_sum_of_nonneg. I verified every cited lemma resolves:

• Matrix.IsHermitian.trace_eq_sum_eigenvalues (Mathlib Analysis/Matrix/Spectrum.lean:237)
• Matrix.IsHermitian.trace_sq_eq_sum_eigenvalues_sq (project lemma, TNLean/Algebra/PerronFrobenius/RankOne.lean:161)
• Matrix.PosSemidef.eigenvalues_nonneg (Mathlib Analysis/Matrix/PosDef.lean:42)
• Finset.sum_sq_le_sq_sum_of_nonneg (Mathlib Algebra/Order/BigOperators/Ring/Finset.lean:35)

The .re projection in the conclusion is well-typed and correct: for a PSD matrix the trace is real, so (trace (A^2)).re = ∑ λᵢ² and (trace A).re = ∑ λᵢ with all λᵢ ≥ 0.

Faithfulness — pass

Wolf Ch. 3, Prop. 3.9 part 1 (Notes/WolfNoteTexSource/ch03_positive_not_completely.tex:697): "Consider a Hermitian matrix A ∈ M_d(ℂ). Then A ≥ 0 ⇒ tr[A]² ≥ tr[A²]." The Lean hypothesis A.PosSemidef is exactly Hermitian-plus-nonnegative — no extra hypotheses beyond the source — and the conclusion (tr A²).re ≤ (tr A).re² is the source inequality. The hypothesis set matches, so this is a faithful formalization of the forward implication. The converse (part 2, with its (d−1) factor), Prop. 3.8, and the trace-preserving lemma correctly remain open under #3402.

Documentation 🟡 — pass

Module docstring and theorem docstring both present, with the eigenvalue-level interpretation and a Wolf citation.

Resolved

The prior-cycle blueprint thread (A.1 — complex-valued ≤ left implicit) is addressed: the statement now writes Re tr(A²) ≤ (Re tr A)² with the real-part extraction explicit, matching the Lean conclusion type. That thread is resolved.

Advisory (ℹ️ — non-blocking)

Two earlier inline notes remain, both genuinely optional cleanups and the proof is correct as written:

• The private helper ofReal_sq_re reproves a norm_cast-able identity; the calc could be inlined.
• Finset.sum_sq_le_sq_sum_of_nonneg / Finset.sum_congr carry a redundant Finset. prefix given open Finset.

These do not block merge.

[claude]

Review Summary — APPROVE

Changes reviewed

This PR adds Matrix.PosSemidef.trace_sq_re_le_trace_re_sq in a new module TNLean/Analysis/MatrixTraceInequalities.lean, formalizing item 1 of Wolf Ch. 3 Proposition 3.9: for PSD $A$, $\operatorname{Re} \operatorname{tr}(A^2) \le (\operatorname{Re} \operatorname{tr} A)^2$. The proof diagonalizes $A$ via Hermitian spectral decomposition, uses nonnegative eigenvalues, and reduces to the Finset inequality $\sum \lambda_i^2 \le (\sum \lambda_i)^2$.

🔴 Proof integrity

No sorry, axiom, admit, native_decide, or unsafeCast. Clean.

🔴 Proof correctness

The proof strategy is correct and follows the paper's strategy (write traces as sums of eigenvalues, apply the elementary sum-of-squares inequality). All lemmas used (IsHermitian.trace_eq_sum_eigenvalues, IsHermitian.trace_sq_eq_sum_eigenvalues_sq, PosSemidef.eigenvalues_nonneg, Finset.sum_sq_le_sq_sum_of_nonneg) exist and are correctly applied. The theorem statement matches Wolf Ch. 3 Prop. 3.9 item 1, with the real-part extraction made explicit (as required in Lean, where Matrix.trace on $\mathbb{C}$ returns a complex value).

🟡 Mathlib style & 🟡 Documentation

No blocking issues. The module and theorem docstrings are present and reference the paper source. The naming convention (PosSemidef.trace_sq_re_le_trace_re_sq) follows Mathlib norms. Two advisory items from the previous review remain:

• Line 33 (ofReal_sq_re): The private lemma could be shortened to by rw [Complex.ofReal_pow, Complex.ofReal_re]. The current form is correct but verbose.
• Lines 55, 57: Finset.sum_congr and Finset.sum_sq_le_sq_sum_of_nonneg carry the Finset. prefix despite open Finset at the module top. The prefix is harmless and arguably clearer for these less common lemmas.

Both are ℹ️ advisory — acceptable to merge as-is.

Previous review cleanup

• The blueprint Re-mismatch thread (PRRT_kwDORK8b986LaOJx) has been resolved: the new commit updates ch04_channels.tex to include \operatorname{Re} on both sides, bringing the blueprint statement into agreement with the Lean conclusion type.

Other categories (🟡 Performance, Type Safety, Modularity, Paper-gaps)

No issues found. The proof is lightweight and unlikely to cause timeouts. Types and universe levels are correct. The import through TNLean.Algebra.PerronFrobenius.RankOne is functional. No paper-gap notes are modified.

Verdict: APPROVE.