refactor(algebra): use Fintype sum zero criterion#3281
Conversation
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
![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 tags · 0 prose issues
Category A — Blueprint ↔ Lean equivalence
No blueprint .tex files are changed. All seven modified files touch only internal proof tactic bodies (private lemmas); no public declaration signatures change. No \lean{...}, \leanok, or \notready tags are added or removed. There is nothing to check for blueprint/Lean synchronization drift.
Category B — Prose quality
No docstrings (/-- … -/), module docs (/-! … -/), block comments, line comments, or section/namespace names appear in the diff. The changed lines are exclusively proof-term rewrites inside tactic blocks and are out of scope for prose review.
|
PR cleanup
Note: The branch name suffix Conventions: CONTRIBUTING.md |
There was a problem hiding this comment.
Review: refactor(algebra): use Fintype sum zero criterion
Verdict: APPROVE. No 🔴 or 🟡 issues found.
This is a faithful mechanical refactor: in seven modules it replaces the proof-local idiom
Finset.sum_eq_zero_iff_of_nonneg (fun j _ => h j) |>.mp hsum i (Finset.mem_univ i) with
congrFun (Fintype.sum_eq_zero_iff_of_nonneg (fun j => h j) |>.mp hsum) i.
Correctness. I confirmed the Mathlib signature is
Fintype.sum_eq_zero_iff_of_nonneg : 0 ≤ f → (∑ i, f i = 0 ↔ f = 0). The nonnegativity
premise 0 ≤ f is the Pi order ∀ j, 0 ≤ f j, supplied correctly by fun j => h j; the
.mp yields the function equality f = 0, and congrFun … i extracts f i = 0 — exactly
the per-index fact the old Finset form produced via Finset.mem_univ. The two phrasings are
definitionally equivalent here, so no mathematical statement, hypothesis, or conclusion changes.
The LiouvillianKernel.lean site correctly adapts (le_of_eq <| congrFun … feeding the
le_antisymm).
Scope check. The claim that proper-subset sums are intentionally left on the Finset lemma
holds: RankOne.lean:114 keeps Finset.sum_eq_zero_iff_of_nonneg over Finset.univ.erase i,
where the whole-Fintype lemma does not apply. This is the right boundary.
Verification. Built TNLean.Algebra.MatrixAux and TNLean.QPF.PosDef locally — both
succeed (exit 0; the only warnings are pre-existing copyright/header-linter notices unrelated to
this diff).
- Proof integrity: clean — no
sorry/axiom/native_decide/kernel bypasses introduced. - Mathlib style: improves library integration (uses the dedicated
Fintypeentry point); lines
within 100 cols. - Type safety / performance / docs: unaffected (no signatures or statements touched).
No changes requested.
There was a problem hiding this comment.
Review: APPROVE ✅
This is a clean, mechanical proof-internal refactor. No issues found in any review category.
Summary of changes
The PR replaces Finset.sum_eq_zero_iff_of_nonneg + Finset.mem_univ with Fintype.sum_eq_zero_iff_of_nonneg + congrFun in seven modules. This is the Mathlib-idiomatic pattern for whole-type sums: Fintype lemmas are designed for sums over the entire finite type, while Finset lemmas handle arbitrary subsets.
Per-category assessment
| Category | Severity | Status |
|---|---|---|
| 🔴 Proof integrity | Blocker | ✅ Pass — no sorry, admit, axiom, native_decide, or unsafeCast in diff |
| 🔴 Proof correctness | Blocker | ✅ Pass — Fintype.sum_eq_zero_iff_of_nonneg returns (∑ f = 0) ↔ (f = 0) (function equality), and congrFun extracts the per-element equality. Mathematically equivalent to the old formulation. |
| 🟡 Mathlib style | Requires changes | ✅ Pass — using Fintype variant for whole-type sums is preferred Mathlib style |
| 🔴 Type safety | Blocker | ✅ Pass — no new type-level changes |
| 🟡 Performance | Requires changes | ✅ Pass — individual file builds complete in seconds; full build in progress |
| 🟡 Modularity | Requires changes | ✅ Pass — Fintype lemma is the more general, appropriate entry point |
| 🟡 Documentation | Requires changes | ✅ Pass — no new definitions or theorems requiring docstrings |
| 🟡 Paper-gap notes | Requires changes | ✅ N/A — no paper-gap file changes |
Verification
lake buildon all seven changed modules: all pass- Diff scan for
sorry/admit/axiom/native_decide/unsafeCast: clean - Proper-subset sums (e.g.,
Finset.univ.erase iinRankOne.lean) correctly left onFinsetlemma
🤖 Generated with Claude Code
2 participants
Motivation
Fintype.sum_eq_zero_iff_of_nonnegas a ready-made theorem for the case where the index set is the whole finite type; the manual specialisationFinset.sum_eq_zero_iff_of_nonneg ... Finset.univin proof scripts is replaced to align with Mathlib idioms and reduce internal boilerplate.Description
Finset.sum_eq_zero_iff_of_nonnegspecialised toFinset.univare replaced byFintype.sum_eq_zero_iff_of_nonneg.TNLean/Algebra/MatrixAux.lean,TNLean/Algebra/PerronFrobenius/RankOne.lean,TNLean/Channel/FixedPoint/Cesaro.lean,TNLean/Channel/Irreducible/Growth/OneStep.lean,TNLean/Channel/Semigroup/LiouvillianKernel.lean,TNLean/MPS/Irreducible/FixedPointProjection.lean,TNLean/QPF/PosDef.lean.Finset.univ.erase iinRankOne.lean) retain theFinsetvariant.Testing
lake exe cache getlake build TNLean.Algebra.MatrixAux TNLean.Algebra.PerronFrobenius.RankOne TNLean.Channel.FixedPoint.Cesaro TNLean.Channel.Irreducible.Growth.OneStep TNLean.QPF.PosDef TNLean.Channel.Semigroup.LiouvillianKernel TNLean.MPS.Irreducible.FixedPointProjection -q --log-level=infogit diff --check; added-line scan forsorry,admit,axiom,native_decide,unsafeCast.python3 scripts/check_reader_facing_prose.py --root . --diff-base origin/mainpython3 scripts/blueprint_lean_sync.py --root . --ciNote
Low Risk
Mechanical proof refactor with no API or mathematical changes; only affects internal proof scripts in algebra/channel/MPS/QPF files.
Overview
Proofs that deduce each summand is zero from a sum of nonnegative terms equals zero now call Mathlib's
Fintype.sum_eq_zero_iff_of_nonnegwithcongrFun, instead of manually instantiatingFinset.sum_eq_zero_iff_of_nonnegonFinset.univwithFinset.mem_univ.The pattern is updated in seven modules (matrix sums, Perron–Frobenius rank-one, Cesàro fixed points, irreducible growth, Liouvillian kernel, MPS fixed-point projection, QPF positive definiteness). Sums over proper subsets (e.g.
Finset.univ.erase iinRankOne.lean) still use theFinsetlemma.No theorem statements, names, or proof conclusions change—only the Mathlib entry point for whole-
Fintypesums.Reviewed by Cursor Bugbot for commit 5fd6d0e. Bugbot is set up for automated code reviews on this repo. Configure here.