refactor(Channel/Determinant): use Fintype sum zero criterion#3276
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 status (Category A): No .tex files changed. The only modified declaration, eq_zero_of_nonneg_of_sum_le_zero, has its proof body simplified but its statement is unchanged, so no \lean{...}, \leanok, or \uses{...} tags are affected. Nothing to flag.
Prose quality (Category B): No blueprint prose, docstrings, or comments were modified. Nothing to flag.
0 equivalence mismatches, 0 stale status tags, 0 prose issues.
claude
Bot
added
formalization
|
PR cleanup
Conventions: CONTRIBUTING.md |
There was a problem hiding this comment.
Review: refactor(Channel/Determinant): use Fintype sum zero criterion
Verdict: APPROVE. No 🔴 or 🟡 issues found.
What was checked
This PR rewrites the proof of eq_zero_of_nonneg_of_sum_le_zero in TNLean/Channel/Determinant/HilbertSchmidt.lean, swapping the Finset.sum_nonneg / Finset.sum_eq_zero_iff_of_nonneg (+ explicit Finset.mem_univ) steps for the Fintype-namespaced Fintype.sum_nonneg and Fintype.sum_eq_zero_iff_of_nonneg.
- Proof integrity 🔴: No
sorry/admit/axiom/native_decide/unsafeCastintroduced; file scans clean. - Proof correctness 🔴: The new proof is sound.
Fintype.sum_nonnegis theto_additiveofFintype.one_le_prod(Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:612), whose hypothesis0 ≤ fin the Pi order is definitionally∀ i, 0 ≤ f i, soFintype.sum_nonneg hftypechecks againsthf : ∀ i, 0 ≤ f i.Fintype.sum_eq_zero_iff_of_nonneg(to_additiveofprod_eq_one_iff_of_one_le, line 618) yields∑ i, f i = 0 ↔ f = 0with function equality on the right, socongrFun (… .mp hsum_zero) i : f i = (0 : ι → ℝ) i, defeq to the goalf i = 0. Thele_antisymm hsum (Fintype.sum_nonneg hf)step is correct. - Statement faithfulness: The public signature (
{ι} [Fintype ι] (f) (hf) (hsum) : ∀ i, f i = 0) and docstring are unchanged; the sole callereq_zero_of_nonneg_of_sum_le_zero _ hgap_trace_nonneg hgap_trace_sum_le(HeisenbergDual.lean:180) still matches positionally. No hypotheses added or removed. - Type safety 🔴 / Performance 🟡 / Modularity 🟡 / Documentation 🟡: No concerns. The change reduces five proof lines to two and removes the
Finset.mem_univplumbing, which is exactly the intended simplification given theFintypehypothesis.
ℹ️ Advisory (non-blocking)
The closing term exact fun i => congrFun ((Fintype.sum_eq_zero_iff_of_nonneg hf).mp hsum_zero) i is eta-expanded; exact congrFun ((Fintype.sum_eq_zero_iff_of_nonneg hf).mp hsum_zero) would suffice against the ∀ i, f i = 0 goal. Purely cosmetic — acceptable as written.
There was a problem hiding this comment.
Review Summary — APPROVE
This is a clean proof refactor of eq_zero_of_nonneg_of_sum_le_zero replacing Finset-scoped lemmas (Finset.sum_nonneg, Finset.sum_eq_zero_iff_of_nonneg) with the corresponding Fintype-scoped lemmas (Fintype.sum_nonneg, Fintype.sum_eq_zero_iff_of_nonneg). The lemma statement and all callers are unchanged.
Assessment by category
| Category | Result |
|---|---|
| 🔴 Proof integrity | ✅ No issues — no sorry/admit/axiom introduced; build passes |
| 🔴 Proof correctness | ✅ Sound — le_antisymm hsum (Fintype.sum_nonneg hf) yields ∑ f = 0, then Fintype.sum_eq_zero_iff_of_nonneg + congrFun gives each f i = 0 |
| 🟡 Mathlib style | ✅ IdIomatic — Fintype lemmas are the natural choice given the [Fintype ι] hypothesis; proof is shorter and eliminates Finset.mem_univ boilerplate |
| 🔴 Type safety | ✅ No issues — congrFun is correctly applied to the function-equality result of Fintype.sum_eq_zero_iff_of_nonneg |
| 🟡 Performance | ✅ Trivial two-step proof, no timeout risk |
| 🟡 Modularity | ✅ No duplication; leverages existing Mathlib Fintype API |
| 🟡 Documentation | ✅ Existing docstring preserved; no new definitions |
| 🟡 Paper-gap notes | ✅ N/A — no paper-gap files changed |
Caller check
The sole caller at TNLean/Channel/Determinant/HeisenbergDual.lean:180 uses eq_zero_of_nonneg_of_sum_le_zero _ hgap_trace_nonneg hgap_trace_sum_le expecting ∀ ij, … = 0. The statement is unchanged, so the caller is unaffected.
No issues found. This is ready to merge.
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
There was a problem hiding this comment.
Category A — Blueprint ↔ Lean equivalence and status: No .tex files changed. The sole modified declaration, eq_zero_of_nonneg_of_sum_le_zero, has only its proof body rewritten; the public signature is unchanged. No \lean{...}, \leanok, or \uses{...} tags are affected. Nothing to flag.
Category B — Prose quality: No blueprint prose, Lean docstrings, or comments were modified. Nothing to flag.
0 equivalence mismatches, 0 stale status tags, 0 prose issues.
There was a problem hiding this comment.
Review: APPROVE
Scope. A 2-line proof refactor of eq_zero_of_nonneg_of_sum_le_zero in TNLean/Channel/Determinant/HilbertSchmidt.lean, swapping the Finset.sum_nonneg / Finset.sum_eq_zero_iff_of_nonneg steps (which threaded explicit Finset.mem_univ membership) for the Fintype.* variants that match the [Fintype ι] hypothesis directly. Statement and callers (HeisenbergDual.lean) unchanged.
1. Proof integrity 🔴 — pass
No sorry/admit/axiom/native_decide/unsafeCast in the file. Verified the file builds: lake build TNLean.Channel.Determinant.HilbertSchmidt → 8651 jobs, exit 0.
2. Proof correctness 🔴 — pass
The new proof is well-structured and the logic is sound:
Fintype.sum_nonneg hf : 0 ≤ ∑ i, f itogether withhsum : ∑ i, f i ≤ 0giveshsum_zero : ∑ i, f i = 0viale_antisymm.(Fintype.sum_eq_zero_iff_of_nonneg hf).mp hsum_zero : f = 0, andcongrFun … i : f i = 0discharges the∀ i, f i = 0goal.
Both Fintype.sum_nonneg and Fintype.sum_eq_zero_iff_of_nonneg are genuine Mathlib lemmas (e.g. used in Mathlib/LinearAlgebra/Matrix/DotProduct.lean, Mathlib/LinearAlgebra/Matrix/PosDef.lean), and both take the membership-free ∀ i, 0 ≤ f i hypothesis, so the refactor is a faithful simplification — strictly fewer steps, identical content. This is exactly the kind of Mathlib reuse the contributing guide asks for.
3–7. Style / type safety / performance / modularity / documentation 🟡 — pass
- Naming and tactic style follow Mathlib conventions; the docstring is retained and explains the mathematical meaning.
- No type-safety, coercion, or universe concerns (the lemma is polymorphic over a
Fintype ι, unchanged). - No performance impact; the proof is shorter and term-mode.
- No duplication introduced; this removes locally-reproved bookkeeping in favor of library lemmas.
8. Paper-gap notes — N/A
No files under docs/paper-gaps/ touched.
ℹ️ Advisory (non-blocking): exact fun i => congrFun ((Fintype.sum_eq_zero_iff_of_nonneg hf).mp hsum_zero) i can be eta-reduced to exact congrFun ((Fintype.sum_eq_zero_iff_of_nonneg hf).mp hsum_zero), since congrFun already yields ∀ i, f i = 0 (with (0 : ι → ℝ) i defeq 0). Purely cosmetic; the current form is perfectly fine.
No 🔴 or 🟡 issues found. Approving.
2 participants
Motivation
The determinant-saturation auxiliary lemma
eq_zero_of_nonneg_of_sum_le_zerowas still written through theFinsetform of the finite-sum nonnegativity and zero-sum criteria. The statement is over an arbitraryFintype, so the correspondingFintypelemmas state the same argument more directly.Description
Finset.sum_nonnegandFinset.sum_eq_zero_iff_of_nonnegsteps withFintype.sum_nonnegandFintype.sum_eq_zero_iff_of_nonneg.Testing
lake exe cache getlake build TNLean.Channel.Determinant.HilbertSchmidt -qgit diff --checkrg -n "sorry|admit|axiom|native_decide|unsafeCast" TNLean/Channel/Determinant/HilbertSchmidt.lean || truepython3 scripts/check_reader_facing_prose.py --root . --diff-base origin/mainpython3 scripts/blueprint_lean_sync.py --root . --ciAddresses #22
Note
Low Risk
Proof refactor only; no API or behavioral change to the lemma or its callers.
Overview
Refactors the proof of
eq_zero_of_nonneg_of_sum_le_zeroinHilbertSchmidt.leanso the argument usesFintype.sum_nonnegandFintype.sum_eq_zero_iff_of_nonneginstead of theFinsetversions (Finset.sum_nonneg,Finset.sum_eq_zero_iff_of_nonneg, and explicitFinset.mem_univ).The lemma's statement and its use in
HeisenbergDual.leanare unchanged; only the internal proof steps are shortened and aligned with the[Fintype ι]hypothesis.Reviewed by Cursor Bugbot for commit 9ad8919. Bugbot is set up for automated code reviews on this repo. Configure here.