refactor(MPS/Symmetry): use trace CLM for string order#3096
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 and prose review
0 equivalence mismatches · 0 stale \leanok · 0 prose issues
Category A — Blueprint ↔ Lean equivalence and status
The only changed file is the proof body of MPSTensor.stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one (TNLean/MPS/Symmetry/StringOrderDefs.lean). The theorem statement is unchanged.
The corresponding blueprint entry (blueprint/src/chapter/ch12_symmetry.tex, lem:boundary_string_order_tendsto_zero, lines 960–973) carries both a statement \leanok and a proof \leanok. Neither is affected: the statement is unmodified and no sorry or admit is introduced in the refactored proof body. Both tags remain accurate.
No \lean{...} tags are added, removed, or renamed; no \notready tags are stale; no new Lean declarations require blueprint entries.
Category B — Prose quality
The diff touches only proof-body Lean code (type annotations and tactic terms). No blueprint .tex prose, Lean docstrings, module docs, or comments are modified. Nothing in scope for Category B is changed.
claude
Bot
added
cleanup
|
PR cleanup
No linked issue found. The branch name The closest existing issue is #2660 (String order with physical endpoint operators), which references Conventions: CONTRIBUTING.md |
There was a problem hiding this comment.
Review: refactor(MPS/Symmetry): use trace CLM for string order
Verdict: APPROVE — no 🔴 or 🟡 issues found.
This is a 7-line, proof-only refactor confined to the body of MPSTensor.stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one (TNLean/MPS/Symmetry/StringOrderDefs.lean). The theorem statement is unchanged, and the spectral-radius / iterate argument above the touched block is untouched.
1. 🔴 Proof integrity
No sorry, admit, axiom, native_decide, or kernel bypass introduced. The change removes a proof-local continuity lemma in favor of bundled Mathlib API. Clean.
2. 🔴 Proof correctness
The trace–boundary pairing functional φ is rebuilt from a bare LinearMap (→ₗ[ℂ]) into a bundled ContinuousLinearMap (→L[ℂ]) via LinearMap.toContinuousLinearMap, then the limit step uses φ.continuous.tendsto 0 instead of the old LinearMap.continuous_of_finiteDimensional + .continuousAt. I verified the substituted API against the pinned Mathlib (4.31):
LinearMap.toContinuousLinearMap(Mathlib/Topology/Algebra/Module/FiniteDimension.lean:299) requires[FiniteDimensional 𝕜 E]; the domainMatrix (Fin D) (Fin D) ℂis finite-dimensional, so the instance is available.LinearMap.coe_toContinuousLinearMap'(same file, line 315) is the simp lemma now used to re-expose the underlyingLinearMapapplication so the rewrittenφmatchesstringOrderBoundaryParam.
The chaining is sound: (φ.continuous.tendsto 0).comp hIter0 : Tendsto (fun L ↦ φ ((twistedTransferMap A u)^L Y)) atTop (𝓝 (φ 0)), and the closing simpa only [map_zero, …, LinearMap.coe_toContinuousLinearMap', …] turns φ 0 into 0 and reconciles the coercion. No dangling hypotheses.
3. 🟡 Mathlib style
Consistent with the surrounding code; let φ : … →L[ℂ] ℂ := LinearMap.toContinuousLinearMap <| … is idiomatic. No naming, import, or open-hygiene concerns.
4. 🔴 Type safety
The →ₗ[ℂ] → →L[ℂ] change is well-typed; the required FiniteDimensional instance is satisfied. No universe or coercion problems.
5–7. Performance / Modularity / Documentation
No performance regression (this removes an ad hoc finite-dimensionality step). No new lemmas to generalize. No docstrings affected (statement and doc comment unchanged).
8. Paper-gap notes
No files under docs/paper-gaps/ are touched.
Blueprint ↔ Lean sync and prose are out of scope here (covered by the dedicated workflow, which already approved this commit).
There was a problem hiding this comment.
Review Summary
Verdict: APPROVE
This is a clean, minimal proof refactoring (7 additions, 7 deletions) that replaces a local continuity proof (LinearMap.continuous_of_finiteDimensional) with Mathlib's bundled ContinuousLinearMap via LinearMap.toContinuousLinearMap. The theorem statement, hypotheses, and spectral-radius argument are unchanged.
Category-by-category findings
| Category | Severity | Finding |
|---|---|---|
| 🔴 Proof integrity | ✅ Pass | No sorry, axiom, or other blockers introduced. |
| 🔴 Proof correctness | ✅ Pass | The replacement is mathematically equivalent: LinearMap.toContinuousLinearMap internally uses continuous_of_finiteDimensional. (φ.continuous.tendsto 0).comp hIter0 is equivalent to the previous hφ_cont.continuousAt.tendsto.comp hIter0. The simpa block correctly unfolds the CLM via LinearMap.coe_toContinuousLinearMap'. |
| 🟡 Mathlib style | ✅ Pass | Code follows surrounding conventions; let binders and `< |
| 🔴 Type safety | ✅ Pass | FiniteDimensional and T2Space instances for Matrix (Fin D) (Fin D) ℂ are available as typeclass instances, satisfying LinearMap.toContinuousLinearMap requirements. |
| 🟡 Performance | ✅ Pass | No performance impact; the file builds in ~5.6s as part of the full build. |
| 🟡 Modularity | ✅ Pass | Improvement: removes a local continuity proof in favor of the Mathlib-provided LinearMap.toContinuousLinearMap. |
| 🟡 Documentation | ✅ Pass | No new definitions or theorems added; existing lemma docstring is adequate. |
| 🟡 Paper-gap notes | ✅ N/A | No paper-gap note changes. |
Mathematical assessment
Lemma stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one (line 226): The trace-pairing functional φ is now constructed as a ContinuousLinearMap rather than a bare LinearMap with an ad-hoc continuity proof. The composed limit argument (φ.continuous.tendsto 0).comp hIter0 is exactly the standard way to push a limit through a continuous function in a normed vector space. No mathematical content changed — this is purely a "use the library" refactoring.
🤖 Generated with Claude Code
LionSR
force-pushed
the
codex/string-order-trace-clm
branch
from
f5b5d1e to
ed879f1
Compare
There was a problem hiding this comment.
Blueprint ↔ Lean sync and prose review
0 equivalence mismatches · 0 stale \leanok · 0 prose issues
Category A — Blueprint ↔ Lean equivalence and status
The only changed file is the proof body of MPSTensor.stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one (TNLean/MPS/Symmetry/StringOrderDefs.lean). The theorem statement is unchanged.
The blueprint entry (blueprint/src/chapter/ch12_symmetry.tex, lem:boundary_string_order_tendsto_zero, lines 960–977) carries a statement \leanok (line 963) and a proof \leanok (line 973). Both remain accurate: the statement is unmodified and no sorry or admit is introduced in the refactored proof body.
No \lean{...} tags are added, removed, or renamed; no \notready tags are stale; no new Lean declarations require blueprint entries.
Category B — Prose quality
The diff touches only proof-body Lean code (type annotations and tactic terms). No blueprint .tex prose, Lean docstrings, module docs, or comments are modified. Nothing in scope for Category B is changed.
There was a problem hiding this comment.
Review: refactor(MPS/Symmetry): use trace CLM for string order
Verdict: APPROVE — no 🔴 or 🟡 issues found.
Scope
Single-lemma proof-only refactor of stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one in TNLean/MPS/Symmetry/StringOrderDefs.lean (+7/−7). The trace–boundary pairing functional φ is rebuilt from a bare LinearMap plus a proof-local LinearMap.continuous_of_finiteDimensional step into a ContinuousLinearMap via LinearMap.toContinuousLinearMap, and the iterate limit now composes with φ.continuous.tendsto 0.
1. Proof integrity 🔴 — clean
No sorry, admit, axiom, native_decide, unsafeCast, or kernel bypass introduced; the change removes a proof-local continuity layer (hφ_cont) rather than adding any. No maxHeartbeats or debug artifacts. I built the file locally — lake build TNLean.MPS.Symmetry.StringOrderDefs completes successfully (exit 0, ✔ Built TNLean.MPS.Symmetry.StringOrderDefs).
2. Proof correctness 🔴 — sound
LinearMap.toContinuousLinearMap(MathlibMathlib/Topology/Algebra/Module/FiniteDimension.lean:299) is the finite-dimensional≃ₗfromE →ₗ[𝕜] F'toE →L[𝕜] F'; its domainMatrix (Fin D) (Fin D) ℂis finite-dimensional, so the construction is well-typed.(φ.continuous.tendsto 0).comp hIter0correctly yieldsTendsto (fun L => φ (((twistedTransferMap A u) ^ L) Y)) atTop (nhds (φ 0)), andmap_zeroreduces the targetnhds (φ 0)tonhds 0in the closingsimpa.- The closing
simpa only [..., LinearMap.coe_toContinuousLinearMap', ...]adds exactly the coercion lemma (MathlibFiniteDimension.lean:315) needed to unfold the CLM application ofφback to the underlyingLinearMap, so the rewritten expression still matchesstringOrderBoundaryParam. Both cited Mathlib lemma names exist and are used as intended.
The theorem statement and the spectral-radius / iterate argument above this block are untouched — no mathematical content changes, so no paper-faithfulness or blueprint-statement concern arises.
3–7. Style / type safety / performance / modularity / documentation
- Style: idiomatic Mathlib; replacing an ad-hoc
continuous_of_finiteDimensionalwith the packaged CLM equivalence is a genuine simplification. - Type safety: domain finite-dimensionality is the only instance requirement and is satisfied; no universe or coercion concerns.
- Performance: removes work; no new wide
simpsets (simpa onlywith an explicit lemma list). - Modularity / documentation: no new declarations, so no docstring obligations; no duplication introduced.
- No
docs/paper-gaps/files touched, so item 8 does not apply.
Note (non-blocking, pre-existing, out of this PR's scope): CI status is pending at review time; the local build is green.
There was a problem hiding this comment.
Review: APPROVE ✅
This is a clean, low-risk proof refactor in a single lemma with no API or mathematical statement changes.
Summary of change
In stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one (TNLean/MPS/Symmetry/StringOrderDefs.lean:289), the trace–boundary pairing functional φ is promoted from a bare LinearMap (with an explicit LinearMap.continuous_of_finiteDimensional step) to a ContinuousLinearMap via LinearMap.toContinuousLinearMap. The limit step now uses φ.continuous.tendsto 0 directly instead of hφ_cont.continuousAt.tendsto. The closing simpa adds LinearMap.coe_toContinuousLinearMap' to handle the type coercion.
Category-by-category assessment
| # | Category | Severity | Finding |
|---|---|---|---|
| 1 | Proof integrity | 🔴 | Pass. No sorry, axiom, admit, native_decide, unsafeCast, or other blockers in the changed file. |
| 2 | Proof correctness | 🔴 | Pass. The refactoring is mathematically equivalent. LinearMap.toContinuousLinearMap is the standard Mathlib mechanism for promoting linear maps between finite-dimensional spaces. The composition (φ.continuous.tendsto 0).comp hIter0 correctly replaces hφ_cont.continuousAt.tendsto.comp hIter0. The added LinearMap.coe_toContinuousLinearMap' in the simpa list correctly resolves the type coercion from ContinuousLinearMap to LinearMap. |
| 3 | Mathlib style | 🟡 | Pass. Using LinearMap.toContinuousLinearMap is idiomatic Mathlib 4. The proof is minimal and follows the surrounding style. No new imports needed. |
| 4 | Type safety | 🔴 | Pass. φ : Matrix (Fin D) (Fin D) ℂ →L[ℂ] ℂ is correctly typed. All instances (FiniteDimensional, NormedSpace, etc.) are available from Mathlib. |
| 5 | Performance | 🟡 | Pass. No decide, no deep simp/rw chains, no performance risk. |
| 6 | Modularity & duplication | 🟡 | Pass. No new lemmas added. The change removes a local redundancy (continuous_of_finiteDimensional step) rather than introducing one. |
| 7 | Documentation | 🟡 | Pass. The theorem docstring (If the continuous linear operator ... has spectral radius < 1, then ... tends to 0) is adequate. The φ binding is a proof-internal let that needs no docstring. |
| 8 | Paper-gap notes | 🟡 | N/A. No changes to docs/paper-gaps/. |
Build verification
lake build succeeds with 9195/9195 jobs completed and no errors related to the changed file.
Verdict
This is a textbook example of a proof-internal cleanup that eliminates a redundant ad-hoc continuity argument in favor of the standard Mathlib API. No issues found across any review category. APPROVE.
There was a problem hiding this comment.
Review: refactor(MPS/Symmetry): use trace CLM for string order
Verdict: APPROVE — no 🔴 or 🟡 issues found.
A 7-line proof-only refactor confined to the body of MPSTensor.stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one (TNLean/MPS/Symmetry/StringOrderDefs.lean). The theorem statement, hypotheses, and the spectral-radius / iterate argument above the touched block are unchanged. I verified the change independently against the pinned Mathlib (4.31) and confirmed the file builds (lake build TNLean.MPS.Symmetry.StringOrderDefs, exit 0; the only warnings are pre-existing header-style warnings on unrelated QPF/* and Spectral/* files).
1. 🔴 Proof integrity
No sorry, admit, axiom, native_decide, or kernel bypass introduced. The diff removes the proof-local LinearMap.continuous_of_finiteDimensional step in favor of bundled Mathlib API. Clean.
2. 🔴 Proof correctness
The trace–boundary pairing functional φ is rebuilt from a bare LinearMap (→ₗ[ℂ]) into a bundled ContinuousLinearMap (→L[ℂ]) via LinearMap.toContinuousLinearMap, and the limit step becomes (φ.continuous.tendsto 0).comp hIter0 : Tendsto (fun L ↦ φ ((twistedTransferMap A u)^L Y)) atTop (𝓝 (φ 0)). The closing simpa only [map_zero, …, LinearMap.coe_toContinuousLinearMap', …] rewrites φ 0 to 0 and unfolds the CLM coercion so the goal matches stringOrderBoundaryParam. No dangling hypotheses.
I confirmed both lemmas in the pinned source: LinearMap.toContinuousLinearMap (Mathlib/Topology/Algebra/Module/FiniteDimension.lean:299, a LinearEquiv applied as a function) and LinearMap.coe_toContinuousLinearMap' (same file, line 315, ⇑(toContinuousLinearMap f) = f).
3. 🟡 Mathlib style
let φ : … →L[ℂ] ℂ := LinearMap.toContinuousLinearMap <| … is idiomatic and consistent with the surrounding block. No naming, import, or open-hygiene concerns.
4. 🔴 Type safety
The →ₗ[ℂ] → →L[ℂ] change is well-typed; Matrix (Fin D) (Fin D) ℂ is finite-dimensional, so the FiniteDimensional instance required by toContinuousLinearMap is available. No universe or coercion problems.
5–8. Performance / Modularity / Documentation / Paper-gaps
No performance regression (the change removes a step). No new lemmas to generalize. Statement and docstring unchanged. No files under docs/paper-gaps/ touched.
Blueprint ↔ Lean sync and prose are out of scope here (handled by the dedicated workflow).
There was a problem hiding this comment.
Review of PR #3096: refactor(MPS/Symmetry): use trace CLM for string order
This is a 7-line proof-only refactor confined to the body of stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one in TNLean/MPS/Symmetry/StringOrderDefs.lean. The change promotes φ from a bare LinearMap (plus an ad-hoc LinearMap.continuous_of_finiteDimensional step) into a bundled ContinuousLinearMap via LinearMap.toContinuousLinearMap. The theorem statement, hypotheses, and the spectral-radius / iterate argument above this block are untouched.
Category-by-category assessment
| # | Category | Severity | Verdict |
|---|---|---|---|
| 1 | Proof integrity | 🔴 | Pass. No sorry, axiom, admit, native_decide, unsafeCast, or kernel bypass introduced. The change removes a proof-local continuity layer rather than introducing any blockers. |
| 2 | Proof correctness | 🔴 | Pass. LinearMap.toContinuousLinearMap (Mathlib FiniteDimension.lean:299) wraps f with f.continuous_of_finiteDimensional. (φ.continuous.tendsto 0).comp hIter0 correctly yields Tendsto (fun L => φ ((twistedTransferMap A u)^L Y)) atTop (𝓝 (φ 0)). The closing simpa adds LinearMap.coe_toContinuousLinearMap' (FiniteDimension.lean:315, ⇑(toContinuousLinearMap f) = f) to resolve the CLM coercion, and map_zero reduces the target to 0. The chaining is mathematically sound. |
| 3 | Mathlib style | 🟡 | Pass. LinearMap.toContinuousLinearMap is the idiomatic Mathlib 4.31 way to bundle continuity into a ContinuousLinearMap for finite-dimensional domains. The `let φ : … →L[ℂ] ℂ := LinearMap.toContinuousLinearMap < |
| 4 | Type safety | 🔴 | Pass. φ : Matrix (Fin D) (Fin D) ℂ →L[ℂ] ℂ is well-typed; FiniteDimensional for Matrix (Fin D) (Fin D) ℂ is available as a typeclass instance. No universe or coercion problems. |
| 5 | Performance | 🟡 | Pass. No decide, no unbounded simp, no deep rw. The change removes a step (less work for the kernel). |
| 6 | Modularity & duplication | 🟡 | Pass. This is a genuine improvement: replacing proof-local continuous_of_finiteDimensional with the Mathlib-provided CLM equivalence. No new lemmas, no duplication. |
| 7 | Documentation | 🟡 | Pass. The lemma's existing docstring (lines 223–225) is adequate; φ is internal to the proof and needs no separate docstring. |
| 8 | Paper-gap notes | 🟡 | N/A. No docs/paper-gaps/ files touched. |
Existing feedback
Six previous bot reviews all approve. The one PR conversation comment covers label addition and issue-linking housekeeping — unrelated to mathematical content. No unresolved review threads exist (GraphQL query returns zero threads).
Verdict
No 🔴 or 🟡 issues found across any review category. APPROVE.
2 participants
Motivation
The string-order decay proof still derived continuity of a trace-pairing functional by a proof-local finite-dimensionality argument. Mathlib 4.31 already provides the finite-dimensional equivalence from linear maps to continuous linear maps, so this local continuity layer can be removed.
Description
TNLean/MPS/Symmetry/StringOrderDefs.lean.stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one, the trace–boundary pairing functionalφis now defined as aContinuousLinearMapviaLinearMap.toContinuousLinearMap, eliminating the explicitcontinuous_of_finiteDimensionalstep and the separatehφ_contcontinuity hypothesis.φ.continuous.tendsto 0directly, in place ofhφ_cont.continuousAt.tendsto.Testing
lake exe cache getlake build TNLean.MPS.Symmetry.StringOrderDefs -q --log-level=infopython3 scripts/check_reader_facing_prose.py --root . --diff-base origin/mainpython3 scripts/blueprint_lean_sync.py --root . --cigit diff --checkgit diff --cached --checkNote
Low Risk
Proof-only refactor inside one lemma; no API or mathematical statement changes.
Overview
In
stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one, the trace–boundary pairing functional φ is no longer a bareLinearMapwith a localcontinuous_of_finiteDimensionalstep. It is built as aContinuousLinearMapviaLinearMap.toContinuousLinearMap, and the limit step usesφ.continuous.tendstoinstead ofcontinuousAtfrom that ad hoc continuity lemma.The
simpaat the end picks upLinearMap.coe_toContinuousLinearMap'so the rewritten φ still matchesstringOrderBoundaryParam. The lemma's statement and the spectral-radius / iterate argument above this block are unchanged.Reviewed by Cursor Bugbot for commit f5b5d1e. Bugbot is set up for automated code reviews on this repo. Configure here.
Note
Low Risk
Single-lemma proof refactor with no API or mathematical statement changes.
Overview
In
stringOrderBoundaryParam_tendsto_zero_of_spectralRadius_lt_one, the trace–boundary pairing φ is now aContinuousLinearMapbuilt withLinearMap.toContinuousLinearMap, instead of a bareLinearMapplus a localcontinuous_of_finiteDimensionalstep.The iterate limit composes with
φ.continuous.tendsto 0directly (replacinghφ_cont.continuousAt.tendsto), and the closingsimpaaddsLinearMap.coe_toContinuousLinearMap'so φ still aligns withstringOrderBoundaryParam. The lemma statement and the spectral-radius / iterate argument above this block are unchanged.Reviewed by Cursor Bugbot for commit ed879f1. Bugbot is set up for automated code reviews on this repo. Configure here.