feat(Channel): record reduction map self-duality

[LionSR]

Summary

This PR records the self-duality part of Wolf Chapter 3, Example 3.1, equation (3.18), for the reduction map
[
T_k(X)=\operatorname{tr}(X)I-k^{-1}X.
]

It adds Matrix.traceAdjointMap_reductionMap, showing that the trace-pairing adjoint of T_k is again T_k. Equivalently,
[
\operatorname{tr}(T_k(\rho)X)=\operatorname{tr}(\rho T_k(X)).
]
The proof is the direct bilinear trace calculation after expanding the definition of T_k.

The blueprint now contains thm:reduction_map_self_dual.

This is progress on #3401. It does not prove the k-positivity criterion or the witness statement; those still require the Ky-Fan / spectral-criterion layer.

Validation

• lake exe cache get
• lake build TNLean.Channel.PositiveExamples -q --log-level=info
• lake build TNLean -q --log-level=info
• python3 scripts/blueprint_lean_sync.py --root . --ci
• python3 scripts/check_reader_facing_prose.py --root . --diff-base origin/main --ci
• python3 scripts/blueprint_lean_sync.py --root . --update-lean-decls, then cd blueprint && leanblueprint checkdecls
• git diff --check
• no proof-integrity markers in TNLean/Channel/PositiveExamples.lean

---

Note

Low Risk
Localized Mathlib-style proof and blueprint sync in channel examples; no auth, runtime, or broad API changes.

Overview
Adds Matrix.traceAdjointMap_reductionMap, showing the trace-pairing adjoint of the reduction map (T_k) equals (T_k) itself—i.e. (\operatorname{tr}(T_k(\rho)X)=\operatorname{tr}(\rho T_k(X))) (Wolf Ch. 3, Ex. 3.1, eq. 3.18). The proof uses nondegeneracy of the trace pairing via trace_mul_right_eq_zero_iff and trace_traceAdjointMap_mul, after expanding reductionMap.

PositiveExamples.lean now imports TNLean.Algebra.TracePairing and documents the new result in the module header.

The blueprint gains thm:reduction_map_self_dual (ch04_channels.tex) with a \leanok proof sketch matching the bilinear trace expansion.

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

[claude]

Review Summary

Verdict: APPROVE ✅

This PR adds Matrix.traceAdjointMap_reductionMap showing the reduction map is self-dual for the trace pairing (Wolf Ch. 3, Ex. 3.1, eq. 3.18), and records it in the blueprint as thm:reduction_map_self_dual. The proof is correct, well-structured, and follows the existing proof pattern in traceAdjointMap_traceAdjointMap.

Category-by-category assessment

Category	Severity	Finding
🔴 Proof integrity	✅ Pass	No sorry, axiom, or integrity markers.
🔴 Proof correctness	✅ Pass	The nondegeneracy argument (trace_mul_right_eq_zero_iff) + trace-adjoint identity (trace_traceAdjointMap_mul) + bilinear trace expansion is correct.
🟡 Mathlib style	✅ Pass	Naming (traceAdjointMap_reductionMap) follows existing conventions. Docstring includes paper citation. Import is minimal.
🔴 Type safety	✅ Pass	No universe or instance issues. Fin D provides Fintype, DecidableEq via classical.
🟡 Performance	✅ Pass	The simp set is bounded; no risk of timeout.
🟡 Modularity	✅ Pass	Lemma is appropriately scoped to PositiveExamples.lean. No Mathlib duplication.
🟡 Documentation	✅ Pass	Theorem docstring, module docstring, and blueprint entry all present and correct.
🟡 Paper-gap notes	N/A	No paper-gap files changed.

Advisory note (non-blocking)

The simp [..., mul_comm] on line 85–86 is a mild anti-pattern — simp with mul_comm can potentially loop. It works here due to the bounded lemma set, but could be replaced by simp [...] followed by ring for robustness.

Blueprint review

The new thm:reduction_map_self_dual entry in ch04_channels.tex is a clean, self-contained statement with a concise proof sketch that matches the Lean proof. The \lean{} tag points to Matrix.traceAdjointMap_reductionMap and \leanok is correctly placed.

🤖 Generated with Claude Code

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.