feat(Channel): prove transposition map is positive and trace-preserving

[LionSR]

Motivation

• Formalizes Wolf, Quantum Channels & Operations, Ch. 3, §3.1 (lines ~32–37 of Notes/WolfNoteTexSource/ch03_positive_not_completely.tex): the matrix transposition map θ : M_d(ℂ) → M_d(ℂ), θ(A) = Aᵀ, is positive and trace-preserving.
• Continues formalization of Wolf Ch. 3, tracked in Tracking: Wolf Ch3 positive but not completely positive maps #995.

Description

• Adds TNLean/Channel/Transposition.lean with:
  • transpositionMap: the matrix transposition θ(A) = Aᵀ on M_d(ℂ) as a ℂ-linear map.
  • transpositionMap_isPositiveMap: θ is positive; proof reduces to Matrix.PosSemidef.transpose.
  • transpositionMap_isTracePreservingMap: θ is trace-preserving; proof uses Matrix.trace_transpose.
  • Both results are stated for general d with no extra hypotheses beyond the matrix algebra.
• Registers the module in TNLean.lean.
• Adds blueprint entries in blueprint/src/chapter/ch04_channels.tex with the transposition definition and the positivity and trace-preservation theorems linked via \lean{} tags.

Testing

• Relies on Lean CI (lean_action_ci.yml) to validate lake build.

---

Addresses #3391

Note

Low Risk
Additive Lean and blueprint content only; proofs are short and reuse existing Channel.Basic predicates with no changes to channel or auth-critical paths.

Overview
Adds transpositionMap on M_d(ℂ) (matrix transpose as a ℂ-linear map) and proves it is IsPositiveMap and IsTracePreservingMap, using Mathlib's PSD transpose lemma and simp for trace.

Exposes the module via TNLean.lean and extends blueprint ch. 4 with the transposition definition and linked positivity / trace-preserving theorems before the quantum-channel definition.

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

[claude]

PR cleanup

Field	Before	After
Title	feat: Transposition is a positive, trace-preserving map	feat(Channel): prove transposition map is positive and trace-preserving
Body	three sections present but Description lacked mathematical content	enriched Description with declaration names, proof reductions, and source citation; Cursor Bugbot note preserved
Labels	none	added: formalization, wolf-ch3
Issue	linked to #3391	comment posted on #3391

Conventions: CONTRIBUTING.md

[claude]

Review Summary

Verdict: APPROVE — no 🔴 or 🟡 issues found across any category.

🔴 Proof Integrity — PASS

No sorry, admit, axiom, native_decide, or unsafeCast. Both proofs are grounded in Mathlib (Matrix.PosSemidef.transpose in LinearAlgebra/Matrix/PosDef.lean:85, Matrix.trace_transpose in LinearAlgebra/Matrix/Trace.lean:72 which is @[simp]). No circular reasoning.

🔴 Proof Correctness — PASS

• transpositionMap correctly defines matrix transposition as a ℂ-linear map via Matrix.transposeLinearEquiv. The transpositionMap_apply lemma is rfl because the toLinearMap unwrapping is definitional.
• transpositionMap_isPositiveMap reduces to hA.transpose from Mathlib's PosSemidef.transpose — this lemma works for general [RCLike R'] on any [DecidableEq n] index type, covering Fin d / ℂ.
• transpositionMap_isTracePreservingMap relies on @[simp] lemma Matrix.trace_transpose (confirmed at Mathlib/LinearAlgebra/Matrix/Trace.lean:72-73); the by simp closure is sound.
• Both results are faithful to the Wolf source (Notes/WolfNoteTexSource/ch03_positive_not_completely.tex, lines 33–37): no extra hypotheses beyond d : ℕ.

🟡 Mathlib Style — PASS

• Naming follows conventions: camelCase for transpositionMap, snake_case for transpositionMap_isPositiveMap and transpositionMap_isTracePreservingMap.
• Line length ≤ 100 chars throughout.
• open scoped and open statements match Channel/Basic.lean conventions.
• @[simp] on transpositionMap_apply is appropriate.
• variable (d : ℕ) / variable {d} pattern for explicit-in-definition, implicit-in-theorems is idiomatic.

🔴 Type Safety — PASS

Fin d provides Fintype and DecidableEq instances. ℂ is RCLike. The IsPositiveMap and IsTracePreservingMap predicates from Channel.Basic correctly infer n := Fin d from the linear map's type. No universe or coercion issues.

🟡 Performance — PASS

Both proof terms are single-tactic one-liners (simpa, simp). No decide on large types, no deep rw chains, no norm_num on symbolic expressions.

🟡 Modularity & Duplication — PASS

TNLean/Channel/Transposition.lean is properly placed under the Channel directory. The Fin d parameterization is appropriate for fixed-dimension quantum systems (matching Wolf's M_d(ℂ)). The import graph is minimal — single import TNLean.Channel.Basic. No duplication of existing Mathlib or project lemmas.

🟡 Documentation — PASS

• Module docstring describes purpose, spectral intuition, and main declarations.
• transpositionMap has a docstring.
• Both theorems carry docstrings with Wolf source citations (Chapter 3, §3.1).
• Reference format [Wolf2012QChannels] matches Channel/Basic.lean.

🟡 Paper-gap Notes — N/A

No paper-gap files are changed or introduced.

Blueprint Additions (ch04_channels.tex)

The three blueprint entries (def:transposition_map, thm:transposition_positive, thm:transposition_trace_preserving) are faithfully linked to Lean via \lean{...} / \leanok tags. The \uses references correctly point to def:positive_map and def:trace_preserving. The proof sketches (spectral decomposition for positivity, diagonal-entry argument for trace preservation) are mathematically correct.

[claude]

Blueprint ↔ Lean Sync & Prose Review (categories A and B only)

Category A — Blueprint ↔ Lean equivalence: ✅ No issues.
All three new blueprint entries (def:transposition_map, thm:transposition_positive, thm:transposition_trace_preserving) carry correct \lean{...} tags pointing to the new Lean declarations. The Lean signatures match the blueprint statements. \leanok on both statement and proof is valid for all three (no sorry in either proof body). \uses{} references def:positive_map and def:trace_preserving, both of which exist.

Category B — Prose: 3 issues (see inline comments).

Summary: 0 equivalence mismatches · 0 stale \leanok · 3 prose issues.

[claude]

Category B — notation collision (D used for two distinct objects)

Throughout this chapter D denotes the matrix dimension (as in \MN{D}). In this proof sketch the same letter is introduced as the diagonal eigenvalue matrix: "$A = U D U^\dagger$, where $U$ is unitary and $D$ is diagonal". A reader who has just seen the ambient space declared as $M_D(\mathbb{C})$ will read both occurrences of D as the matrix dimension.

Replace the eigenvalue diagonal with an unambiguous symbol, e.g. \Lambda:

    If $A \ge 0$ then $A$ is Hermitian with spectral decomposition $A = U \Lambda
    U^\dagger$, where $U$ is unitary and $\Lambda = \operatorname{diag}(\lambda_1,
    \ldots, \lambda_D)$ has nonneg­ative diagonal entries. Hence
    $A^{T} = \overline{U} \Lambda U^{T}$, which has the same eigenvalues, so $A^{T} \ge 0$.

[claude]

Review: transposition map is positive and trace-preserving

Verdict: Approve. This is a clean, minimal, self-contained addition. I verified it builds locally (lake build TNLean.Channel.Transposition completes successfully with no errors), it contains no sorry/axiom/kernel bypasses, and the statements are faithful to the cited source with no extra hypotheses.

Proof integrity 🔴 — pass

No sorry, admit, axiom, native_decide, or other blockers from docs/PROOF_INTEGRITY.md. Both proofs are one-liners reducing to existing Mathlib lemmas.

Proof correctness 🔴 — pass

• transpositionMap_isPositiveMap : IsPositiveMap (transpositionMap d) reduces to Matrix.PosSemidef.transpose ({M : Matrix n n R'} (hM : M.PosSemidef) : Mᵀ.PosSemidef) via simpa. Correct: transpositionMap d X = Xᵀ by transpositionMap_apply, and the goal (Xᵀ).PosSemidef is exactly hA.transpose.
• transpositionMap_isTracePreservingMap : IsTracePreservingMap (transpositionMap d) reduces to Matrix.trace_transpose (trace Aᵀ = trace A) via simp. Correct.

Faithfulness to the source — pass

Checked against Notes/WolfNoteTexSource/ch03_positive_not_completely.tex (lines ~32–39): "The transposition is trace preserving and positive: if UDU† is the spectral decomposition of any Hermitian matrix ... then (UDU†)ᵀ = U̅ D Uᵀ has the same eigenvalues." The Lean definition θ(A) = Aᵀ with ⟨i|Aᵀ|j⟩ = ⟨j|A|i⟩, the positivity theorem, and the trace-preservation theorem all match the source statement. Both Lean theorems are stated for general d with no hypotheses beyond the matrix algebra, so they are faithful formalizations (per the CLAUDE.md faithfulness rule), not stricter specializations. The blueprint \uses{def:positive_map, def:trace_preserving} references resolve to existing labels in ch04_channels.tex.

Documentation 🟡 — pass

Module docstring, definition docstring, and both theorem docstrings are present and explain the mathematical meaning (spectral-decomposition argument, eigenvalue invariance) rather than Lean syntax.

Advisory (ℹ️, non-blocking)

1. Modularity (transpositionMap, line 38): the definition is fixed to Fin d, but the predicates it feeds (IsPositiveMap/IsTracePreservingMap) are generic over n : Type* with [Fintype n] [DecidableEq n], and transposeLinearEquiv, PosSemidef.transpose, and trace_transpose are all type-generic. The result could be stated over a generic index type for wider reuse. Acceptable as-is since Fin d matches the \MN{D} blueprint notation.
2. Copyright year (line 2): the header reads 2025 while sibling files such as Channel/Basic.lean use 2026. Trivial.
3. The Copyright too short! header-linter warning fires on this file, but it also fires on Channel/Basic.lean and the large majority of the project's files lack an Authors: line — this is the established project convention, not a regression introduced here.

No 🔴 or 🟡 issues found.

[claude]

Category B — notation collision (D used for two distinct objects)

Throughout this chapter D denotes the matrix dimension, as in \MN{D}. In this proof sketch the same letter is introduced as the diagonal eigenvalue matrix: "$A = U D U^\dagger$, where $U$ is unitary and $D$ is diagonal". A reader who has just seen the ambient space declared as $M_D(\mathbb{C})$ will read both occurrences of D as the matrix dimension.

Replace the eigenvalue diagonal with an unambiguous symbol, e.g. \Lambda:

    If $A \ge 0$ then $A$ is Hermitian with spectral decomposition $A = U \Lambda
    U^\dagger$, where $U$ is unitary and $\Lambda = \operatorname{diag}(\lambda_1,
    \ldots, \lambda_D)$ has nonnegative diagonal entries. Hence
    $A^{T} = \overline{U} \Lambda U^{T}$, which has the same eigenvalues, so $A^{T} \ge 0$.

[claude]

Category B — word-only proof sketch; formula required

"Transposition fixes the diagonal entries of $A$, hence preserves their sum" is a verbal description without the equation. Per docs/prose_style.md, proof sketches must carry the argument by formula. The identity is elementary, so two lines suffice:

    The diagonal entries satisfy $(A^{T})_{ii} = A_{ii}$ for all $i$, so
    $\tr(A^{T}) = \sum_{i} (A^{T})_{ii} = \sum_{i} A_{ii} = \tr(A)$.

[claude]

Category B — backtick code spans around non-Lean mathematical content

Lines 13–15 wrap the spectral-decomposition argument in backtick code spans:

`θ : M_d(ℂ) → M_d(ℂ)`, `θ(A) = Aᵀ`
`A = U D U†` … `Aᵀ = Ū D Uᵀ` … `D`

Per docs/prose_style.md §1, backticks in Lean docstrings are for genuine Lean identifiers. The symbol θ has no Lean name (the Lean name is transpositionMap), and U, D, Ū in the spectral decomposition are mathematical variables, not Lean expressions. Using code spans here misrepresents prose mathematics as Lean syntax.

Rewrite as plain mathematical prose (the \(...\) convention is optional outside the TNLean/MPS/ParentHamiltonian region):

Matrix transposition θ(A) = Aᵀ is introduced as a ℂ-linear map on M_d(ℂ)
and shown to be positive and trace preserving.

Positivity follows from the spectral decomposition: if A ≥ 0 then A = U Λ U†
where U is unitary and Λ is diagonal with nonnegative entries, so Aᵀ = Ū Λ Uᵀ
has the same eigenvalues and is again positive semidefinite.

(Replace the Λ suggestion as needed to avoid the collision with dimension D noted separately in the blueprint.)

[LionSR]

Closing as a duplicate of #3404, which has merged the positive trace-preserving transposition result.