refactor(Channel/Irreducible): use CLM for corner convergence

[LionSR]

Motivation

The irreducibility-from-spectral proof transported a Cesaro subsequence limit through the corner map by proving continuity from finite dimensionality. The corner map is already a linear map, so Mathlib 4.31 can bundle it as a continuous linear map directly.

Description

This PR replaces the proof-local LinearMap.continuous_of_finiteDimensional use for sandwichLinearMap P P with LinearMap.toContinuousLinearMap. The theorem statement and invariant-corner argument are unchanged.

• File modified: TNLean/Channel/Irreducible/FromSpectral.lean

Testing

• lake exe cache get
• lake build TNLean.Channel.Irreducible.FromSpectral -q --log-level=info
• python3 scripts/check_reader_facing_prose.py --root . --diff-base origin/main
• python3 scripts/blueprint_lean_sync.py --root . --ci
• git diff --check HEAD~1..HEAD
• git diff --cached --check

---

Note

Low Risk
Proof-only refactor in one lemma; no statement or API changes, only a different Mathlib continuity route for the same limit step.

Overview
In isIrreducibleMap_of_channel_posDef_fixedPoint_unique, the proof that Cesàro means converge inside the corner P · · · P now goes through LinearMap.toContinuousLinearMap (sandwichLinearMap P P) instead of invoking LinearMap.continuous_of_finiteDimensional on that map ad hoc.

The argument is unchanged: rewrite the sequence as composition with sandwichLinearMap, apply continuous.tendsto, then relate back to P * … * P. This matches how sandwichLinearMap continuity is handled elsewhere (e.g. SpectralRadius.lean).

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

---

Note

Low Risk
Single-lemma proof refactor with no statement or API changes; only the Mathlib continuity route for the same limit step.

Overview
In isIrreducibleMap_of_channel_posDef_fixedPoint_unique, the step showing Cesàro subsequence limits commute with the corner map P · · · P no longer calls LinearMap.continuous_of_finiteDimensional on sandwichLinearMap P P.

The proof now packages that map as LinearMap.toContinuousLinearMap (sandwichLinearMap P P), rewrites the limit as composition with sandwichLinearMap, and applies corner.continuous.tendsto. The target limit and the rest of the invariant-corner argument are unchanged.

This aligns with how sandwichLinearMap continuity is obtained elsewhere (e.g. SpectralRadius.lean).

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

[claude]

Blueprint ↔ Lean equivalence and status (Category A): No issues. The PR modifies only the proof body of a have step inside isIrreducibleMap_of_channel_posDef_fixedPoint_unique. The theorem statement is unchanged, no Lean declarations are added or renamed, and no .tex files are modified. The theorem has no blueprint entry, so there are no \lean{...}, \leanok, or \notready tags to check.

Prose quality (Category B): No issues. The diff touches only proof-tactic lines — no docstrings, comments, section names, or blueprint prose are modified.

0 equivalence mismatches, 0 stale status tags, 0 prose issues.

[claude]

PR cleanup

Field	Before	After
Title	refactor(Channel/Irreducible): use CLM for corner convergence	unchanged — already compliant
Body	Missing --- footer; Cursor Bugbot block embedded in HTML comment	Restructured: three template sections kept, --- footer added with note about missing issue, Cursor Bugbot block preserved verbatim after footer
Labels	(none)	added: cleanup
Issue	No linked issue found — branch codex/irreducible-corner-clm carries no issue-{N} segment; PR body, commits, and open/closed issue search found no match. Please add Addresses #N to the footer when a tracking issue is opened or identified.

Conventions: CONTRIBUTING.md

[claude]

Review: refactor(Channel/Irreducible): use CLM for corner convergence

Proof-only refactor of one have step (hcorner_tendsto) inside isIrreducibleMap_of_channel_posDef_fixedPoint_unique in TNLean/Channel/Irreducible/FromSpectral.lean. The theorem statement and the surrounding invariant-corner argument are unchanged.

Proof integrity 🔴 — OK

No sorry, axiom, native_decide, admit, or kernel bypass introduced. The edit only swaps the route for proving a single continuity-of-corner limit.

Proof correctness 🔴 — OK

The new proof is sound by definitional reduction:

• sandwichLinearMap L R is defined with toFun X := L * X * R (FromSpectral.lean:68). Hence sandwichLinearMap P P σ is definitionally P * σ * P and (sandwichLinearMap P P ∘ fun k => cesaroMean E ρ₀ (φ k + 1)) k is P * cesaroMean E ρ₀ (φ k + 1) * P. The change at lines 330–332 is therefore valid defeq.
• corner.continuous.tendsto σ |>.comp hσ_tendsto yields Tendsto (⇑corner ∘ fun k => cesaroMean …) atTop (nhds (corner σ)). The final simpa [corner] rewrites ⇑corner to ⇑(sandwichLinearMap P P) via the @[simp] rfl lemma ContinuousLinearMap.coe_toContinuousLinearMap' (Mathlib Topology/Algebra/Module/FiniteDimension.lean:314), matching the changed goal.

This mirrors the established pattern at TNLean/Channel/Irreducible/SpectralRadius.lean:131, so it is consistent with how sandwichLinearMap continuity is handled elsewhere.

Style / type safety / performance / docs 🟡 — OK

No naming, import, coercion, or performance concerns; no documentation surface changed.

ℹ️ Advisory (non-blocking)

Because coe_toContinuousLinearMap' is rfl, the let corner binding is pure indirection — the step could be written directly as simpa using ((LinearMap.toContinuousLinearMap (sandwichLinearMap (D := D) P P)).continuous.tendsto σ).comp hσ_tendsto. Keeping the named binding is fine and arguably more readable; purely a matter of taste.

Note: I confirmed the change by definitional inspection and by verifying the cited Mathlib simp lemma; I did not run a full lake build (dependency oleans were not present in the local checkout). The PR description reports a successful lake build TNLean.Channel.Irreducible.FromSpectral.

No 🔴 or 🟡 issues. Approving.

[claude]

Review Summary

This PR replaces a proof-local LinearMap.continuous_of_finiteDimensional call for sandwichLinearMap P P with LinearMap.toContinuousLinearMap in the Cesàro corner-convergence step of isIrreducibleMap_of_channel_posDef_fixedPoint_unique. The theorem statement and the rest of the proof are unchanged.

Category-by-category assessment

Category	Severity	Status
1. Proof integrity	🔴 Blocker	✅ Pass
2. Proof correctness	🔴 Blocker	✅ Pass
3. Mathlib style	🟡 Requires changes	✅ Pass
4. Type safety	🔴 Blocker	✅ Pass
5. Performance	🟡 Requires changes	✅ Pass
6. Modularity & duplication	🟡 Requires changes	✅ Pass
7. Documentation	🟡 Requires changes	✅ Pass
8. Paper-gap notes	🟡 Requires changes	✅ Pass

1. Proof integrity — No sorry, admit, axiom, native_decide, unsafeCast, or any other blocked pattern in the diff. No set_option maxHeartbeats changes. ✅

2. Proof correctness — The mathematical argument is unchanged. LinearMap.toContinuousLinearMap bundles the same finite-dimensional continuity of sandwichLinearMap P P into a ContinuousLinearMap. The change instruction correctly rewrites P * X * P as (sandwichLinearMap P P) X (definitional by the toFun clause of sandwichLinearMap), and (corner.continuous.tendsto σ).comp hσ_tendsto transports the Cesàro subsequence limit through the corner map. The simpa [corner] resolves the toContinuousLinearMap unfolding (definitional since ContinuousLinearMap extends LinearMap in Mathlib 4). ✅

3. Mathlib style — The let corner : … →L[ℂ] … pattern matches the project's existing usage in SpectralRadius.lean:131-133. No naming or style violations. ✅

4. Type safety — Correct type annotation Matrix (Fin D) (Fin D) ℂ →L[ℂ] Matrix (Fin D) (Fin D) ℂ. All instances (FiniteDimensional, ContinuousSMul) are available through existing imports. ✅

5. Performance — Local proof refactor with no performance impact. ✅

6. Modularity & duplication — Aligns this usage with the preferred LinearMap.toContinuousLinearMap idiom already used in SpectralRadius.lean and elsewhere in Channel/Semigroup/. The sandwichLinearMap remains private as before. ✅

7. Documentation — No new declarations; no missing docstrings introduced. ✅

8. Paper-gap notes — No paper-gap note changes. ✅

Verdict: APPROVE

No issues found across any review category. The change is a clean, low-risk proof refactor that uses the idiomatic Mathlib 4 API for finite-dimensional continuity.

[claude]

Blueprint ↔ Lean equivalence and status (Category A): 0 issues

No .tex blueprint files are changed in this PR. The theorem isIrreducibleMap_of_channel_posDef_fixedPoint_unique has no blueprint entry, so there are no \lean{...}, \leanok, or \notready tags to validate. The theorem signature is unchanged — only the proof tactic for the hcorner_tendsto sub-goal is rewritten. No sorry or admit is present in the file.

Prose quality (Category B): 0 issues

The diff touches only the tactic proof body. No docstrings, comments, section names, or namespace names are modified, so there is nothing in scope for prose review.

0 equivalence mismatches, 0 stale status tags, 0 prose issues.

[claude]

Review: refactor(Channel/Irreducible): use CLM for corner convergence

Proof-only refactor in one have step (hcorner_tendsto) inside isIrreducibleMap_of_channel_posDef_fixedPoint_unique. The theorem statement and invariant-corner argument are unchanged.

Category-by-category assessment

Category	Severity	Status
1. Proof integrity	🔴 Blocker	✅ Pass
2. Proof correctness	🔴 Blocker	✅ Pass
3. Mathlib style	🟡 Requires changes	✅ Pass
4. Type safety	🔴 Blocker	✅ Pass
5. Performance	🟡 Requires changes	✅ Pass
6. Modularity & duplication	🟡 Requires changes	✅ Pass
7. Documentation	🟡 Requires changes	✅ Pass
8. Paper-gap notes	🟡 Requires changes	✅ Pass

1. Proof integrity — No sorry, admit, axiom, native_decide, unsafeCast, or any blocked pattern in the diff. No set_option maxHeartbeats changes. ✅

2. Proof correctness — Sound by definitional reduction. sandwichLinearMap (line 68) defines toFun X := L * X * R, so P * σ * P is definitionally (sandwichLinearMap P P) σ. The change instruction at lines 330–332 rewrites the goal faithfully. corner.continuous.tendsto σ composed with hσ_tendsto transports the Cesàro subsequence limit through the corner map. simpa [corner] resolves because let corner unfolds definitionally and ⇑(toContinuousLinearMap f) is definitionally ⇑f (via the rfl lemma coe_toContinuousLinearMap' in Mathlib Topology/Algebra/Module/FiniteDimension.lean:314). ✅

3. Mathlib style — The let corner : … →L[ℂ] … binding matches the existing usage at SpectralRadius.lean:131-133. No naming or style violations. ✅

4. Type safety — Correct type annotation Matrix (Fin D) (Fin D) ℂ →L[ℂ] Matrix (Fin D) (Fin D) ℂ. All instances available through existing imports. ✅

5. Performance — Local tactical refactor with no impact on proof elaboration time. ✅

6. Modularity & duplication — Aligns this location with the LinearMap.toContinuousLinearMap idiom already established at SpectralRadius.lean:131-133 and elsewhere in Channel/Semigroup/. ✅

7. Documentation — No new declarations; no missing docstrings introduced. ✅

8. Paper-gap notes — No paper-gap note changes. ✅

Verdict: APPROVE

No issues found across any review category. The change is a clean, low-risk refactor that replaces ad-hoc finite-dimensional continuity with the idiomatic Mathlib 4 LinearMap.toContinuousLinearMap API, consistent with the project's existing pattern.

[claude]

Review: APPROVE

Proof-only refactor of the corner-convergence step hcorner_tendsto inside isIrreducibleMap_of_channel_posDef_fixedPoint_unique (TNLean/Channel/Irreducible/FromSpectral.lean:325-333). The ad-hoc LinearMap.continuous_of_finiteDimensional (sandwichLinearMap P P) call is replaced by a bundled LinearMap.toContinuousLinearMap (sandwichLinearMap (D := D) P P). The theorem statement and the rest of the invariant-corner argument are unchanged.

Proof integrity 🔴 — clear

No sorry, admit, axiom, native_decide, or kernel-bypass introduced. The diff only swaps the continuity route for the same limit step.

Proof correctness 🔴 — verified by inspection

The rewrite is sound:

• sandwichLinearMap L R has toFun X := L * X * R (line 68), so sandwichLinearMap P P X = P * X * P definitionally. The change to Tendsto ((sandwichLinearMap P P) ∘ fun k => cesaroMean E ρ₀ (φ k + 1)) atTop (nhds ((sandwichLinearMap P P) σ)) therefore holds by defeq: (sandwichLinearMap P P ∘ g) k = P * g k * P and nhds (sandwichLinearMap P P σ) = nhds (P * σ * P).
• (corner.continuous.tendsto σ).comp hσ_tendsto yields Tendsto (corner ∘ (fun k => cesaroMean …)) atTop (nhds (corner σ)), and simpa [corner] reconciles the ContinuousLinearMap coercion (LinearMap.toContinuousLinearMap f x = f x) with the LinearMap coercion in the changed goal.
• All hypotheses remain used; hσ_tendsto feeds the composition, and the downstream tendsto_nhds_unique hcorner_tendsto hcorner_tendsto' argument is untouched.

This matches the established continuity idiom for sandwichLinearMap already used at TNLean/Channel/Irreducible/SpectralRadius.lean:131-133, improving consistency.

Mathlib style 🟡 — clean

Naming and tactic style are consistent with the surrounding proof and with the cited SpectralRadius.lean usage.

Type safety / Performance / Modularity / Documentation — no concerns

No new universe, instance, or coercion hazards; no new lemmas requiring docstrings; private sandwichLinearMap unchanged.

I could not type-check the file standalone in this environment (local TNLean dependency oleans are not built and a full lake build of the dependency tree is impractical here), but the change is defeq-trivial and the PR reports a successful lake build TNLean.Channel.Irreducible.FromSpectral. No 🔴 or 🟡 issues found.

ℹ️ Advisory (non-blocking): the let corner := … binding is only consumed in the final simpa [corner], while the change spells out sandwichLinearMap (D := D) P P directly. This is readable as written; it could be tightened (e.g. drop the let and inline, or drop the change and let simpa close the goal) if a smaller proof body is preferred.

[claude]

Review: refactor(Channel/Irreducible): use CLM for corner convergence

Proof-only refactor of one have step (hcorner_tendsto) inside isIrreducibleMap_of_channel_posDef_fixedPoint_unique (TNLean/Channel/Irreducible/FromSpectral.lean:325-333). The ad-hoc LinearMap.continuous_of_finiteDimensional (sandwichLinearMap P P) call is replaced by the bundled LinearMap.toContinuousLinearMap (sandwichLinearMap (D := D) P P). The theorem statement and the rest of the invariant-corner argument are unchanged.

Category-by-category assessment

Category	Severity	Status
1. Proof integrity	🔴 Blocker	✅ Pass
2. Proof correctness	🔴 Blocker	✅ Pass
3. Mathlib style	🟡 Requires changes	✅ Pass
4. Type safety	🔴 Blocker	✅ Pass
5. Performance	🟡 Requires changes	✅ Pass
6. Modularity & duplication	🟡 Requires changes	✅ Pass
7. Documentation	🟡 Requires changes	✅ Pass
8. Paper-gap notes	🟡 Requires changes	✅ Pass

1. Proof integrity — No sorry, admit, axiom, native_decide, unsafeCast, or any other blocked pattern in the diff. No set_option maxHeartbeats changes.

2. Proof correctness — Sound by definitional reduction:

• sandwichLinearMap L R (line 68) defines toFun X := L * X * R, so (sandwichLinearMap P P) σ is definitionally P * σ * P and (sandwichLinearMap P P ∘ f) k = P * f k * P. The change at lines 330–332 is therefore valid by defeq.
• (corner.continuous.tendsto σ).comp hσ_tendsto yields Tendsto (corner ∘ (fun k => cesaroMean …)) atTop (nhds (corner σ)).
• simpa [corner] resolves the ContinuousLinearMap → function coercion because ContinuousLinearMap extends LinearMap, making the coercion definitionally equal to the underlying LinearMap.toFun. The let corner := … is unfolded, yielding (sandwichLinearMap P P) ∘ … and (sandwichLinearMap P P) σ, matching the changed goal exactly.

This mirrors the established pattern at TNLean/Channel/Irreducible/SpectralRadius.lean:131-133.

3. Mathlib style — The let corner : … →L[ℂ] … binding and LinearMap.toContinuousLinearMap pattern matches the project's existing usage. Naming and tactic style are consistent with the surrounding proof.

4. Type safety — Correct type annotation Matrix (Fin D) (Fin D) ℂ →L[ℂ] Matrix (Fin D) (Fin D) ℂ. All required instances (FiniteDimensional, ContinuousSMul) are available through existing imports.

5. Performance — Local tactical refactor with no impact on proof elaboration time. No decide on large types, no unbounded simp, no deep rw chains.

6. Modularity & duplication — Aligns this location with the LinearMap.toContinuousLinearMap idiom already established at SpectralRadius.lean:131-133 and elsewhere in Channel/Semigroup/.

7. Documentation — No new declarations introduced; no missing docstrings.

8. Paper-gap notes — No paper-gap note changes.

Verdict: APPROVE

No 🔴 or 🟡 issues found across any review category. The change is a clean, low-risk proof refactor that replaces ad-hoc finite-dimensional continuity with the idiomatic Mathlib 4 LinearMap.toContinuousLinearMap API, consistent with the project's existing pattern.

[claude]

Review: refactor(Channel/Irreducible): use CLM for corner convergence

Verdict: Approve. No 🔴 or 🟡 issues found.

This is a tightly-scoped proof-only refactor of the hcorner_tendsto step inside isIrreducibleMap_of_channel_posDef_fixedPoint_unique (TNLean/Channel/Irreducible/FromSpectral.lean:325-333). The theorem statement and the rest of the invariant-corner argument are unchanged.

Proof integrity 🔴 — clean

No sorry, admit, axiom, native_decide, or other blockers introduced (the only axiom/sorry-substring hit in the file is the word inside the HasSpectralProperties docstring at line 179, not an actual blocker).

Proof correctness 🔴 — sound, and verified by build

The new route is logically equivalent to the old one:

• The change rewrites the goal to Tendsto ((sandwichLinearMap P P) ∘ fun k => cesaroMean E ρ₀ (φ k + 1)) atTop (nhds ((sandwichLinearMap P P) σ)). This holds by definitional equality, since sandwichLinearMap P P has toFun X := P * X * P (FromSpectral.lean:65-72), so (sandwichLinearMap P P) X is defeq to P * X * P and nhds ((sandwichLinearMap P P) σ) is defeq to nhds (P * σ * P).
• (corner.continuous.tendsto σ).comp hσ_tendsto yields Tendsto (corner ∘ fun k => cesaroMean …) atTop (nhds (corner σ)), and simpa [corner] discharges the coercion of LinearMap.toContinuousLinearMap back to the underlying linear map.

I independently confirmed the file compiles: lake build TNLean.Channel.Irreducible.FromSpectral exits 0. The only emitted warnings are the pre-existing Copyright too short! header-linter warnings shared by every file in Channel/Irreducible/ (Similarity, PerronFrobenius, Ergodicity, SpectralRadius, FromSpectral) — not introduced by this PR.

Type safety / performance / modularity / docs — no concerns

Build time for the file is ~11s; no new definitions or API surface.

ℹ️ Advisory (non-blocking)

The replaced one-liner (exact ((LinearMap.continuous_of_finiteDimensional (sandwichLinearMap P P)).tendsto σ).comp hσ_tendsto) was shorter than the new let/change/simpa block, and LinearMap.continuous_of_finiteDimensional is not deprecated — so the change is stylistic rather than a correctness or maintenance fix. The stated rationale (matching how sandwichLinearMap continuity is obtained in SpectralRadius.lean:131-133 via LinearMap.toContinuousLinearMap) is reasonable, and the consistency benefit is a fair justification. Optionally, the let corner binding could be inlined since it is used only in the final simpa, but this is purely cosmetic.

Approving — the change is correct, in-scope, and builds.

[claude]

Blueprint ↔ Lean equivalence and status (Category A): 0 issues

No .tex files are changed. No declarations are added, removed, or renamed. The statement of isIrreducibleMap_of_channel_posDef_fixedPoint_unique is unchanged, so the blueprint's existing \lean{...} tag and \leanok markers remain accurate. Nothing to flag.

Prose quality (Category B): 0 issues

The only changed text is a tactic-local let corner binding inside a proof block. No docstrings, comments, section names, or blueprint prose are touched. Nothing to flag.

Summary: 0 equivalence mismatches, 0 stale \leanok, 0 prose issues.

[claude]

Review Summary

This PR replaces a direct LinearMap.continuous_of_finiteDimensional invocation in the proof of isIrreducibleMap_of_channel_posDef_fixedPoint_unique with LinearMap.toContinuousLinearMap, matching the continuity pattern already established in SpectralRadius.lean (lines 131, 133).

Findings by Category

Category	Severity	Result
🔴 Proof integrity	Blocker	✅ No issues — no sorry, axiom, native_decide, or circular reasoning
🔴 Proof correctness	Blocker	✅ Correct — sandwichLinearMap is definitionally transparent, change is valid, simpa closes via definitional reduction of toContinuousLinearMap
🟡 Mathlib style	Requires changes	✅ No issues — consistent with existing patterns, line lengths within 100 chars, no unnecessary imports
🔴 Type safety	Blocker	✅ No issues — LinearMap.toContinuousLinearMap is available via existing import chain
🟡 Performance	Requires changes	✅ No concerns — toContinuousLinearMap is O(1)
🟡 Modularity & duplication	Requires changes	✅ No issues — aligns with SpectralRadius.lean continuity pattern
🟡 Documentation	Requires changes	✅ N/A — proof-only refactor, no new declarations
🟡 Paper-gap notes	Requires changes	✅ N/A — no paper-gap changes

Verdict

APPROVE. The change is confined to a single proof block with no statement, API, or import changes. The new proof correctly packages sandwichLinearMap P P as a ContinuousLinearMap via toContinuousLinearMap, uses change to rewrite the goal to the map's functional form (definitionally valid since sandwichLinearMap.toFun X := P * X * P), and closes via ContinuousLinearMap.continuous.tendsto. This is mathematically equivalent to the old continuous_of_finiteDimensional path and consistent with the idiom used elsewhere in the module hierarchy.

[claude]

Review: refactor(Channel/Irreducible): use CLM for corner convergence

Verdict: Approve. No 🔴 blocker or 🟡 requires-changes issues found. One ℹ️ advisory note below.

What the PR does

Inside isIrreducibleMap_of_channel_posDef_fixedPoint_unique (TNLean/Channel/Irreducible/FromSpectral.lean:325), the proof of the hcorner_tendsto step — that the Cesàro subsequence limit commutes with the corner map P · P — replaces the ad-hoc LinearMap.continuous_of_finiteDimensional (sandwichLinearMap P P) with LinearMap.toContinuousLinearMap (sandwichLinearMap P P). The theorem statement and the rest of the invariant-corner argument are unchanged.

Findings by category

1. 🔴 Proof integrity — Clean. No sorry, axiom, native_decide, admit, or kernel-bypass introduced; the diff only swaps the continuity route for one limit step.
2. 🔴 Proof correctness — Sound and verified. sandwichLinearMap P P is defined with toFun X := P * X * P (FromSpectral.lean:65-68), so the change to the sandwichLinearMap-composition form holds by defeq, and simpa [corner] reduces ⇑(toContinuousLinearMap (sandwichLinearMap P P)) to the bare linear-map coercion before applying corner.continuous.tendsto σ |>.comp hσ_tendsto. I built the module locally — lake build TNLean.Channel.Irreducible.FromSpectral completes with exit code 0 (only pre-existing, repo-wide "Copyright too short!" header-linter warnings, not introduced here).
3. 🟡 Mathlib style — Acceptable. The chosen idiom (LinearMap.toContinuousLinearMap (sandwichLinearMap …)).continuous matches existing usage in TNLean/Channel/Irreducible/SpectralRadius.lean:131, so the PR's alignment claim is accurate. Line length within 100 chars; naming unchanged. (See advisory on conciseness.)
4. 🔴 Type safety — No issues. The explicit (D := D) named arguments are correctly supplied; no universe or coercion problems.
5. 🟡 Performance — No concern; a trivial proof-local change.
6. 🟡 Modularity & duplication — No new duplication; reuses the established CLM idiom.
7. 🟡 Documentation — N/A; proof-internal step, no docstring required.
8. 🟡 Paper-gap notes — N/A; no files under docs/paper-gaps/ changed.

ℹ️ Advisory (non-blocking)

The new proof is more verbose than necessary. The original step was a single exact, and exact already discharged the same coercion defeq. Since toContinuousLinearMap's coercion is defeq to the underlying LinearMap coercion, the same one-liner structure should work directly, making the let corner / change / simpa unnecessary:

exact ((LinearMap.toContinuousLinearMap
  (sandwichLinearMap (D := D) P P)).continuous.tendsto σ).comp hσ_tendsto

This would keep the diff to a true one-for-one swap and mirror the SpectralRadius.lean:131 idiom. Worth trying, but the current proof is correct and builds, so this does not block approval.