refactor(Spectral): use trace CLM for cross correlations#3095
Conversation
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Blueprint ↔ Lean equivalence and prose review
0 equivalence mismatches, 0 stale \leanok, 0 prose issues.
Category A — Blueprint ↔ Lean equivalence and status
No .tex files were changed. The modified declaration MPSTensor.cross_correlation_tendsto_zero has a blueprint entry at ch07_spectral.tex lines 557–569.
A.1 Mathematical equivalence. The Lean signature is unchanged by this PR. Comparing it against the blueprint statement:
| Blueprint | Lean |
|---|---|
| injective |
IsInjective A, IsInjective B ✓ |
| normalized |
∑ i, (A i)ᴴ * A i = 1, ∑ i, (B i)ᴴ * B i = 1 ✓ |
| not gauge-phase equivalent |
¬ GaugePhaseEquiv A B ✓ |
X : Matrix (Fin D) (Fin D) ℂ ✓ |
|
Filter.Tendsto (fun N => Matrix.trace (((mixedTransferMap A B)^N) X)) Filter.atTop (nhds 0) ✓ |
No quantifier weakening, conclusion drift, or indexing mismatch.
A.2 \leanok accuracy. Both the statement \leanok (line 559) and the proof \leanok (line 566) remain valid. The new proof body contains no sorry or admit; it applies mixedTransfer_pow_tendsto_zero and Matrix.traceLinearMap_apply to close the goal completely.
A.3 \notready. No \notready tags in scope.
A.4 Tag presence. No declarations were added or renamed; no \lean{...} tags need updating.
Category B — Prose quality
All lines changed by this PR are Lean proof tactics (let, simpa, rw, funext, exact). No docstrings, comments, section names, or blueprint prose were modified. Nothing to flag.
Review:
|
claude
Bot
added
cleanup
|
PR cleanup
Issue search performed: branch name ( Conventions: CONTRIBUTING.md |
There was a problem hiding this comment.
Review Summary
Verdict: APPROVE — no blockers or required changes found.
This is a clean, proof-only refactor in TNLean/Spectral/CrossCorrelation.lean that replaces the ad-hoc LinearMap.continuous_of_finiteDimensional continuity proof for Matrix.traceLinearMap with the bundled ContinuousLinearMap via LinearMap.toContinuousLinearMap. The theorem statement (cross_correlation_tendsto_zero) is unchanged.
Category-by-category assessment:
| Category | Status |
|---|---|
| 🔴 Proof integrity | ✅ No sorry, axiom, or kernel bypasses |
| 🔴 Proof correctness | ✅ tr.continuous.tendsto 0 with .comp h is mathematically valid; tr 0 = 0 definitionally; final rw step correctly converts composition to Matrix.trace |
| 🟡 Mathlib style | ✅ Idiomatic use of ContinuousLinearMap; let binding is clear |
| 🔴 Type safety | ✅ Finite-dimensionality instances available for Fin D matrices |
| 🟡 Performance | ✅ Simple analytic composition; no heavy tactics |
| 🟡 Modularity | ✅ No new definitions introduced |
| 🟡 Documentation | ✅ Existing docstrings are sufficient and unchanged |
| 🟡 Paper-gap notes | N/A |
No inline review threads or PR conversation comments exist on this PR.
LionSR
force-pushed
the
codex/cross-correlation-trace-clm
branch
from
52043c6 to
1246f50
Compare
There was a problem hiding this comment.
Review: refactor(Spectral): use trace CLM for cross correlations
Verdict: Approve. No 🔴 or 🟡 issues found.
I verified this end-to-end:
lake build TNLean.Spectral.CrossCorrelationcompletes successfully (3494 jobs), so the rewritten proof ofcross_correlation_tendsto_zerotype-checks.- No
sorry,axiom, or other proof-integrity blockers are introduced. - The theorem signature (statement, hypotheses
hA,hB,hA_norm,hB_norm,hAB, and conclusion) is byte-for-byte unchanged — only the proof body ofcross_correlation_tendsto_zerodiffers, consistent with the PR description. LinearMap.toContinuousLinearMapandMatrix.traceLinearMap_applyboth exist in the pinned Mathlib (v4.31.0) and are used correctly; the composition(tr.continuous.tendsto 0).comp hagainstmixedTransfer_pow_tendsto_zerois sound (tr 0 = 0discharged bysimpa).
ℹ️ Advisory (non-blocking): the new proof is longer than necessary
The PR motivation describes the result as "a single composition chain," but the new body (lines 62–74) is actually more verbose than the one it replaces (~12 lines vs. the prior ~5). In particular, Matrix.traceLinearMap is defined with toFun := trace (Mathlib Matrix/Trace.lean:91) and tagged @[simps], so Matrix.traceLinearMap_apply is a definitional (rfl) lemma. That means the composition
(Matrix.traceLinearMap (Fin D) ℂ ℂ) ∘ fun N => ((mixedTransferMap A B) ^ N) X
is already definitionally fun N => Matrix.trace (((mixedTransferMap A B) ^ N) X), making the entire rw [show … = …] block on lines 69–73 redundant. The proof from have h onward could collapse to roughly:
have h := mixedTransfer_pow_tendsto_zero A B hA hB hA_norm hB_norm hAB X
let tr : Matrix (Fin D) (Fin D) ℂ →L[ℂ] ℂ :=
LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin D) ℂ ℂ)
simpa [tr] using (tr.continuous.tendsto 0).comp hwhich keeps the stated goal (the Matrix.trace form) and the Mathlib-native CLM. This is a clarity suggestion only and does not block merge.
There was a problem hiding this comment.
Review Summary
Verdict: APPROVE — no 🔴 blockers or 🟡 required changes found.
This is a clean, proof-only refactor in TNLean/Spectral/CrossCorrelation.lean that replaces the ad-hoc LinearMap.continuous_of_finiteDimensional continuity proof with the bundled ContinuousLinearMap via LinearMap.toContinuousLinearMap. The theorem statement (cross_correlation_tendsto_zero) is unchanged.
Category-by-category
| Category | Status |
|---|---|
| 🔴 Proof integrity | ✅ No sorry, axiom, or kernel bypasses. Build succeeds. |
| 🔴 Proof correctness | ✅ (tr.continuous.tendsto 0).comp h is valid — trace is linear (tr 0 = 0) and continuous; the composition correctly sends the transfer-operator limit to the trace limit. The rw step via Matrix.traceLinearMap_apply converts the composition to the goal form. |
| 🟡 Mathlib style | ✅ Idiomatic use of ContinuousLinearMap via LinearMap.toContinuousLinearMap. The let binding is clear. Tactics are correctly applied. (The two-step h2 + rw structure is slightly verbose but not a style violation — see advisory note.) |
| 🔴 Type safety | ✅ Finite-dimensionality instances available for Fin D matrices through the import chain. |
| 🟡 Performance | ✅ Simple analytic composition — no heavy tactics. |
| 🟡 Modularity & duplication | ✅ No new definitions; uses standard Mathlib abstractions. |
| 🟡 Documentation | ✅ Existing docstrings are sufficient and unchanged. |
| 🟡 Paper-gap notes | N/A |
Advisory note (ℹ️, non-blocking)
The proof body could be shortened from ~11 lines to ~3 lines by combining the h2 and rw steps:
simpa [tr, Matrix.traceLinearMap_apply] using (tr.continuous.tendsto 0).comp hThe current two-step approach is correct and clear — this is a style preference, not a requirement.
No inline review threads exist on this PR; no prior feedback to resolve.
There was a problem hiding this comment.
Review: refactor(Spectral): use trace CLM for cross correlations
Verdict: REQUEST_CHANGES — one outstanding 🟡 (simplification), carried over from the previous review cycle and not addressed by the latest commit. Scope is a single proof-only change to the body of cross_correlation_tendsto_zero in TNLean/Spectral/CrossCorrelation.lean.
🔴 Proof integrity — clean
No sorry/axiom/admit/native_decide/kernel bypass introduced. No maxHeartbeats bump or debug artifacts. The signature of cross_correlation_tendsto_zero (and its Tendsto (fun N ↦ Matrix.trace ((mixedTransferMap A B ^ N) X)) atTop (nhds 0) conclusion) is unchanged; only the proof body that commutes Matrix.trace past the mixed-transfer limit is rewritten. No faithfulness/paper-gap implications.
🔴 Proof correctness — sound
The argument is valid. tr := LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin D) ℂ ℂ) is well-typed (Matrix (Fin D) (Fin D) ℂ and ℂ are finite-dimensional, satisfying toContinuousLinearMap's FiniteDimensional requirement). (tr.continuous.tendsto 0).comp h gives Tendsto (tr ∘ fun N ↦ (mixedTransferMap A B)^N X) atTop (nhds (tr 0)), and tr 0 = 0 (a linear map) collapses the target to 0. The final traceLinearMap_apply rewrite back to Matrix.trace is correct.
🟡 Mathlib style / simplification — requires changes
See the inline comment on lines 69–74. The refactor is billed as a cleanup but is a net +5 lines, and the final rw [show … by funext N; exact …] at h2; exact h2 block is strictly more verbose than the one-line simpa [Matrix.traceLinearMap_apply] using h2 it replaced. Since Matrix.traceLinearMap_apply is a simp lemma (traceLinearMap is @[simps]), the closing step should collapse back to a simpa. Additionally, the refactor's justification is thin: both the removed LinearMap.continuous_of_finiteDimensional route and the new LinearMap.toContinuousLinearMap route rely equally on finite-dimensionality, so no lemma-dependency is actually eliminated.
Other categories — no issues
- 🔴 Type safety:
Fintype (Fin D)/ finite-dimensionality instances resolve as before; no universe or coercion concerns. - 🟡 Performance: no
decide/unboundedsimpover large types; trivially fast. - 🟡 Modularity / duplication: no new declarations; nothing upstreamable introduced.
- 🟡 Documentation / paper-gap: no new definitions, no
docs/paper-gaps/changes; the existing docstring still describes the (unchanged) statement.
Please either adopt the simpa form or add a one-line justification for the bundled-CLM phrasing, and confirm the result with lake build TNLean.Spectral.CrossCorrelation.
There was a problem hiding this comment.
Review: APPROVE ✅
This is a clean proof-only refactor in TNLean/Spectral/CrossCorrelation.lean — the proof of cross_correlation_tendsto_zero. The theorem statement, hypotheses, and transfer-gap argument are all unchanged.
Summary by category
| Category | Severity | Verdict |
|---|---|---|
| 🔴 Proof integrity | Blocker | ✅ Clean — no sorry, axiom, admit, native_decide, or unsafeCast |
| 🔴 Proof correctness | Blocker | ✅ Sound — LinearMap.toContinuousLinearMap is the correct Mathlib-native way to obtain continuity of the trace linear map; the composition (tr.continuous.tendsto 0).comp h correctly composes the limit with continuity |
| 🟡 Mathlib style | Requires changes | ✅ No violations — let binding with type ascription, simpa with explicit unfolding, and rw of a pointwise equality are all idiomatic |
| 🔴 Type safety | Blocker | ✅ No issues — tr : Matrix (Fin D) (Fin D) ℂ →L[ℂ] ℂ is the correct type |
| 🟡 Performance | Requires changes | ✅ No concerns — no decide on large types, simpa with bounded lemma set |
| 🟡 Modularity & duplication | Requires changes | ✅ No new lemmas introduced; change is proof-local |
| 🟡 Documentation | Requires changes | ✅ Existing docstrings unchanged; all theorems have documentation |
| 🟡 Paper-gap notes | Requires changes | ✅ N/A — no changes to docs/paper-gaps/ |
Summary: The change replaces LinearMap.continuous_of_finiteDimensional with LinearMap.toContinuousLinearMap, which is the preferred Mathlib abstraction — it bundles continuity and linearity together rather than computing them separately. The new proof is a small improvement in Mathlib idiom with no regression in clarity or performance.
LionSR
force-pushed
the
codex/cross-correlation-trace-clm
branch
from
1246f50 to
a97672b
Compare
There was a problem hiding this comment.
Blueprint ↔ Lean & Prose Review — 0 Category A issues, 0 Category B issues.
Category A (blueprint ↔ Lean equivalence): No blueprint .tex files are touched. The statement of cross_correlation_tendsto_zero is unchanged. No \leanok, \notready, or \lean{...} tags were added, removed, or moved. Nothing to check.
Category B (prose quality): The diff is entirely proof-body Lean code. No docstrings, block comments, section/namespace names, or blueprint prose are added or modified. The one existing in-proof comment (-- Compose: F^N(X) → 0 …) is unchanged and raises no issue.
Thread resolution: The prior claude inline thread (verbose rw [show …] at h2; exact h2 concern) is now outdated — the new commit already uses simpa throughout — and has been resolved.
There was a problem hiding this comment.
Review: refactor(Spectral): use trace CLM for cross correlations
Verdict: APPROVE. Proof-only refactor to cross_correlation_tendsto_zero in TNLean/Spectral/CrossCorrelation.lean; the single blocking item from the prior cycle is now resolved.
Verification
lake build TNLean.Spectral.CrossCorrelationsucceeds locally (3494 jobs, no errors). The only warning is the pre-existingCopyright too short!header-linter note shared by many files in the repo — not introduced by this PR.
Proof integrity 🔴 — clean
No sorry/axiom/native_decide/kernel bypass. The signature of cross_correlation_tendsto_zero (statement, hypotheses, conclusion) is byte-for-byte unchanged; only the proof body that commutes Matrix.trace past the mixedTransferMap limit is rewritten.
Proof correctness 🔴 — sound
tr := LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin D) ℂ ℂ) is well-typed (both source and target are finite-dimensional, satisfying the FiniteDimensional requirement). (tr.continuous.tendsto 0).comp h gives convergence of tr ∘ (fun N ↦ (mixedTransferMap A B)^N X) to tr 0 = 0, and Matrix.traceLinearMap_apply (a simp lemma, since traceLinearMap is @[simps]) rewrites back to Matrix.trace. Sound.
Mathlib style / simplification 🟡 — addressed
The prior cycle flagged the final step as a net regression (a multi-line rw [show … by funext …] at h2; exact h2 block replacing a one-liner). The new commit adopts exactly the requested form:
simpa [tr, Function.comp_def, Matrix.traceLinearMap_apply] using
(tr.continuous.tendsto 0).comp hFunction.comp_def is the appropriate modern lemma. The prior claude review thread is already resolved/outdated. No remaining style concern.
Other categories — no issues
- Type safety 🔴: instances (
Fintype (Fin D), finite-dimensionality) resolve as before; no universe/coercion concerns. - Performance 🟡: trivially fast (2.4s build of the module); no
decide/unboundedsimpover large types. - Modularity / Documentation / Paper-gap 🟡: no new declarations, no docstring or
docs/paper-gaps/changes required for a proof-body refactor.
There was a problem hiding this comment.
Review: refactor(Spectral): use trace CLM for cross correlations
Verdict: APPROVE — no 🔴 blockers or 🟡 required changes.
This is a clean, proof-only refactor of cross_correlation_tendsto_zero in TNLean/Spectral/CrossCorrelation.lean. The theorem statement, hypotheses, and transfer-gap argument are unchanged; only the proof body is rewritten to use LinearMap.toContinuousLinearMap instead of the ad-hoc LinearMap.continuous_of_finiteDimensional route.
Category-by-category assessment
| Category | Severity | Status |
|---|---|---|
| 🔴 Proof integrity | Blocker | ✅ No sorry, axiom, admit, native_decide, unsafeCast, or kernel bypasses. Build succeeds (3494/3494 jobs). |
| 🔴 Proof correctness | Blocker | ✅ (1) tr : Matrix (Fin D) (Fin D) ℂ →L[ℂ] ℂ is well-typed — finite-dimensionality instances resolve through the import chain. (2) (tr.continuous.tendsto 0).comp h composes the limit from mixedTransfer_pow_tendsto_zero ((mixedTransferMap A B)^N X → 0) with continuity of tr, yielding tr ∘ (λ N ↦ …) → tr 0 = 0. (3) simpa [tr, Function.comp_def, Matrix.traceLinearMap_apply] correctly unpacks tr, the composition, and the linear-map application to match the h2 goal. (4) Final simpa [Matrix.traceLinearMap_apply] converts traceLinearMap to Matrix.trace exactly as the theorem conclusion requires. |
| 🟡 Mathlib style | Requires changes | ✅ Idiomatic: let binding with type ascription, simpa with explicit lemma sets. The two-step structure (h2 intermediate goal) separates the continuity composition from the algebraic rewriting — a conventional and readable pattern. The prior review's concern (verbose rw [show …] block on commit 1246f50) has been addressed in commit a97672b. |
| 🔴 Type safety | Blocker | ✅ Fintype (Fin D) and finite-dimensionality instances resolve as before. No universe or coercion issues. |
| 🟡 Performance | Requires changes | ✅ Simple simpa with bounded lemma sets; no decide on large types. Trivially fast. |
| 🟡 Modularity & duplication | Requires changes | ✅ No new definitions or lemmas introduced. Uses standard Mathlib abstractions. |
| 🟡 Documentation | Requires changes | ✅ Existing docstrings are unchanged and sufficient. Theorem documentation is accurate. |
| 🟡 Paper-gap notes | Requires changes | ✅ N/A — no changes to docs/paper-gaps/. |
Prior review thread resolution
The single inline review thread from the previous cycle (PRRT_kwDORK8b986K9j8g, on the old rw [show …] at h2; exact h2 block) is already isResolved: true and isOutdated: true — commit a97672b replaced that block with clean simpa calls, resolving the concern.
2 participants
Motivation
cross_correlation_tendsto_zeroinTNLean/Spectral/CrossCorrelation.leanestablished continuity of the trace functional viaLinearMap.continuous_of_finiteDimensional, a one-off step that reconstructs whatLinearMap.toContinuousLinearMapprovides directly as a Mathlib-nativeContinuousLinearMap. Using the latter makes the limit argument a single composition chain without an intermediateContinuoushypothesis.Description
TNLean/Spectral/CrossCorrelation.lean— proof body ofcross_correlation_tendsto_zeroonly:Matrix.traceLinearMapis now obtained viaLinearMap.toContinuousLinearMaprather thanLinearMap.continuous_of_finiteDimensional..continuous.tendsto 0withmixedTransfer_pow_tendsto_zeroand rewriting toMatrix.traceusingMatrix.traceLinearMap_apply.Testing
lake exe cache getlake build TNLean.Spectral.CrossCorrelation -q --log-level=infopython3 scripts/check_reader_facing_prose.py --root . --diff-base origin/mainpython3 scripts/blueprint_lean_sync.py --root . --cigit diff --checkandgit diff --cached --check(no trailing whitespace)Note
Low Risk
Proof-only refactor in spectral theory; no API or mathematical statement changes.
Overview
cross_correlation_tendsto_zerois unchanged at the statement level; only the Lean proof that trace commutes with the mixed-transfer limit is rewritten.Instead of a one-off
Continuous (Matrix.traceLinearMap …)viaLinearMap.continuous_of_finiteDimensional, the proof now packages trace as a continuous linear map withLinearMap.toContinuousLinearMap, appliestr.continuous.tendsto 0composed withmixedTransfer_pow_tendsto_zero, and rewrites back toMatrix.traceusingMatrix.traceLinearMap_apply.Reviewed by Cursor Bugbot for commit 52043c6. Bugbot is set up for automated code reviews on this repo. Configure here.
Note
Low Risk
Proof-only change in spectral theory with no API or mathematical statement changes.
Overview
cross_correlation_tendsto_zerois unchanged at the statement level; only the Lean proof that trace commutes with the mixed-transfer limit is rewritten.The proof no longer builds
Continuous (Matrix.traceLinearMap …)withLinearMap.continuous_of_finiteDimensionaland a manualcontinuousAt.tendsto.compstep. It introducestrasLinearMap.toContinuousLinearMap (Matrix.traceLinearMap …), derives convergence on the linear-map formulation with(tr.continuous.tendsto 0).compapplied tomixedTransfer_pow_tendsto_zero, then rewrites toMatrix.traceviaMatrix.traceLinearMap_apply.Reviewed by Cursor Bugbot for commit a97672b. Bugbot is set up for automated code reviews on this repo. Configure here.