refactor(Channel/Semigroup): reuse finite-dimensional Choi CLM#3092
Conversation
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Blueprint ↔ Lean sync & prose review — 0 issues found.
Category A — Blueprint ↔ Lean equivalence and status
choiCLM has no blueprint entry (grep of blueprint/src/ returns nothing for choiCLM, choiLinearOnCLM, or CPClosure). No .tex files were changed in this PR. There are no \lean{...}, \leanok, or \notready tags to audit.
Category B — Prose quality
The only changed text is the definition body; the docstring /-- The Choi matrix as a continuous linear map on continuous endomorphisms. -/ is unmodified and contains no Lean jargon, banned software-engineering terms, or LLM writing patterns.
Summary: 0 equivalence mismatches, 0 stale status tags, 0 prose issues.
There was a problem hiding this comment.
Review Summary
Verdict: APPROVE ✅
This is a one-definition refactor in TNLean/Channel/Semigroup/CPClosure.lean that replaces the manual ContinuousLinearMap construction of choiCLM with the standard Mathlib LinearMap.toContinuousLinearMap.
Category-by-category check
| Category | Result |
|---|---|
| 🔴 Proof integrity | No sorry, admit, axiom, or other blocked patterns. The change removes a manual cont proof and delegates to Mathlib's standard infrastructure. |
| 🔴 Proof correctness | The old construction (cont := choiLinearOnCLM.continuous_of_finiteDimensional) is definitionally equivalent to what LinearMap.toContinuousLinearMap provides. No mathematical change. |
| 🟡 Mathlib style | Using LinearMap.toContinuousLinearMap is the preferred Mathlib idiom. The docstring is preserved. |
| 🔴 Type safety | The type signature is unchanged. No instance or coercion issues. |
| 🟡 Performance | The construction is simplified, not complicated. No performance risk. |
| 🟡 Modularity & duplication | Removes manual duplication of the Mathlib pattern — a net improvement. |
| 🟡 Documentation | Existing docstring preserved. |
| 🟡 Paper-gap notes | No paper-gap files changed. |
Downstream compatibility verified
.continuousprojection at line 221simpa [choiCLM]at line 217- Both work identically with the new definition.
No issues to flag. Clean refactor, ready to merge.
🤖 Generated with Claude Code
claude
Bot
added
cleanup
|
PR cleanup
Conventions: CONTRIBUTING.md |
There was a problem hiding this comment.
Review: refactor(Channel/Semigroup): reuse finite-dimensional Choi CLM
Verdict: Approve. No 🔴 or 🟡 issues found.
This is a faithful, semantics-preserving simplification of the choiCLM definition in TNLean/Channel/Semigroup/CPClosure.lean. The hand-rolled ContinuousLinearMap structure
toLinearMap := choiLinearOnCLM
cont := choiLinearOnCLM.continuous_of_finiteDimensional
is replaced by LinearMap.toContinuousLinearMap choiLinearOnCLM.
Correctness / type safety. The two forms are definitionally equal: LinearMap.toContinuousLinearMap packages exactly the same underlying LinearMap (choiLinearOnCLM) with the continuity witness drawn from finite-dimensionality of the domain MatrixCLM (Fin D), and the cont field is a Prop (proof-irrelevant). Hence choiCLM's action (choiCLM T = choiMatrix T.toLinearMap) and its .continuous projection are unchanged.
Downstream impact — checked, none.
isClosed_setOf_isCPMap(CPClosure.lean:210) unfoldschoiCLMviasimpa [ChoiJamiolkowski.choiCLM]and uses(choiCLM (D := D)).continuous— both remain valid.EulerStep.leanconsumers (choiCLM.restrictScalars ℝat line 59 and thecongrArg/changeat lines 104–106) are unaffected.
Build. lake build TNLean.Channel.Semigroup.CPClosure TNLean.Channel.Semigroup.LindbladForm.EulerStep succeeds (exit 0). No new sorry/axiom/integrity blockers (docs/PROOF_INTEGRITY.md), no style, performance, modularity, or documentation concerns. The retained docstring on choiCLM is accurate.
LionSR
force-pushed
the
codex/choi-clm-finite-dimensional
branch
from
42d8f03 to
0826166
Compare
There was a problem hiding this comment.
Blueprint ↔ Lean sync & prose review — 0 issues found.
Category A — Blueprint ↔ Lean equivalence and status
No .tex files were changed. choiCLM and choiLinearOnCLM have no blueprint entries (blueprint/src/ contains no references to either). There are no \lean{...}, \leanok, or \notready tags to audit. The change is a purely definitional refactor with no added or removed declarations, so no new blueprint entries are required.
Category B — Prose quality
The only reader-facing text in scope is the docstring on choiCLM (line 198), which is unchanged: /-- The Choi matrix as a continuous linear map on continuous endomorphisms. -/. It contains no Lean jargon, no banned software-engineering terms, and no LLM writing patterns.
Summary: 0 equivalence mismatches, 0 stale status tags, 0 prose issues.
There was a problem hiding this comment.
Review: refactor(Channel/Semigroup): reuse finite-dimensional Choi CLM
Verdict: APPROVE — no 🔴 or 🟡 issues found.
Summary
This is a one-line definitional refactor of ChoiJamiolkowski.choiCLM in TNLean/Channel/Semigroup/CPClosure.lean. The anonymous ContinuousLinearMap constructor
{ toLinearMap := choiLinearOnCLM
cont := choiLinearOnCLM.continuous_of_finiteDimensional }is replaced by the idiomatic Mathlib wrapper LinearMap.toContinuousLinearMap choiLinearOnCLM, which is exactly the construction "promote a linear map on a finite-dimensional space to a continuous linear map." Good reuse — it removes the manual cont field while sourcing continuity from the same continuous_of_finiteDimensional fact internally.
Checks performed
- Proof integrity 🔴: No
sorry/axiom/native_decide/kernel bypass introduced. The underlying linear mapchoiLinearOnCLMis untouched. - Proof correctness 🔴: The only subtle point is that
isClosed_setOf_isCPMap(lines 213–218) useschange ... ↔ (choiMatrix T.toLinearMap).PosSemideffollowed bysimpa [choiCLM], which depends onchoiCLM Tbeing definitionallychoiMatrix T.toLinearMap.LinearMap.toContinuousLinearMappreserves this defeq (its coercion reduces to the underlying linear map'stoFun), and the continuity argument at line 221 (choiCLM.continuous) is unaffected. - Build 🔴: Verified locally —
lake build TNLean.Channel.Semigroup.CPClosurecompletes successfully (3004 jobs). The only warnings are pre-existing copyright-header linter messages on unrelated files. - Style / type safety / docs: Docstring on
choiCLMretained; type signature unchanged; no new declarations; no API surface change.
Clean, minimal, mathematically inert cleanup. Nice.
There was a problem hiding this comment.
Review Summary
This is a clean, minimal refactor (+2/−3 lines) that replaces an explicit ContinuousLinearMap structure constructor with LinearMap.toContinuousLinearMap. The change is definitionally equivalent and verified by a successful lake build.
Category-by-category assessment
🔴 Proof integrity — ✅ Pass.
No sorry, axiom, admit, or other blockers introduced or affected.
🔴 Proof correctness — ✅ Pass.
LinearMap.toContinuousLinearMap (Mathlib Topology/Algebra/Module/FiniteDimension.lean:299) is defined as ⟨f, f.continuous_of_finiteDimensional⟩ — exactly the same construction the old code performed manually. The underlying linear map choiLinearOnCLM is unchanged. All downstream uses (choiCLM T application, choiCLM.continuous, simpa [choiCLM], .restrictScalars ℝ) are verified compatible.
🟡 Mathlib style — ✅ Pass.
Using LinearMap.toContinuousLinearMap is the standard Mathlib idiom for promoting a linear map on a finite-dimensional space. The old field-by-field construction was unnecessarily verbose. No naming or style issues.
🔴 Type safety — ✅ Pass.
No type changes, universe issues, or instance requirements altered. The [FiniteDimensional ℂ (MatrixCLM (Fin D))] instance was already required (and available) for continuous_of_finiteDimensional in the old code.
🟡 Performance — ✅ Pass.
No algorithmic or proof-search changes. The @[simps] attribute on LinearMap.toContinuousLinearMap may even improve simp unfolding behavior.
🟡 Modularity & duplication — ✅ Pass.
This change reduces duplication by reusing Mathlib's existing LinearMap.toContinuousLinearMap instead of manually inlining the structure fields.
🟡 Documentation — ✅ Pass.
The existing docstring /-- The Choi matrix as a continuous linear map on continuous endomorphisms. -/ remains present.
🟡 Paper-gap notes — N/A. No paper-gap files changed.
Verdict: APPROVE
No 🔴 or 🟡 issues found. This is a textbook definitional cleanup.
There was a problem hiding this comment.
Review: refactor(Channel/Semigroup): reuse finite-dimensional Choi CLM
Verdict: Approve. No 🔴 or 🟡 issues.
Summary
This is a single, well-scoped definitional cleanup. The continuous linear map choiCLM in TNLean/Channel/Semigroup/CPClosure.lean is rebuilt from the anonymous ContinuousLinearMap constructor ({ toLinearMap := choiLinearOnCLM, cont := choiLinearOnCLM.continuous_of_finiteDimensional }) to the idiomatic LinearMap.toContinuousLinearMap choiLinearOnCLM. The underlying linear map choiLinearOnCLM is untouched, and no declarations are added or removed.
Correctness verification
I checked that the definitional behaviour relied upon by both call sites is preserved:
isClosed_setOf_isCPMap(CPClosure.lean:210) usessimpa [ChoiJamiolkowski.choiCLM] ...and(choiCLM (D := D)).continuous. Thesimpadischarge goes throughLinearMap.coe_toContinuousLinearMap', which is@[simp]and proven byrflinMathlib/Topology/Algebra/Module/FiniteDimension.lean:314, sochoiCLM Tstill reduces tochoiLinearOnCLM T = choiMatrix T.toLinearMap..continuousis available on any CLM.EulerStep.lean:104–108uses achangethat depends onchoiCLM Tbeing definitionally equal tochoiMatrix T.toLinearMap. Becausecoe_toContinuousLinearMap'isrfl,(LinearMap.toContinuousLinearMap choiLinearOnCLM) Treduces byrfltochoiLinearOnCLM T, exactly as the old structure-projection form did. Definitional equality is preserved, so thechangeandrestrictScalars/choiRCLMuses remain valid.
Categories
- Proof integrity: No
sorry/axiom/kernel bypasses introduced. ✅ - Proof correctness: No mathematical content changed; continuity still derives from finite-dimensionality, now via the standard Mathlib equiv. ✅
- Mathlib style: The change moves toward the canonical idiom. ✅
- Type safety / Performance / Modularity / Documentation: Unaffected; the docstring on
choiCLMis retained. ✅
Note: the PR description lists a build check for TNLean.Channel.Semigroup.CPClosure only, while EulerStep.lean also consumes choiCLM. The defeq analysis above indicates EulerStep should be unaffected, and CI (lean_action_ci.yml) covers it — worth confirming that run is green before merge.
There was a problem hiding this comment.
Review: refactor(Channel/Semigroup): reuse finite-dimensional Choi CLM
Verdict: APPROVE — no 🔴 or 🟡 issues found.
Summary
This replaces the manual ContinuousLinearMap structure constructor for choiCLM with LinearMap.toContinuousLinearMap choiLinearOnCLM (+2/−3 lines). The Mathlib definition (Topology/Algebra/Module/FiniteDimension.lean:299) is:
def toContinuousLinearMap : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F' where
toFun f := ⟨f, f.continuous_of_finiteDimensional⟩This is definitionally identical to the old { toLinearMap := choiLinearOnCLM; cont := choiLinearOnCLM.continuous_of_finiteDimensional }.
Category-by-category
| Category | Result |
|---|---|
| 🔴 Proof integrity | ✅ Pass. No sorry/axiom/admit introduced or affected. |
| 🔴 Proof correctness | ✅ Pass. Definitionally equivalent to the old construction. All downstream uses (choiCLM T application, choiCLM.continuous, simpa [choiCLM]) verified compatible. |
| 🟡 Mathlib style | ✅ Pass. LinearMap.toContinuousLinearMap is the standard Mathlib idiom. |
| 🔴 Type safety | ✅ Pass. No type signature or instance changes. |
| 🟡 Performance | ✅ Pass. No algorithmic changes. |
| 🟡 Modularity & duplication | ✅ Pass. Reduces manual duplication of a Mathlib pattern. |
| 🟡 Documentation | ✅ Pass. Existing docstring retained. |
| 🟡 Paper-gap notes | N/A. No paper-gap files changed. |
Build
lake build TNLean.Channel.Semigroup.CPClosure completes successfully (3004 jobs).
Clean refactor, ready to merge.
2 participants
Motivation
choiCLMinChannel/Semigroup/CPClosurewas built with an anonymousContinuousLinearMapstructure constructor, manually specifyingtoLinearMap := choiLinearOnCLMandcont := choiLinearOnCLM.continuous_of_finiteDimensional. Mathlib'sLinearMap.toContinuousLinearMapprovides exactly this construction for linear maps on finite-dimensional spaces, removing the need to spell out both fields.Description
TNLean/Channel/Semigroup/CPClosure.lean:choiCLMis nowLinearMap.toContinuousLinearMap choiLinearOnCLM(+2 / −3 lines). The underlying linear mapchoiLinearOnCLMis unchanged, and all downstream uses (e.g.isClosed_setOf_isCPMapviachoiCLM.continuous) are unaffected. No declarations added or removed; no mathematical content altered.Testing
lake build TNLean.Channel.Semigroup.CPClosure -q --log-level=infopython3 scripts/check_reader_facing_prose.py --root . --diff-base origin/mainpython3 scripts/blueprint_lean_sync.py --root . --cilean_action_ci.yml) to validate build.Note
Low Risk
Single definitional refactor with no API or proof changes; continuity still comes from finite-dimensionality via Mathlib.
Overview
choiCLMinCPClosure.leanno longer uses an explicitContinuousLinearMapconstructor with separatetoLinearMapandcontinuous_of_finiteDimensionalfields. It is nowLinearMap.toContinuousLinearMap choiLinearOnCLM, aligning with the usual Mathlib pattern for finite-dimensional linear maps.choiLinearOnCLMis unchanged. Call sites such asisClosed_setOf_isCPMap(continuity for the PSD preimage) andchoiRCLMin Lindblad Euler-step arguments still use the samechoiCLMAPI; this is a definitional cleanup only.Reviewed by Cursor Bugbot for commit 0826166. Bugbot is set up for automated code reviews on this repo. Configure here.