refactor(Channel/FixedPoint): use CLMs in Cesaro limits#3097
Conversation
|
PR cleanup
No linked issue was found after checking the branch name ( Conventions: CONTRIBUTING.md |
![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 status tags, 0 prose issues.
Category A — Blueprint ↔ Lean equivalence
Only proof bodies are changed; no .tex blueprint files and no theorem signatures are touched.
-
IsChannel.exists_posSemidef_fixedPointis linked inch04_channels.texline 362 (\lean{IsChannel.exists_posSemidef_fixedPoint}) with\leanokon both statement and proof. The Lean signature(hE : IsChannel E) (hD : 0 < D) : ∃ ρ, ρ.PosSemidef ∧ ρ ≠ 0 ∧ E ρ = ρmatches the blueprint's statement (channel$E$ on$\mathcal{M}_D$ with$D \ge 1$ , nonzero PSD fixed point). Nosorryoradmitpresent in either modified file, so both\leanoktags remain valid. -
IsChannel.cesaroMean_subseq_limit_fixedPointis a helper lemma with no blueprint entry; none is required. - No
\notreadytags affected.
Category B — Prose quality
No .tex files changed; no Lean docstrings or inline comments added or modified. Nothing to flag.
There was a problem hiding this comment.
Review: refactor(Channel/FixedPoint): use CLMs in Cesaro limits
Verdict: Approve. No 🔴 or 🟡 issues found.
This is a minimal, proof-only refactor that swaps the local continuity witness LinearMap.continuous_of_finiteDimensional E for the bundled E' := LinearMap.toContinuousLinearMap E in two limit arguments. The mathematical statements are unchanged.
Correctness
In both files E : Matrix (Fin D) (Fin D) ℂ →ₗ[ℂ] Matrix (Fin D) (Fin D) ℂ is a linear endomorphism of a finite-dimensional ℂ-space, so LinearMap.toContinuousLinearMap applies and rests on exactly the same finite-dimensionality used by the original continuous_of_finiteDimensional. The coercion of E' back to a function is definitionally E, so:
IsChannel.exists_posSemidef_fixedPoint(Cesaro.lean:295-296):simpa [E'] using (E'.continuous.tendsto ρ).comp hφ_tendstocorrectly re-derivesTendsto (E ∘ σ ∘ φ) atTop (nhds (E ρ)).IsChannel.cesaroMean_subseq_limit_fixedPoint(Ergodicity.lean:102-106): the addedchangetoE ∘ (fun k => cesaroMean E ρ (ψ k + 1))plussimpa [E']is the right shape;(E'.continuous.tendsto σ).comp hσ_tendstomatchesnhds (E σ).
The telescoping identities (cesaroMean_telescope) and the h_diff/h_rhs_zero limit chains are untouched and continue to feed tendsto_nhds_unique as before.
Checks
- Proof integrity: No
sorry/admit/axiom/native_decideintroduced. - Build:
lake build TNLean.Channel.FixedPoint.Cesaro TNLean.Channel.Irreducible.Ergodicitycompletes successfully (8631 jobs, exit 0). The only warnings are pre-existing "Copyright too short" header-linter notes, unrelated to this diff. - Style/type safety: The
let E' : … →L[ℂ] …binding is idiomatic and well-typed; no coercion or universe concerns. - Docs/paper-gaps: No statement, API, or
docs/paper-gaps/changes, so nothing to document.
Nice cleanup — leveraging the bundled finite-dimensional map removes the ad hoc continuity witnesses without altering any obligation.
There was a problem hiding this comment.
Review Summary
This is a clean, focused proof-only refactor that replaces local LinearMap.continuous_of_finiteDimensional continuity witnesses with Mathlib's bundled LinearMap.toContinuousLinearMap API in two Cesàro fixed-point theorems.
What changed
IsChannel.exists_posSemidef_fixedPoint(TNLean/Channel/FixedPoint/Cesaro.lean): replacedhE_cont : Continuous Ewithlet E' : ... →L[ℂ] ... := LinearMap.toContinuousLinearMap E, then usedE'.continuous.tendstoviasimpa.IsChannel.cesaroMean_subseq_limit_fixedPoint(TNLean/Channel/Irreducible/Ergodicity.lean): same replacement, with achangestep to align the goal's syntactic form forsimpa.
Category-by-category assessment
| Category | Verdict |
|---|---|
| 🔴 Proof integrity | ✅ No blockers — no sorry, axiom, native_decide, or kernel bypasses introduced |
| 🔴 Proof correctness | ✅ The mathematical logic is unchanged; LinearMap.toContinuousLinearMap produces the same Continuous property that continuous_of_finiteDimensional provided, now bundled as a ContinuousLinearMap |
| 🟡 Mathlib style | ✅ Idiomatic use of let, simpa, and change; type annotation on let binding is appropriate |
| 🔴 Type safety | ✅ Domain Matrix (Fin D) (Fin D) ℂ is finite-dimensional, so LinearMap.toContinuousLinearMap is valid |
| 🟡 Performance | ✅ No performance impact — both old and new are thin wrappers |
| 🟡 Modularity | ✅ This is a modularity improvement — it uses Mathlib's bundled CLM API instead of ad hoc continuity proofs |
| 🟡 Documentation | ✅ N/A — proof-internal change only; theorem docstrings already present |
| 🟡 Paper-gap notes | ✅ N/A — no paper-gap notes changed |
Build
lake build TNLean.Channel.FixedPoint.Cesaro TNLean.Channel.Irreducible.Ergodicity
# Build completed successfully (8631 jobs)No new warnings introduced.
Verdict
APPROVE. No 🔴 or 🟡 issues found. This is a minimal, well-scoped refactor that improves alignment with Mathlib conventions.
LionSR
force-pushed
the
codex/cesaro-limit-clms
branch
from
90bed29 to
50143f3
Compare
There was a problem hiding this comment.
Blueprint ↔ Lean sync and prose review — 0 equivalence mismatches, 0 stale status tags, 0 prose issues.
Category A — Blueprint ↔ Lean equivalence
No .tex blueprint files are changed. Both modified files touch only proof bodies inside have blocks, with no change to any theorem signature.
IsChannel.exists_posSemidef_fixedPointcarries\lean{IsChannel.exists_posSemidef_fixedPoint}and\leanokon both statement and proof in the blueprint. The Lean signature is unchanged and nosorryoradmitis introduced, so both tags remain valid.IsChannel.cesaroMean_subseq_limit_fixedPointhas no blueprint entry; none is required for a proof-internal helper.- No
\notreadytags are affected. No declarations renamed or removed.
Category B — Prose quality
No .tex files changed. No Lean docstrings, module/sectioning comments, or inline comments are added or modified. Nothing to flag.
There was a problem hiding this comment.
Review Summary
Proof-only refactor that replaces the local LinearMap.continuous_of_finiteDimensional E continuity witnesses with the bundled finite-dimensional map E' := LinearMap.toContinuousLinearMap E in two Cesàro fixed-point arguments. No mathematical statement, hypothesis, or API changes.
Verification (commit 50143f3, current HEAD)
- Build:
lake build TNLean.Channel.FixedPoint.Cesaro TNLean.Channel.Irreducible.Ergodicity→ exit 0, "Build completed successfully (8631 jobs)". The only warnings are pre-existing "Copyright too short" header-linter notes on unrelated files, not introduced by this diff. - Proof integrity: no
sorry/admit/axiom/native_decide/kernel bypasses added.
Correctness
In both theorems E : Matrix (Fin D) (Fin D) ℂ →ₗ[ℂ] Matrix (Fin D) (Fin D) ℂ is a linear endomorphism of a finite-dimensional ℂ-space, so LinearMap.toContinuousLinearMap is valid and rests on the same finite-dimensionality previously supplied by continuous_of_finiteDimensional. The coercion of E' back to a function is definitionally E, so simpa [E'] recovers the original goal shape:
IsChannel.exists_posSemidef_fixedPoint(Cesaro.lean:295-296):simpa [E'] using (E'.continuous.tendsto ρ).comp hφ_tendstore-derivesTendsto (E ∘ σ ∘ φ) atTop (nhds (E ρ)).IsChannel.cesaroMean_subseq_limit_fixedPoint(Ergodicity.lean:104-106): the addedchangetoE ∘ (fun k => cesaroMean E ρ (ψ k + 1))followed bysimpa [E']aligns the goal with(E'.continuous.tendsto σ).comp hσ_tendstoatnhds (E σ).
The downstream telescoping (cesaroMean_telescope), h_diff, and h_rhs_zero chains feeding tendsto_nhds_unique are untouched.
Category assessment
| Category | Verdict |
|---|---|
| 🔴 Proof integrity | ✅ No blockers |
| 🔴 Proof correctness | ✅ Logic unchanged; toContinuousLinearMap yields the same continuity |
| 🔴 Type safety | ✅ Domain is finite-dimensional; let E' : … →L[ℂ] … is well-typed |
| 🟡 Mathlib style | ✅ Idiomatic let/simpa/change |
| 🟡 Performance | ✅ Thin wrappers; no impact |
| 🟡 Modularity | ✅ Improvement — uses bundled Mathlib CLM API over ad hoc witnesses |
| 🟡 Documentation | ✅ N/A — proof-internal only |
| 🟡 Paper-gap notes | ✅ N/A — none changed |
Verdict: APPROVE. No 🔴 or 🟡 issues. Clean, well-scoped cleanup.
There was a problem hiding this comment.
Review: APPROVE ✅
Summary
Clean, well-scoped, proof-only refactor replacing ad hoc LinearMap.continuous_of_finiteDimensional witnesses with bundled LinearMap.toContinuousLinearMap E. No mathematical statement changes, no API changes.
Category-by-category assessment
| Category | Severity | Status |
|---|---|---|
| 1. Proof integrity | 🔴 | ✅ Pass |
| 2. Proof correctness | 🔴 | ✅ Pass |
| 3. Mathlib style | 🟡 | ✅ Pass |
| 4. Type safety | 🔴 | ✅ Pass |
| 5. Performance | 🟡 | ✅ Pass |
| 6. Modularity & duplication | 🟡 | ✅ Pass |
| 7. Documentation | 🟡 | ✅ Pass |
| 8. Paper-gap notes | 🟡 | ✅ Pass |
Details
Proof correctness: The simpa [E'] calls correctly use the @[simp] lemma coe_toContinuousLinearMap' (Mathlib Topology/Algebra/Module/FiniteDimension.lean:315) — ⇑(toContinuousLinearMap f) = f — to reduce E' applications to E applications. The telescoping and limit arguments are mathematically identical to the original proofs. The change in Ergodicity.lean is semantically redundant (E ∘ f is definitionally fun x ↦ E (f x)) but harmless.
No issues found. No 🔴 blockers, no 🟡 required changes.
There was a problem hiding this comment.
Review: refactor(Channel/FixedPoint): use CLMs in Cesaro limits
Verdict: APPROVE. No 🔴 or 🟡 issues found. This is a correct, mathematically-equivalent proof-only refactor of two lemmas.
Scope
IsChannel.exists_posSemidef_fixedPoint(TNLean/Channel/FixedPoint/Cesaro.lean)IsChannel.cesaroMean_subseq_limit_fixedPoint(TNLean/Channel/Irreducible/Ergodicity.lean)
Both replace the local continuity witness have hE_cont : Continuous E := LinearMap.continuous_of_finiteDimensional E with a bundled map E' := LinearMap.toContinuousLinearMap E, then obtain the Filter.Tendsto of E along the convergent (sub)sequence via E'.continuous.tendsto.
Correctness
- Type safety ✓ —
E : Matrix (Fin D) (Fin D) ℂ →ₗ[ℂ] Matrix (Fin D) (Fin D) ℂ(Cesaro.lean:38) is aLinearMapon a finite-dimensional ℂ-space, soLinearMap.toContinuousLinearMap Eis well-typed. - The
simpa [E']bridge is sound —LinearMap.coe_toContinuousLinearMap'(Mathlib/Topology/Algebra/Module/FiniteDimension.lean:315) is a non-deprecated@[simp]rfl-lemma stating⇑(toContinuousLinearMap f) = f, soE' ρ/E' ∘ …reduce toE ρ/E ∘ …definitionally. InErgodicity.leanthe precedingchangetoE ∘ fun k => …correctly aligns the goal beforesimpa. - The telescoping identities (
cesaroMean_telescope),h_diff, and the0-limit arguments are untouched. Mathematical statements and hypotheses are unchanged.
Proof integrity ✓
No sorry/axiom/native_decide/kernel bypass introduced; no maxHeartbeats or debug artifacts. No documentation changes needed (statements unchanged). No docs/paper-gaps/ files touched.
ℹ️ Advisory (does not block)
The PR motivation ("Mathlib 4.31 provides the finite-dimensional map … so these proof-local continuity witnesses can be removed") is slightly misleading. LinearMap.continuous_of_finiteDimensional is not deprecated — it is exactly the lemma Mathlib uses to construct toContinuousLinearMap (FiniteDimension.lean:300, toFun f := ⟨f, f.continuous_of_finiteDimensional⟩). The previous two-line form was arguably more direct and avoided the let + coercion-bridging simpa (the diff grows from 2→4 lines in Cesaro.lean and 3→6 in Ergodicity.lean). Either form is correct; this is a stylistic preference, not the removal of an obsolete API.
Note: I could not run lake build locally (project oleans not built in this environment), so correctness above is established by reading the diff against the cited Mathlib lemmas; the PR reports a successful targeted build of both files.
There was a problem hiding this comment.
Review: APPROVE ✅
Summary
Clean, minimal, proof-only refactor that replaces the local LinearMap.continuous_of_finiteDimensional E continuity witnesses with the bundled E' := LinearMap.toContinuousLinearMap E in two Cesàro fixed-point limit arguments. No mathematical statement, hypothesis, API, or blueprint changes.
Category-by-category assessment
| Category | Severity | Status |
|---|---|---|
| 1. Proof integrity | 🔴 | ✅ Pass |
| 2. Proof correctness | 🔴 | ✅ Pass |
| 3. Mathlib style | 🟡 | ✅ Pass |
| 4. Type safety | 🔴 | ✅ Pass |
| 5. Performance | 🟡 | ✅ Pass |
| 6. Modularity & duplication | 🟡 | ✅ Pass |
| 7. Documentation | 🟡 | ✅ Pass |
| 8. Paper-gap notes | 🟡 | ✅ Pass |
Details
Proof correctness: The simpa [E'] calls correctly exploit the @[simp] lemma coe_toContinuousLinearMap' (Mathlib Topology/Algebra/Module/FiniteDimension.lean) — ⇑(toContinuousLinearMap f) = f — to reduce E' applications to E applications. The change in Ergodicity.lean:104-105 is semantically neutral (E ∘ f is definitionally fun x ↦ E (f x)) and just aligns the goal shape for simpa. The downstream telescoping (cesaroMean_telescope), h_diff, and h_rhs_zero chains feeding tendsto_nhds_unique are completely untouched.
Proof integrity: No sorry, axiom, admit, native_decide, or kernel bypasses introduced. Build succeeds with 8631 jobs; the only warnings are pre-existing "Copyright too short" header-linter notes on unrelated files.
Type safety: Matrix (Fin D) (Fin D) ℂ is finite-dimensional, so LinearMap.toContinuousLinearMap is valid and rests on the same finite-dimensionality that the original continuous_of_finiteDimensional used.
No 🔴 blockers. No 🟡 required changes.
LionSR
force-pushed
the
codex/cesaro-limit-clms
branch
from
50143f3 to
47f0402
Compare
There was a problem hiding this comment.
Blueprint ↔ Lean sync and prose review — 0 equivalence mismatches, 0 stale status tags, 0 prose issues.
Category A — Blueprint ↔ Lean equivalence
No .tex blueprint files are changed. Both modified files touch only proof bodies (proof-internal have/let blocks); no theorem signature is altered.
IsChannel.exists_posSemidef_fixedPointcarries\lean{IsChannel.exists_posSemidef_fixedPoint}with\leanokon statement and proof in the blueprint. The Lean signature is unchanged and nosorryoradmitis introduced, so both tags remain valid.IsChannel.cesaroMean_subseq_limit_fixedPointhas no blueprint entry; none is required for a proof-internal helper lemma.- No
\notreadytags affected. No declarations renamed or removed.
Category B — Prose quality
No .tex files changed. No Lean docstrings, module/sectioning comments, or inline comments are added or modified. Nothing to flag.
There was a problem hiding this comment.
Review: APPROVE ✅
Clean, minimal, proof-only refactor. The local continuity witnesses LinearMap.continuous_of_finiteDimensional E in two Cesàro fixed-point limit arguments are replaced by the bundled continuous linear map E' := LinearMap.toContinuousLinearMap E. No theorem signature, hypothesis, mathematical statement, API, or blueprint entry changes.
Category-by-category assessment
| Category | Severity | Status |
|---|---|---|
| 1. Proof integrity | 🔴 | ✅ Pass |
| 2. Proof correctness | 🔴 | ✅ Pass |
| 3. Mathlib style | 🟡 | ✅ Pass |
| 4. Type safety | 🔴 | ✅ Pass |
| 5. Performance | 🟡 | ✅ Pass |
| 6. Modularity & duplication | 🟡 | ✅ Pass |
| 7. Documentation | 🟡 | ✅ Pass |
| 8. Paper-gap notes | 🟡 | ✅ Pass |
Details
Proof correctness. In IsChannel.exists_posSemidef_fixedPoint (Cesaro.lean:292–296) and IsChannel.cesaroMean_subseq_limit_fixedPoint (Ergodicity.lean:100–106), the Filter.Tendsto fact for E along the Cesàro subsequence is now obtained from E'.continuous.tendsto _ composed with the Cesàro convergence hypothesis. The simpa [E'] step is sound: it unfolds the let-bound E' and applies the @[simp] lemma LinearMap.coe_toContinuousLinearMap' (Mathlib/Topology/Algebra/Module/FiniteDimension.lean:315, ⇑(toContinuousLinearMap f) = f) to rewrite E' applications back to E. The change to E ∘ (fun k ↦ …) in Ergodicity.lean:104–105 is definitionally neutral and only aligns the goal shape for simpa. The downstream telescoping (cesaroMean_telescope), h_diff, h_rhs_zero, and tendsto_nhds_unique chains are unchanged.
Proof integrity. No sorry, axiom, admit, native_decide, or kernel bypasses; no maxHeartbeats or debug artifacts.
Type safety. Matrix (Fin D) (Fin D) ℂ is finite-dimensional, so LinearMap.toContinuousLinearMap applies on the same finite-dimensionality the original continuous_of_finiteDimensional relied on.
ℹ️ Advisory (does not block)
The PR motivation states the proof-local continuity witnesses "can be removed" because Mathlib 4.31 provides the bundled map. To be precise, LinearMap.continuous_of_finiteDimensional is not deprecated — it is exactly what toContinuousLinearMap is built from. Both forms are correct; this is a stylistic preference rather than removal of an obsolete API. Not a blocker.
No 🔴 blockers, no 🟡 required changes.
There was a problem hiding this comment.
Review: APPROVE ✅
Clean, proof-only refactor replacing ad hoc LinearMap.continuous_of_finiteDimensional witnesses with the bundled LinearMap.toContinuousLinearMap E in two Cesàro fixed-point limit arguments. No mathematical statement, hypothesis, API, or blueprint changes.
Category-by-category assessment
| Category | Severity | Status |
|---|---|---|
| 1. Proof integrity | 🔴 | ✅ Pass — no sorry/axiom/admit/native_decide/kernel bypasses |
| 2. Proof correctness | 🔴 | ✅ Pass — simpa [E'] correctly uses coe_toContinuousLinearMap' (@[simp]); limit arguments logically identical |
| 3. Mathlib style | 🟡 | ✅ Pass — idiomatic let/simpa/change |
| 4. Type safety | 🔴 | ✅ Pass — domain Matrix (Fin D) (Fin D) ℂ is finite-dimensional; toContinuousLinearMap valid |
| 5. Performance | 🟡 | ✅ Pass — trivial rewrites, no performance impact |
| 6. Modularity | 🟡 | ✅ Pass — net improvement: uses Mathlib's bundled CLM API |
| 7. Documentation | 🟡 | ✅ N/A — proof-internal change only; no new statements |
| 8. Paper-gap notes | 🟡 | ✅ N/A — no paper-gap files changed |
Verification
- Build:
lake build TNLean.Channel.FixedPoint.Cesaro TNLean.Channel.Irreducible.Ergodicity→ exit 0, 8631 jobs. Only pre-existing "Copyright too short" header-linter warnings, unrelated to this diff. rgscan: Nosorry/axiom/admit/native_decide/unsafeCastin changed files.
Correctness detail
In IsChannel.exists_posSemidef_fixedPoint (Cesaro.lean:292–296): E'.continuous.tendsto ρ yields Tendsto E' (nhds ρ) (nhds (E' ρ)); composing with hφ_tendsto gives Tendsto (E' ∘ σ ∘ φ) atTop (nhds (E' ρ)); simpa [E'] reduces E' to E via coe_toContinuousLinearMap'. Telescoping (cesaroMean_telescope), h_diff, and h_rhs_zero chains are untouched.
In IsChannel.cesaroMean_subseq_limit_fixedPoint (Ergodicity.lean:100–106): same mechanism, with a semantically neutral change to E ∘ … before simpa to align the goal shape. Downstream logic unchanged.
No 🔴 blockers. No 🟡 required changes. Approved.
2 participants
Motivation
The Cesaro fixed-point arguments transported convergence through a channel by first proving continuity from finite dimensionality. Mathlib 4.31 provides the finite-dimensional map from linear maps to continuous linear maps, so these proof-local continuity witnesses can be removed.
Description
This PR replaces the local
LinearMap.continuous_of_finiteDimensionalcontinuity facts inIsChannel.exists_posSemidef_fixedPointandIsChannel.cesaroMean_subseq_limit_fixedPointwith bundled mapsLinearMap.toContinuousLinearMap E. The mathematical statements and telescoping arguments are unchanged.Files modified:
TNLean/Channel/FixedPoint/Cesaro.leanTNLean/Channel/Irreducible/Ergodicity.leanTesting
lake exe cache getlake build TNLean.Channel.FixedPoint.Cesaro TNLean.Channel.Irreducible.Ergodicity -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 in channel fixed-point/ergodicity lemmas; no API, runtime, or mathematical statement changes.
Overview
Cesàro fixed-point proofs now push convergence through
LinearMap.toContinuousLinearMap Einstead of ad hocLinearMap.continuous_of_finiteDimensionalwitnesses.In
IsChannel.exists_posSemidef_fixedPoint(Cesaro.lean) andIsChannel.cesaroMean_subseq_limit_fixedPoint(Ergodicity.lean), the local continuity fact is replaced by a bundled continuous linear mapE', andFilter.TendstoforEalong Cesàro subsequences is obtained viaE'.continuous.tendsto. The ergodicity lemma additionally rewrites the goal asE ∘ …beforesimpa. Telescoping identities and limit arguments are unchanged.Reviewed by Cursor Bugbot for commit 90bed29. Bugbot is set up for automated code reviews on this repo. Configure here.
Note
Low Risk
Proof-only refactor in channel fixed-point lemmas; no API or statement changes.
Overview
Cesàro fixed-point proofs now route
Filter.Tendstofor channel iterates through a bundledLinearMap.toContinuousLinearMap E(E') instead of a localLinearMap.continuous_of_finiteDimensionalwitness.In
IsChannel.exists_posSemidef_fixedPoint(Cesaro.lean) andIsChannel.cesaroMean_subseq_limit_fixedPoint(Ergodicity.lean), continuity is obtained viaE'.continuous.tendsto, withsimpa [E']to alignEwith the CLM. The ergodicity lemma adds achangetoE ∘ …before that step. Telescoping and limit arguments are unchanged.Reviewed by Cursor Bugbot for commit 47f0402. Bugbot is set up for automated code reviews on this repo. Configure here.