refactor(Algebra): use native Fin.castLE order isomorphism

[LionSR]

Motivation

• sum_castLE_extend_zero previously reindexed finite sums via Fin.castLEquiv from Mathlib.Logic.Equiv.Fin.Basic; the native Fin.castLEOrderIso from Mathlib.Order.Fin.Tuple is the canonical order-isomorphism for this purpose and is more idiomatic.
• The subtype-to-filter and filter-to-universe sum comparison steps used explicit transitivity chains; direct rw calls shorten the proof without altering the result.

Description

• TNLean/Algebra/FinSum.lean: replaces the finite-index equivalence in sum_castLE_extend_zero with (Fin.castLEOrderIso h).toEquiv, importing from Mathlib.Order.Fin.Tuple instead of Mathlib.Logic.Equiv.Fin.Basic. Shortens the subtype-sum and filtered-sum comparison steps to direct rw calls on Finset.sum_subtype_eq_sum_filter and Finset.sum_filter, replacing explicit Finset.sum_congr transitivity chains. The theorem statement and all call sites are unchanged.

Testing

• lake env lean TNLean/Algebra/FinSum.lean
• git diff --check
• Relies on Lean CI (lean_action_ci.yml) to validate the full build.

---

Note

Low Risk
Only the Lean proof and imports in FinSum.lean change; the theorem statement and call sites are unchanged.

Overview
Refactors the proof of sum_castLE_extend_zero without changing its statement or downstream uses (e.g. Kraus padding arguments).

The first step now reindexes via Fin.castLEOrderIso h).toEquiv instead of Fin.castLEquiv, with Mathlib.Order.Fin.Tuple replacing Mathlib.Logic.Equiv.Fin.Basic. The subtype-to-filter and filter-to-universe sum steps are shortened to direct rw calls on Finset.sum_subtype_eq_sum_filter and Finset.sum_filter, with smaller Finset.sum_congr blocks instead of explicit transitivity chains.

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

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

[claude]

Blueprint ↔ Lean equivalence and status (Category A): No blueprint .tex files are changed. sum_castLE_extend_zero has no blueprint entry, so there are no \lean{...} tags, \leanok markers, or \notready tags to verify. The theorem statement is unchanged by this PR — only the proof body is refactored. Nothing to flag.

Prose quality (Category B): The diff contains no new or modified docstrings, block comments, line comments, or section/namespace names. Nothing to flag.

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

[claude]

PR cleanup

Field	Before	After
Title	refactor(Algebra): use native Fin.castLE order isomorphism	unchanged
Body	Summary: / Tests: headings (non-standard)	restructured to ### Motivation / ### Description / ### Testing template; Cursor Bugbot block preserved
Labels	(none)	added: cleanup
Issue	no issue found — branch codex/finsum-native-castle contains no issue-N pattern; PR body and commits contain no #N reference; open issues contain no mention of FinSum.lean or sum_castLE_extend_zero — please link an issue manually if one exists

Conventions: CONTRIBUTING.md

[claude]

Review: refactor(Algebra): use native Fin.castLE order isomorphism

Verdict: APPROVE — no blocker (🔴) or requires-changes (🟡) issues found.

Scope

The PR refactors the proof of Fin.sum_castLE_extend_zero in TNLean/Algebra/FinSum.lean. The theorem statement, its docstring, and all downstream call sites are unchanged; only the proof body and one import are touched.

Verification

• Builds clean. lake env lean TNLean/Algebra/FinSum.lean exits 0 with no errors, warnings, or sorry/axiom.
• Proof integrity (🔴): No sorry, admit, native_decide, axiom, or kernel bypass. Clean.
• Proof correctness (🔴): The first calc step now reindexes via (Fin.castLEOrderIso h).toEquiv rather than the removed-path Fin.castLEquiv. Fin.castLEOrderIso h : Fin r ≃o { i : Fin s // (i:ℕ) < r } (Mathlib/Order/Fin/Tuple.lean:185) sends j ↦ ⟨Fin.castLE h j, _⟩, whose underlying value is j.val, so the Fintype.sum_equiv obligation f j = f ⟨(castLE h j).val, _⟩ is discharged by simp — faithful to the original reindexing. The subtype→filter and filter→universe steps are now single rws on Finset.sum_subtype_eq_sum_filter and Finset.sum_filter plus small sum_congr blocks, mathematically equivalent to the prior explicit trans chains and a net reduction of 23 lines.
• Mathlib style (🟡): Idiomatic — uses the canonical order-isomorphism instead of the more general Equiv, and the import is correctly narrowed to Mathlib.Order.Fin.Tuple. No issues blocking approval.
• Type safety (🔴): .toEquiv on the OrderIso yields the right Fin r ≃ {i : Fin s // …} subtype; classical supplies decidability for the if hlt : branches. No coercion or universe concerns.
• Performance / Modularity / Documentation: Unaffected — small finite sums, no new lemmas, docstring retained.

Advisory (ℹ️, non-blocking)

• Lines 40–44: refine Finset.sum_congr ?_ ?_ focuses the first goal with a · bullet but lets the second fall through unbulleted. This is accepted Mathlib practice for a trailing main goal; bulleting both would be marginally more uniform. Not required.

Nice cleanup — shorter and more idiomatic with no change to the statement or its consumers.

[claude]

Review Summary

This is a clean proof refactoring of sum_castLE_extend_zero in TNLean/Algebra/FinSum.lean. The PR replaces Fin.castLEquiv with the canonical (Fin.castLEOrderIso h).toEquiv and simplifies the proof by using direct rw calls instead of explicit transitivity chains.

All categories pass with no issues found:

• Proof integrity — no sorry, axiom, native_decide, or other blockers.
• Proof correctness — both Fin.castLEquiv and Fin.castLEOrderIso have identical toFun/invFun definitions (both use Fin.castLE with by simp), so the mathematical equivalence is preserved. The simp/rw steps are all sound, and the file compiles cleanly with lake env lean.
• Mathlib style — Mathlib.Order.Fin.Tuple is the canonical module for Fin order isomorphisms; the old import was from the less idiomatic Mathlib.Logic.Equiv.Fin.Basic. Indentation and proof structure follow Mathlib conventions.
• Type safety — no issues.
• Performance — the proof is cleaner and shorter (40 lines removed, 17 added).
• Modularity — no duplication; using the canonical module.
• Documentation — existing docstrings suffice; no new definitions.
• Paper-gap notes — not applicable.

No inline comments needed. ✅ Approved.