feat(Channel/Schwarz): add positive-map resolvent Jensen

[LionSR]

Refs #778, #138, #3375.

Summary

This PR proves the pointwise resolvent inequality needed in the matrix-level route to Wolf Corollary 5.2 for positive subunital maps.

• Adds TNLean.OperatorJensen.posSemidef_spectral_resolution, a finite spectral resolution of a positive semidefinite matrix by positive rank-one spectral pieces with nonnegative eigenvalue weights.
• Adds TNLean.OperatorJensen.positiveMap_resolvent_inv_le:
  ((T A) + t • 1)⁻¹ ≤ T ((A + t • 1)⁻¹) + t⁻¹ • (1 - T 1)
  for a positive subunital linear map T, a positive semidefinite matrix A, and t > 0.
• Updates blueprint Chapter 18 with the spectral-resolution and positive-map resolvent entries, and rewires the concave real-power Jensen entry to cite this positive-map resolvent step.

The proof uses the spectral resolution A = ∑ᵢ λᵢ Pᵢ, positivity of T(Pᵢ), CFC.sqrt to write T(Pᵢ) = Cᵢ Cᵢᴴ, the square root of the subunital defect 1 - ∑ᵢ T(Pᵢ), and the existing finite-POVM resolvent inequality.

Scope

This is a focused step for #778. It does not remove the three operator-Jensen axioms yet. It supplies the bare-positive-map resolvent estimate that the Löwner-integral assembly for posMap_rpow_concave_jensen should use next; the convex and logarithmic cases remain follow-on work.

During issue scouting, #766, #784, and #3395 were left out of this branch because they are independent open tasks with different mathematical inputs.

Validation

• lake env lean TNLean/Channel/Schwarz/OperatorJensenAux.lean
• lake build TNLean.Channel.Schwarz.OperatorJensenAux
• lake build TNLean
• python3 scripts/blueprint_lean_sync.py --root . --ci
• leanblueprint checkdecls
• git diff --check
• rg -n "sorry|admit|native_decide|\baxiom\b" TNLean/Channel/Schwarz/OperatorJensenAux.lean

No new sorry, admit, axiom, or native_decide is introduced. The full build still reports pre-existing warnings elsewhere in the repository, including the existing periodic-overlap sorry warning outside this PR.

---

Note

Low Risk
New proved lemmas and documentation only; no changes to axioms, runtime behavior, or auth/data paths. Mathematical correctness is localized to operator Jensen auxiliary theory.

Overview
Adds the pointwise resolvent inequality for positive subunital maps on finite matrices: ((T A) + t • 1)⁻¹ ≤ T ((A + t • 1)⁻¹) + t⁻¹ • (1 - T 1) as TNLean.OperatorJensen.positiveMap_resolvent_inv_le.

The proof introduces spectral-projector machinery (PSD rank-one pieces summing to 1, spectral sum and shifted resolvent expansions), packages posSemidef_spectral_resolution, factors T(Pᵢ) and the subunital defect via CFC.sqrt, and applies the existing povm_resolvent_inv_le.

Docs: OperatorJensenAux and OperatorConvexity status notes now treat this step as done and leave the CFC-integrand rewrite plus Löwner integral assembly as the next work toward posMap_rpow_concave_jensen. Blueprint Chapter 18 adds matching lemmas and cites the positive-map resolvent lemma in the concave real-power Jensen entry (still \notready).

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

[claude]

Review Summary

Verdict: APPROVE — no 🔴 blockers or 🟡 must-fix issues found. One ℹ️ advisory inline.

What this PR does

Adds two results to TNLean/Channel/Schwarz/OperatorJensenAux.lean in a new PositiveMapResolvent section:

• posSemidef_spectral_resolution — packages the spectral resolution of a PSD matrix as a finite family of PSD projectors summing to identity, with eigenvalue weights.
• positiveMap_resolvent_inv_le — the positive-map resolvent inequality: for a positive subunital linear map T, PSD matrix A, and t > 0:
  ((T A) + t • 1)⁻¹ ≤ T ((A + t • 1)⁻¹) + t⁻¹ • (1 - T 1)

Updates the blueprint (Chapter 18) with \leanok entries for both lemmas and rewires the concave rpow Jensen theorem dependency.

Category-by-category assessment

Category	Result
🔴 Proof integrity	Pass — no sorry, admit, axiom, native_decide, or unsafe features in new code
🔴 Proof correctness	Pass — spectral decomposition → POVM reduction chain is sound; each calc/rw/noncomm_ring step checks out; hypotheses are used correctly
🟡 Mathlib style	Pass — naming (snake_case for lemmas, camelCase for defs), tactic style, variable naming all consistent with surrounding file
🔴 Type safety	Pass — IsPositiveMap T applied to Fin D matrices uses correct [Fintype]/[DecidableEq] instances; eigenvalue coercion ℝ → ℂ is handled correctly
🟡 Performance	Pass — no decide on large types, no unbounded simp, noncomm_ring and linarith calls are on small expressions
🟡 Modularity & duplication	Pass — private helper lemmas (spectralProjection, spectral_sum_eq, etc.) are tightly scoped; posSemidef_spectral_resolution is public but appropriately specialized to Fin D for consistency with the rest of the file; no duplicated Mathlib lemmas
🟡 Documentation	Pass (1 ℹ️ advisory) — both public lemmas have docstrings; private lemma names are descriptive. One advisory: positiveMap_resolvent_inv_le docstring could include the explicit formula (see inline)
🟡 Paper-gap notes	N/A — no paper-gap files changed

Proof structure

The core proof of positiveMap_resolvent_inv_le proceeds cleanly:

1. Spectral resolution A = Σᵢ λᵢ Pᵢ via posSemidef_spectral_resolution
2. Positivity of T gives Bᵢ = T(Pᵢ) PSD
3. CFC.sqrt factorization: Bᵢ = Cᵢ Cᵢᴴ and defect 1 − Σ Bᵢ = S Sᴴ
4. These provide the C, S, hdef inputs to the existing povm_resolvent_inv_le
5. The POVM bound simplifies directly to the desired inequality

The auxiliary lemmas (spectral_sum_eq, spectral_shift_inv_sum, sqrt_mul_conjTranspose_sqrt) are well-factored and the calc blocks are structured and readable.

Blueprint

Both new lemmas carry correct \lean{...}, \leanok, and \uses{...} tags. The dependency graph update for thm:posMap_rpow_concave_jensen (from povm_resolvent → positive_map_resolvent) correctly reflects the new proof architecture described in the PR body.

🤖 Generated with Claude Code

[claude]

Review Summary (synchronize)

Verdict: APPROVE — no 🔴 blockers or 🟡 must-fix issues found.

What changed since last review

The synchronize trigger fired. I reviewed the current diff against all eight categories. The existing inline advisory (ℹ️) about the positiveMap_resolvent_inv_le docstring remains unresolved — the formula wasn't added — but that is an advisory, not a blocker.

Category-by-category assessment

Category	Result
🔴 Proof integrity	Pass — no sorry, admit, axiom, native_decide, or unsafe features in new code
🔴 Proof correctness	Pass — the spectral-decomposition → CFC.sqrt factorization → povm_resolvent_inv_le reduction chain is mathematically sound. The proof structure is: (1) spectral resolution A = Σᵢ λᵢ Pᵢ, (2) positivity of T gives Bᵢ = T(Pᵢ) PSD, (3) CFC.sqrt factorizations Bᵢ = Cᵢ Cᵢᴴ and 1 − Σ Bᵢ = S Sᴴ, (4) old povm_resolvent_inv_le with (C, S, λᵢ) directly yields the claimed inequality
🔴 Type safety	Pass — IsPositiveMap T applied to PSD matrices over Fin D uses the correct typeclass instances; eigenvalue coercion ℝ → ℂ via algebraMap is correct; LinearMap.map_smul_of_tower handles the ℝ/ℂ algebra tower properly
🟡 Mathlib style	Pass — naming follows conventions (snake_case lemmas, camelCase private defs), calc blocks are structured, classical blocks are scoped
🟡 Performance	Pass — no decide on large types, no unbounded simp, noncomm_ring and linarith calls are on small expressions
🟡 Modularity & duplication	Pass — private spectral helpers are tightly scoped; posSemidef_spectral_resolution is the only public interface from the spectral machinery; no duplicated Mathlib lemmas
🟡 Documentation	Pass — module docstring updated; new public lemmas have docstrings; the one pre-existing advisory (formula in docstring) persists
🟡 Paper-gap notes	N/A — no paper-gap files changed

Unresolved threads

The existing advisory thread from claude[bot] (line 595, OperatorJensenAux.lean) about adding the explicit inequality formula to the positiveMap_resolvent_inv_le docstring is still relevant — the formula was not added. Since this is advisory, it does not block approval.

🤖 Generated with Claude Code

[claude]

Review: APPROVE ✅

This is a clean, well-structured PR that proves the pointwise resolvent inequality for positive subunital maps — a key step toward the concave real-power operator Jensen inequality (Wolf Corollary 5.2, #778).

Summary of changes (3 files)

TNLean/Channel/Schwarz/OperatorJensenAux.lean (+328/−7):

• Adds posSemidef_spectral_resolution: spectral resolution of a PSD matrix into rank-one positive spectral projectors with eigenvalue weights. Correct, with clear supporting private lemmas (spectralProjection, spectral_sum_eq, spectral_shift_eq, spectral_shift_inv_sum).
• Adds positiveMap_resolvent_inv_le: (T A + t·1)⁻¹ ≤ T((A + t·1)⁻¹) + t⁻¹·(1 − T 1) for positive subunital T. The proof diagonalizes A via posSemidef_spectral_resolution, factors T(Pᵢ) and the subunital defect through CFC.sqrt, and applies the existing povm_resolvent_inv_le. Proof structure is clear, each intermediate identity is named and justified.
• Updates the module status note to reflect what is now done vs. remaining.

TNLean/Axioms/OperatorConvexity.lean (+12/−11): Status note updates are accurate — the pointwise resolvent step is correctly marked as proved (via positiveMap_resolvent_inv_le), with the CFC-integrand rewrite and Löwner-integral assembly as the remaining steps.

blueprint/src/chapter/ch18_operator_convexity.tex (+45/−1): Two new entries with \leanok, correctly wired to the \lean declarations. The thm:posMap_rpow_concave_jensen \uses is correctly updated from the raw POVM resolvent to the positive-map resolvent.

Category checks

Category	Severity	Verdict
Proof integrity	🔴 Blocker	✅ Clean: no sorry, admit, axiom, or native_decide in changed files
Proof correctness	🔴 Blocker	✅ The spectral reduction to povm_resolvent_inv_le is mathematically sound; all hypotheses are used; no dangling assumptions
Mathlib style	🟡 Requires changes	✅ Naming follows conventions; proof layout is idiomatic
Type safety	🔴 Blocker	✅ No type mismatches, universe issues, or missing instances
Performance	🟡 Requires changes	✅ No heavy decide/norm_num; calc/rw/linarith chains are appropriately sized
Modularity	🟡 Requires changes	✅ Private lemmas are appropriately scoped; no duplication of existing Mathlib API
Documentation	🟡 Requires changes	✅ Module-level status update, lemma docstrings with mathematical content and formula display
Paper-gap notes	🟡 Requires changes	N/A — no paper-gap changes

Resolved from previous review cycle

One stale claude[bot] thread (PRRT_kwDORK8b986LuYFL) suggesting the explicit inequality formula be added to the positiveMap_resolvent_inv_le docstring was resolved: the formula is already present at line 599.

No issues remain. Approved.

[chatgpt-codex-connector]

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

[claude]

Review Summary

Verdict: APPROVE — no 🔴 blockers or 🟡 must-fix issues.

Note: This PR was already merged at the time of review (state: MERGED). This review confirms the correctness and quality of the merged code.

What this PR delivers

Two new results in TNLean/Channel/Schwarz/OperatorJensenAux.lean:

• posSemidef_spectral_resolution (line 573): Packages the spectral resolution of a PSD matrix A as a finite family of PSD spectral projectors Pᵢ summing to 1, with A = Σ λᵢ Pᵢ where λᵢ are the nonnegative eigenvalues.
• positiveMap_resolvent_inv_le (line 603): For a positive subunital map T, PSD A, and t > 0:

  ((T A) + t • 1)⁻¹ ≤ T ((A + t • 1)⁻¹) + t⁻¹ • (1 - T 1)
  

  This is the pointwise resolvent inequality that feeds into the Löwner-integral proof of concave real-power operator Jensen (Wolf Corollary 5.2, #778).

Blueprint Chapter 18 updated with \leanok entries for both lemmas and corrected dependency wiring for thm:posMap_rpow_concave_jensen.

Category-by-category assessment

Category	Severity	Result
🔴 Proof integrity	Blocker	Pass — no sorry, admit, axiom, native_decide, unsafeCast, or other blockers introduced. The pre-existing sanctioned axioms in OperatorConvexity.lean are untouched.
🔴 Proof correctness	Blocker	Pass — The spectral decomposition → CFC.sqrt factorization → povm_resolvent_inv_le reduction chain is mathematically sound. Every have is correctly justified; all hypotheses are used; calc/rw/noncomm_ring/linarith steps check out. The Matrix.le_iff rewrite correctly converts T 1 ≤ 1 to (1 - T 1).PosSemidef (as defined at Mathlib/Analysis/Matrix/Order.lean:57).
🔴 Type safety	Blocker	Pass — IsPositiveMap T with T : MatD →ₗ[ℂ] MatD uses correct typeclass instances for Fin D matrices. Eigenvalue coercion ℝ → ℂ via RCLike.ofReal/Complex.ofReal is correctly handled. LinearMap.map_smul_of_tower correctly handles the ℝ/ℂ algebra tower in hTA_sum and hTInv_sum.
🟡 Mathlib style	Requires changes	Pass — snake_case lemmas, camelCase private defs. calc blocks are properly indented and structured. Tactic choice is appropriate. One very minor style observation: the hdef_pos proof line 629–632 mutates hSub with rw ... at hSub rather than using Matrix.le_iff.mp — mathematically correct but slightly less idiomatic. Not blocking.
🟡 Performance	Requires changes	Pass — No decide on large types. No unbounded simp. noncomm_ring and linarith calls are on small expressions. No maxHeartbeats overrides.
🟡 Modularity & duplication	Requires changes	Pass — Private spectral helpers (spectralProjection, spectral_sum_eq, spectral_shift_eq, spectral_shift_inv_sum, sqrt_mul_conjTranspose_sqrt) are appropriately scoped. posSemidef_spectral_resolution is the only public interface from the spectral machinery. No duplicated Mathlib lemmas identified — sqrt_mul_conjTranspose_sqrt is a narrow combination of CFC.sqrt_mul_sqrt_self + self-adjointness of CFC.sqrt that does not exist as a standalone Mathlib lemma.
🟡 Documentation	Requires changes	Pass — Module docstring updated. Both public lemmas have docstrings with mathematical content. positiveMap_resolvent_inv_le includes the explicit inequality formula (line 599), resolving the previous advisory thread (PRRT_kwDORK8b986LuYFL). Private lemmas lack docstrings, which is standard for private helpers.
🟡 Paper-gap notes	Requires changes	N/A — no paper-gap files changed.

✅ Resolved from previous review cycle

The one pre-existing thread (PRRT_kwDORK8b986LuYFL) about adding the explicit formula to the positiveMap_resolvent_inv_le docstring was resolved — the formula is present at line 599.

Proof structure walkthrough for positiveMap_resolvent_inv_le

1. Spectral decomposition: A = Σ λᵢ Pᵢ where Pᵢ are PSD, Σ Pᵢ = 1, λᵢ ≥ 0 (from posSemidef_spectral_resolution and private spectral lemmas).
2. Apply T: Bᵢ = T(Pᵢ) → PSD (positivity of T); Σ Bᵢ = T 1 ≤ 1 (subunitality).
3. CFC.sqrt factorizations: Bᵢ = Cᵢ Cᵢᴴ and 1 - Σ Bᵢ = S Sᴴ via CFC.sqrt and sqrt_mul_conjTranspose_sqrt.
4. Resolvent formula: (A + t·1)⁻¹ = Σ (λᵢ + t)⁻¹ Pᵢ (from spectral_shift_inv_sum).
5. Reduce to POVM: povm_resolvent_inv_le with (C, S, λᵢ) gives the claimed inequality.

The proof is well-factored: each intermediate identity (hTA_c, hTInv_c, hS_def_T) is explicitly named and justified before the final simpa.

🤖 Generated with Claude Code