feat(Channel): formalize positive trace-preserving transposition#3404
Conversation
claude
Bot
added
formalization
|
PR cleanup
Conventions: CONTRIBUTING.md |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Review: APPROVE ✅
This is a clean, well-scoped PR that formalizes matrix transposition as a positive, trace-preserving linear map on M_n(ℂ) per Wolf Ch. 3 §3.1.
Assessment by category
1. 🔴 Proof integrity — No issues. No sorry, axiom, admit, native_decide, unsafeCast, or other blockers in the changed code.
2. 🔴 Proof correctness — Both proofs are mathematically sound:
transposeLinearMapComplex_isPositiveMap: usesPosSemidef.transpose(MathlibLinearAlgebra/Matrix/PosDef.lean:85), which proves that transposition preserves PSD via the quadratic-form definition. Thesimpacorrectly unfoldstransposeLinearMapComplex.transposeLinearMapComplex_isTracePreservingMap: usestrace_transpose(MathlibLinearAlgebra/Matrix/Trace.lean:73), which isrfl. Thesimpchain correctly reduces throughLinearEquiv.toLinearMap_apply→transposeLinearEquiv_apply→trace_transpose.
Both theorems are faithful to the source (Notes/WolfNoteTexSource/ch03_positive_not_completely.tex, lines ~32–37): the statement is exactly "transposition is positive and trace-preserving" with no extra hypotheses.
3. 🟡 Mathlib style — No issues. Naming follows conventions (lowerCamelCase for transposeLinearMapComplex, snake_case for theorems). simp/simpa calls use explicit lemma lists. Variable binder pattern (variable (n : Type*) / variable {n : Type*}) is standard Mathlib idiom. The results are placed in the Matrix namespace where they naturally belong.
4. 🔴 Type safety — No issues. [Fintype n] appears only on the trace-preservation theorem where it's mathematically needed. [DecidableEq n] is handled implicitly via the existing IsPositiveMap/IsTracePreservingMap definitions. No universe or coercion problems.
5. 🟡 Performance — No concerns. Both proofs are 2-3 lines with no heavy computation.
6. 🟡 Modularity & duplication — No issues. The definition reuses Matrix.transposeLinearEquiv from Mathlib directly rather than introducing an ad hoc linear map. All lemmas used (PosSemidef.transpose, trace_transpose) are existing Mathlib results.
7. 🟡 Documentation — Adequate. All three new declarations have docstrings. Module-level doc comments updated to cite Wolf Ch. 3 and list the new results. The blueprint entry (thm:transpose_positive_trace_preserving) is clear and self-contained.
8. Paper-gap notes — Not applicable (no files changed under docs/paper-gaps/).
Summary
The PR correctly proves that θ(A) = Aᵀ on M_n(ℂ) is a positive, trace-preserving linear map — the first two properties of the canonical example of a positive-but-not-CP map from Wolf Ch. 3 §3.1. The third property (not CP) is explicitly out of scope per issue #3391.
There was a problem hiding this comment.
Review summary
Category A — Blueprint ↔ Lean equivalence: no issues.
- Theorem
thm:transpose_positive_trace_preservinglinks to two Lean declarations (Matrix.transposeLinearMapComplex_isPositiveMapandMatrix.transposeLinearMapComplex_isTracePreservingMap). Both resolve and match the blueprint statement (positivity + trace-preservation of$\theta(X)=X^T$ ). - Both Lean proofs are sorry-free; statement and proof
\leanokare valid. -
\uses{def:positive_map, def:trace_preserving}labels both exist (lines 8 and 31 of the file). - No stale
\notready, no missing\leanok, no renamed declarations.
Category B — Prose quality: 1 issue.
- The positivity half of the proof sketch ("because transposition preserves positive semidefiniteness") is a circular verbal claim that restates the conclusion without the supporting identity. See inline comment on line 50. The trace-preservation half correctly shows the identity
$\tr(X^T)=\tr(X)$ and needs no change.
Counts: 0 equivalence mismatches, 0 stale \leanok, 1 prose issue (formula missing).
There was a problem hiding this comment.
Review summary
Small, well-scoped addition formalizing matrix transposition
Proof integrity 🔴 — clean
No sorry, axiom, native_decide, admit, or kernel bypasses. I built the file locally (lake env lean TNLean/Channel/Basic.lean, exit 0, no warnings).
Proof correctness 🔴 — clean
Matrix.transposeLinearMapComplex_isPositiveMap:intro A hA; simpa [transposeLinearMapComplex] using hA.transpose—hA.transpose : Aᵀ.PosSemidef, andsimpreducestransposeLinearMapComplex n AtoAᵀvia the@[simps apply]-generatedMatrix.transposeLinearEquiv_apply. Correct and minimal.Matrix.transposeLinearMapComplex_isTracePreservingMap:intro A; simp [transposeLinearMapComplex]dischargestrace Aᵀ = trace AthroughMatrix.trace_transpose. Correct.
The blueprint claim (thm:transpose_positive_trace_preserving) is mathematically sound and faithful to the source: it asserts only positivity and trace preservation (not the "not CP" half), matching what is formalized.
Type safety 🔴 — clean
I verified the elaborated signatures. IsPositiveMap requires no Fintype/DecidableEq (its @-signature is {n : Type*} → (Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) → Prop), so the positivity theorem correctly carries no instance hypotheses. IsTracePreservingMap uses trace, which needs [Fintype n], and the trace theorem declares exactly that. No autoImplicit reliance, no coercion issues. The two theorems' instance assumptions are each minimal and correct — not an inconsistency.
Mathlib style 🟡 / Modularity ℹ️
transposeLinearMapComplexis a thin specialization ofMatrix.transposeLinearEquivtoR = α = ℂon square matrices. The specialization is justified as a bridge to the ℂ-typedIsPositiveMap/IsTracePreservingMappredicates — acceptable, not flagged.- Naming (
camelCasedef, snake_case theorems) is fine.
Documentation 🟡 — one item
The transposeLinearMapComplex docstring uses \(...\) LaTeX delimiters, inconsistent with the file's backtick-unicode convention and Mathlib's documented $...$ inline-math delimiter (docs/MATHLIB_doc.md:158); see the inline comment with a suggested fix.
Verdict
Requesting changes solely for the docstring notation. Once the inline suggestion is applied, this is good to merge.
There was a problem hiding this comment.
Review Summary — PR #3404
PR: feat(Channel): formalize positive trace-preserving transposition
Verdict: REQUEST CHANGES — 1 🟡 issue remains unresolved
What this PR does
Adds Matrix.transposeLinearMapComplex on transposeLinearEquiv, with proofs that transposition is positive (transposeLinearMapComplex_isPositiveMap) and trace-preserving (transposeLinearMapComplex_isTracePreservingMap). Blueprint Ch. 4 gains Theorem thm:transpose_positive_trace_preserving.
Previous review cycle follow-up
- ✅ Resolved (Thread 1): The blueprint proof was updated to use formula-first reasoning (
$X = C^\dagger C \implies X^T = C^T\overline{C} = \overline{C}^\dagger\overline{C} \ge 0$ ) instead of the tautological "transposition preserves positive semidefiniteness." The proof is now mathematically self-contained and follows the prose style guide. - ❌ Still unresolved (Thread 2): The
transposeLinearMapComplexdocstring atTNLean/Channel/Basic.lean:89still uses\(M_n(\mathbb C)\)instead of the file's backtick-unicode convention (see inline comment).
Category-by-category assessment
| Category | Status |
|---|---|
| 🔴 Proof integrity | ✅ No sorry, axiom, or circular reasoning |
| 🔴 Proof correctness | ✅ Both proofs are mathematically correct; PosSemidef.transpose and trace_transpose confirmed in Mathlib |
| 🟡 Mathlib style | ✅ Naming, variable conventions, lemma placement all follow Mathlib patterns |
| 🔴 Type safety | ✅ No universe issues; [Fintype n] properly scoped to trace theorem |
| 🟡 Performance | ✅ Trivial one-liner simpa/simp proofs |
| 🟡 Modularity & duplication | ✅ Good reuse of Matrix.transposeLinearEquiv from Mathlib |
| 🟡 Documentation | ❌ Docstring for transposeLinearMapComplex uses \(...\) instead of backtick-unicode (file convention) |
| 🟡 Paper-gap notes | ✅ N/A |
Action required
Fix the docstring on TNLean/Channel/Basic.lean:89 to use backtick-unicode notation matching the rest of the file:
/-- Matrix transposition as a complex-linear map on `M_n(ℂ)`. -/This is a one-line change. No other issues found — the proofs are correct, the blueprint proof is formula-first, and all other categories pass cleanly.
There was a problem hiding this comment.
Review — APPROVE
Small, well-scoped PR formalizing matrix transposition Notes/WolfNoteTexSource/ch03_positive_not_completely.tex lines 32–37: "The transposition is trace preserving and positive"). The two previously-raised issues from earlier review cycles have been addressed in later commits.
1. 🔴 Proof integrity — clean
No sorry, axiom, admit, native_decide, unsafeCast, or kernel bypasses in the diff. I built the file locally: lake env lean TNLean/Channel/Basic.lean → exit 0, no warnings.
2. 🔴 Proof correctness — clean
Matrix.transposeLinearMapComplex_isPositiveMap(TNLean/Channel/Basic.lean:96):intro A hA; simpa [transposeLinearMapComplex] using hA.transpose.hA.transpose : Aᵀ.PosSemidefcomes fromMatrix.PosSemidef.transpose(Mathlib/LinearAlgebra/Matrix/PosDef.lean:85), whose ring constraint[CommRing R'] [PartialOrder R'] [StarRing R']is satisfied by ℂ.simpreducestransposeLinearMapComplex n AtoAᵀvia the@[simps apply]-generatedMatrix.transposeLinearEquiv_apply(Mathlib/Data/Matrix/Basic.lean:883). Matches.Matrix.transposeLinearMapComplex_isTracePreservingMap(TNLean/Channel/Basic.lean:102):intro A; simp [transposeLinearMapComplex]dischargestrace Aᵀ = trace Athrough the@[simp]lemmaMatrix.trace_transpose(Mathlib/LinearAlgebra/Matrix/Trace.lean:73, definitionallyrfl). Correct.
The result is faithful to the source: the statement is exactly positivity + trace preservation, with no extra hypotheses smuggled in. The "not CP" half is explicitly out of scope per #3391.
3. 🔴 Type safety — clean
The Mathlib 4.31 Matrix.PosSemidef is defined over n →₀ R (Finsupp), so it carries no [Fintype n]/[DecidableEq n] requirement; consequently transposeLinearMapComplex_isPositiveMap correctly declares no instance hypotheses, while transposeLinearMapComplex_isTracePreservingMap declares exactly [Fintype n] (needed by trace). The two signatures' instance assumptions are each minimal and correct. No universe or coercion problems.
4. 🟡 Mathlib style — clean
Naming follows convention (lowerCamelCase def, snake_case theorems). The variable (n : Type*) / variable {n : Type*} toggle is standard. simp/simpa use explicit lemma lists. Results placed in the Matrix namespace, where they belong.
5. 🟡 Performance — no concern
Both proofs are ≤3 lines with no heavy computation.
6. 🟡 Modularity & duplication — clean
transposeLinearMapComplex is a thin specialization of Matrix.transposeLinearEquiv (R = α = ℂ), justified as a bridge to the ℂ-typed IsPositiveMap/IsTracePreservingMap predicates rather than an ad-hoc map. All supporting lemmas are existing Mathlib results.
7. 🟡 Documentation — addressed
All three new declarations carry docstrings; the module doc and References now cite Wolf Ch. 3. The earlier concern that the transposeLinearMapComplex docstring used \( ... \) delimiters is resolved in commit 02ef1f1, which switches to $ ... $ — the inline-math delimiter documented in docs/MATHLIB_doc.md:158. I've resolved that bot thread. (ℹ️ advisory only: the file's other docstrings use backtick-unicode M_n(ℂ); $...$ is equally Mathlib-valid, so no change is required.)
8. Paper-gap notes — N/A
No files under docs/paper-gaps/ changed.
Blueprint ↔ Lean sync and prose quality are out of scope here (handled by the Blueprint Sync & Prose Review workflow).
Verdict: No outstanding 🔴 or 🟡 issues. Approving.
There was a problem hiding this comment.
Review — APPROVE ✅
Small, well-scoped PR formalizing matrix transposition lake env lean TNLean/Channel/Basic.lean → exit 0, no warnings) and verified faithfulness against the cited source.
1. 🔴 Proof integrity — clean
No sorry, axiom, admit, native_decide, unsafeCast, or kernel bypasses in the diff.
2. 🔴 Proof correctness — clean
Matrix.transposeLinearMapComplex_isPositiveMap(TNLean/Channel/Basic.lean:96):intro A hA; simpa [transposeLinearMapComplex] using hA.transpose.hA.transpose : Aᵀ.PosSemidefcomes fromMatrix.PosSemidef.transpose;simpreducestransposeLinearMapComplex n AtoAᵀvia the@[simps apply]-generatedMatrix.transposeLinearEquiv_apply. Correct and minimal.Matrix.transposeLinearMapComplex_isTracePreservingMap(TNLean/Channel/Basic.lean:102):intro A; simp [transposeLinearMapComplex]dischargestrace Aᵀ = trace AthroughMatrix.trace_transpose. Correct.
Faithfulness: The source (Notes/WolfNoteTexSource/ch03_positive_not_completely.tex:35) states verbatim "The transposition is trace preserving and positive". The Lean statements assert exactly positivity and trace preservation with no extra hypotheses; the "not completely positive" half is explicitly out of scope per #3391. Matches the source hypothesis set.
3. 🟡 Mathlib style — clean
lowerCamelCase def, snake_case theorems, explicit simp/simpa lemma lists, variable (n) / variable {n} toggle, placed in the Matrix namespace where it belongs.
4. 🔴 Type safety — clean
Matrix.PosSemidef carries no [Fintype n]/[DecidableEq n], so the positivity theorem correctly declares no instance hypotheses; transposeLinearMapComplex_isTracePreservingMap declares exactly [Fintype n] as required by trace. Each signature's instance assumptions are minimal and correct. No universe or coercion issues.
5. 🟡 Performance — no concern
Both proofs are ≤3 lines; no heavy computation.
6. 🟡 Modularity & duplication — clean
transposeLinearMapComplex is a thin specialization of Matrix.transposeLinearEquiv (R = α = ℂ), justified as a bridge to the ℂ-typed IsPositiveMap/IsTracePreservingMap predicates. Supporting lemmas are existing Mathlib results.
7. 🟡 Documentation — addressed
All three new declarations carry docstrings; the module doc and References now cite Wolf Ch. 3. The earlier concern that the transposeLinearMapComplex docstring used \( ... \) delimiters is resolved — it now uses backtick-unicode (`Matrix n n ℂ`), matching the file convention. I resolved that outdated bot thread.
8. Paper-gap notes — N/A
No files under docs/paper-gaps/ changed.
Blueprint ↔ Lean sync and prose quality are out of scope here (handled by the dedicated Blueprint Sync & Prose Review workflow).
Verdict: No outstanding 🔴 or 🟡 issues. Approving.
There was a problem hiding this comment.
Review — APPROVE ✅
Small, well-scoped PR formalizing matrix transposition Notes/WolfNoteTexSource/ch03_positive_not_completely.tex lines 35–37: "The transposition is trace preserving and positive"). All previously-raised issues from earlier review cycles are resolved.
1. 🔴 Proof integrity — clean
No sorry, axiom, admit, native_decide, unsafeCast, or kernel bypasses in the diff.
2. 🔴 Proof correctness — clean
-
Matrix.transposeLinearMapComplex_isPositiveMap(TNLean/Channel/Basic.lean:96):intro A hA; simpa [transposeLinearMapComplex] using hA.transpose.hA.transpose : Aᵀ.PosSemidefcomes fromMatrix.PosSemidef.transpose(Mathlib/LinearAlgebra/Matrix/PosDef.lean:85), whose proof uses commutativity of multiplication and Finsupp summation to show the quadratic form condition holds for$A^T$ when it holds for$A$ . Correct. -
Matrix.transposeLinearMapComplex_isTracePreservingMap(TNLean/Channel/Basic.lean:102):intro A; simp [transposeLinearMapComplex]dischargestrace Aᵀ = trace AthroughMatrix.trace_transpose(definitionallyrfl). Correct.
The result is faithful to the source: the statement is exactly positivity + trace preservation, with no extra hypotheses smuggled in. The "not CP" third property is explicitly out of scope per issue #3391.
3. 🔴 Type safety — clean
Matrix.PosSemidefis defined overn →₀ R(Finsupp) and does not intrinsically require[Fintype n]. The[Fintype n] [DecidableEq n]constraints come fromIsPositiveMap's section variables and are added as implicit instance arguments by Lean elaboration. Both theorems carry the correct instance assumptions.- The positivity theorem needs no explicit
Fintype(added implicitly); the trace theorem correctly declares[Fintype n](needed bytrace). No coercion or universe issues.
4. 🟡 Mathlib style — clean
- Naming follows convention:
camelCasedef,snake_casetheorems. variable (n : Type*)/variable {n : Type*}toggle is standard Mathlib idiom.- Results placed in
Matrixnamespace — correct location. simp/simpause explicit lemma lists.
5. 🟡 Performance — no concern. Both proofs are ≤3 lines with no heavy computation.
6. 🟡 Modularity & duplication — clean. transposeLinearMapComplex reuses Matrix.transposeLinearEquiv from Mathlib directly, with no ad-hoc reimplementations.
7. 🟡 Documentation — addressed
All three new declarations carry docstrings. Module doc and References now cite Wolf Ch. 3. The previously-flagged \(...\) docstring notation has been replaced with backtick-unicode `Matrix n n ℂ` matching the rest of the file.
8. 🟡 Paper-gap notes — N/A (no files changed under docs/paper-gaps/).
Previous review follow-up
- ✅ Resolved (Thread 1): Blueprint proof updated to formula-first reasoning (
$X = C^\dagger C \implies X^T = C^T\overline{C} = \overline{C}^\dagger\overline{C} \ge 0$ ). - ✅ Resolved (Thread 3): Docstring now uses backtick-unicode (resolved in this review cycle).
Verdict
No outstanding 🔴 or 🟡 issues. Approving.
There was a problem hiding this comment.
Blueprint ↔ Lean & Prose Review — 0 issues (A), 0 issues (B)
Category A — Blueprint ↔ Lean equivalence
A.1 — Mathematical equivalence. The blueprint theorem (ch04_channels.tex) asserts "$\theta(X) = X^T$ on \lean{} tag lists two Lean declarations whose conjunction covers exactly this claim:
-
Matrix.transposeLinearMapComplex_isPositiveMap:IsPositiveMap (transposeLinearMapComplex n)— no finiteness hypothesis required (positivity is pointwise). ✓ -
Matrix.transposeLinearMapComplex_isTracePreservingMap [Fintype n]:IsTracePreservingMap (transposeLinearMapComplex n)—Fintype nis implicit in the blueprint's "$M_D(\mathbb{C})$" context. ✓
The Lean statements are weakly more general (arbitrary n : Type*), which is not a sync bug: the blueprint claims the finite-dimensional special case that the Lean results cover.
A.2 — \leanok accuracy. Both Lean proofs are sorry-free (simpa ... using hA.transpose and simp [transposeLinearMapComplex]). The statement \leanok and proof \leanok are both valid.
A.4 — \uses accuracy. \uses{def:positive_map, def:trace_preserving} — both labels exist in the chapter (lines 8 and 31 of ch04_channels.tex). Correct.
Category B — Prose quality
The proof sketch is now formula-driven:
The identity chain is mathematically correct:
No banned software-engineering terms, no Lean jargon, no LLM writing patterns found.
Housekeeping
Resolved one outdated claude-authored thread (PRRT_kwDORK8b986LZu2U) whose notation complaint (docstring used \(M_n(\mathbb{C})\)) has been fixed — the current code correctly uses `M_n(ℂ)`.
Summary: 0 equivalence mismatches, 0 stale \leanok, 0 prose issues.
There was a problem hiding this comment.
Review — feat(Channel): formalize positive trace-preserving transposition
Verdict: APPROVE. No 🔴 or 🟡 issues found. The changes are a small, faithful formalization of Wolf Ch. 3 §3.1 (transposition as the standard positive, trace-preserving, not-completely-positive map).
Proof integrity 🔴
Clean. No sorry, axiom, native_decide, or kernel bypasses. lake env lean TNLean/Channel/Basic.lean compiles (exit 0).
Proof correctness 🔴
Matrix.transposeLinearMapComplex_isPositiveMap:simpa [transposeLinearMapComplex] using hA.transpose. The@[simps apply]ontransposeLinearEquivreducestransposeLinearMapComplex n AtoAᵀ, andMatrix.PosSemidef.transpose(valid over aCommRing+PartialOrder+StarRing, which ℂ satisfies) closes the goal. Correct.Matrix.transposeLinearMapComplex_isTracePreservingMap:simp [transposeLinearMapComplex]reduces totrace Aᵀ = trace A, discharged by the simp lemmaMatrix.trace_transpose. Correct.
Both proofs are short and delegate to existing Mathlib facts rather than reproving — no brute-forced tactic chains.
Type safety 🔴
Matrix.PosSemidef is defined via finitely-supported vectors (n →₀ R), so IsPositiveMap carries no Fintype/DecidableEq requirement. The positivity theorem is therefore correctly stated for arbitrary n : Type* with no instance binders, while the trace theorem correctly adds [Fintype n] (trace is a finite sum). No reliance on autoImplicit-inserted instances, no coercion or universe issues.
Style / Modularity / Documentation 🟡
- Naming follows conventions:
transposeLinearMapComplex(camelCase def),..._isPositiveMap/..._isTracePreservingMap(snake_case theorems). - Reuses Mathlib's
Matrix.transposeLinearEquivinstead of introducing an ad-hoc linear map — no duplication. - Both new declarations and the def have docstrings stating their mathematical meaning; module docstring and
## Main resultsupdated to cite Wolf Ch. 3.
Paper-gaps
No files under docs/paper-gaps/ are touched, so no paper-gap review applies.
The blueprint theorem thm:transpose_positive_trace_preserving and its proof sketch (X = C†C ⟹ Xᵀ = Cᵀ C̄ = C̄† C̄ ≥ 0; tr(Xᵀ) = tr(X)) are mathematically correct, but blueprint↔Lean sync and prose are out of scope for this review thread.
There was a problem hiding this comment.
Review Summary
Verdict: APPROVE — no blocking issues found.
What this PR does
Adds Matrix.transposeLinearMapComplex (matrix transposition as a ℂ-linear map on M_n(ℂ)) and proves it is positive (transposeLinearMapComplex_isPositiveMap) and trace-preserving (transposeLinearMapComplex_isTracePreservingMap), formalizing Wolf Ch. 3, §3.1 (lines ~32–37). Adds the corresponding blueprint theorem thm:transpose_positive_trace_preserving with equation-based proof sketch.
Category-by-category findings
| Category | Severity | Status |
|---|---|---|
| Proof integrity | 🔴 | Clean — no sorry, axiom, or suspicious patterns |
| Proof correctness | 🔴 | Both proofs are correct and grounded in Mathlib (PosSemidef.transpose, trace_transpose) |
| Mathlib style | 🟡 | Names follow conventions; tactic usage minimal and idiomatic |
| Type safety | 🔴 | Compiles clean; [Fintype n] correctly required only where trace needs it |
| Performance | 🟡 | Trivial simpa/simp proofs — no timeout risk |
| Modularity | 🟡 | Uses Matrix.transposeLinearEquiv from Mathlib rather than ad hoc definition |
| Documentation | 🟡 | All declarations have docstrings matching file conventions; module doc updated |
| Paper-gap notes | - | N/A (no paper-gap files changed) |
Previous review threads
All three prior bot threads are resolved and outdated. Both flagged issues have been addressed:
- Blueprint proof updated from verbal to equation-based form.
- Docstring notation fixed from
\(...\)to backtick-quoted unicode.
No 🔴 or 🟡 issues remain. The PR is faithful to the cited source (Wolf Ch. 3, lines 32–37: "The transposition is trace preserving and positive") and ready to merge.
2 participants
Motivation
Notes/WolfNoteTexSource/ch03_positive_not_completely.tex, lines ~32–37): ordinary matrix transpositionDescription
Matrix.transposeLinearMapComplexonM_n(ℂ)viaMatrix.transposeLinearEquiv.Matrix.transposeLinearMapComplex_isPositiveMap(positivity: PSD is preserved under transposition) usingPosSemidef.transpose.Matrix.transposeLinearMapComplex_isTracePreservingMap(trace invariance) usingtrace_transposethroughsimp.thm:transpose_positive_trace_preservinginblueprint/src/chapter/ch04_channels.texwith\lean{}tags for both new declarations, establishing transposition as the standard positive-but-not-CP example.Testing
lake env lean TNLean/Channel/Basic.leanpython3 scripts/blueprint_lean_sync.py --root . --diff-base origin/main --cipython3 scripts/check_reader_facing_prose.py --root . --diff-base origin/main --cichktex -q -l blueprint/.chktexrc blueprint/src/chapter/ch04_channels.texgit diff --checkCloses #3391
Note
Low Risk
Small, localized additions to channel foundations and blueprint sync; proofs are short and use existing Mathlib transpose facts.
Overview
Adds
Matrix.transposeLinearMapComplexonM_n(ℂ)via Mathlib'stransposeLinearEquiv, and proves it isIsPositiveMap(PSD preserved under transpose) andIsTracePreservingMap(trace unchanged).TNLean/Channel/Basic.leanmodule docs now cite Wolf Ch. 3 as well as Ch. 6 and list the new lemmas. Blueprint Ch. 4 gains Theorem "Transposition is positive and trace-preserving" (thm:transpose_positive_trace_preserving) linked to those Lean names—setting up transposition as the standard positive, trace-preserving map that is not CP.Reviewed by Cursor Bugbot for commit 4c4b18a. Bugbot is set up for automated code reviews on this repo. Configure here.
Note
Low Risk
Small additive lemmas and blueprint sync; proofs delegate to existing Mathlib transpose/PSD facts with no changes to channel or density-matrix core logic.
Overview
Formalizes matrix transposition on
M_n(ℂ)as the standard positive, trace-preserving linear map (Wolf Ch. 3 example), wired into Lean and the blueprint.Adds
Matrix.transposeLinearMapComplexvia Mathlib’stransposeLinearEquiv, with short proofs that it isIsPositiveMap(PosSemidef.transpose) andIsTracePreservingMap(simpon trace).TNLean/Channel/Basic.leanmodule docs now cite Wolf Ch. 3 and list these lemmas.Blueprint Ch. 4 gains Theorem
thm:transpose_positive_trace_preserving(proof sketch +\lean{}links) immediately after the trace-preserving definition, before completely positive maps.Reviewed by Cursor Bugbot for commit 59e67ab. Bugbot is set up for automated code reviews on this repo. Configure here.