sum_fin_eq_sum_range
plain-language theorem explainer
Finite sums indexed by `Fin N` equal the same sums over the natural range `{0,...,N-1}`. Anyone reindexing a shell or cutoff sum from a finite-type carrier onto `Finset.range` cites this. The proof is a short induction on `N`, peeling the last term with the standard `Fin` and range successor lemmas.
Claim. Let $\alpha$ be an additive commutative monoid, $f:\mathbb{N}\to\alpha$, and $N\in\mathbb{N}$. Then $\sum_{i:\mathrm{Fin}\,N} f(i) = \sum_{i\in\{0,\ldots,N-1\}} f(i)$.
background
The ambient module builds the carrier bridge behind CapShellCompatibility: at a complexity cap $B$, bounded complexes and exact-shell complexes (shell index $n\le B$) are identified up to incidence data and relabeling, so their quotient carriers match and $1/|\mathrm{Aut}|$ class measures agree. Reindexing finite quotient sums along that equivalence is what eventually equates a sum over the disjoint-union shell carrier with the exact complexity cutoff through $B$ (range $B+1$, shell $B$ included).
This lemma is pure finite-sum bookkeeping. Fin N is the type of naturals strictly below $N$; Finset.range N is the set ${0,\ldots,N-1}$. Both index the same $N$ terms of an $\alpha$-valued sequence when $\alpha$ is only an additive commutative monoid (no ring or topology required). No gravity, continuum, or phase hypothesis enters.
proof idea
Induct on $N$. The zero case is immediate by simplification of empty sums. In the successor step, rewrite the left-hand side via Fin.sum_univ_castSucc as the sum over Fin N plus the value at $N$; apply the inductive hypothesis; then fold the last term back with Finset.sum_range_succ. The calculation is a three-line calc chain.
why it matters
Parent use is sum_shellsUpTo_eq_exactComplexityCutoff: after the capped-to-exact shell carrier equivalence is in hand, the finite sum over ShellsUpTo B must be rewritten as the exact complexity cutoff sum whose shell range is $B+1$. That reindexing step needs Fin-indexed sums to match range-indexed sums; this lemma supplies the equality with no extra hypotheses.
In the Seven Gaps / P2.3 story it is scaffolding glue, not a physical claim: it lets the bridge preserve the discrete class measure and transport an arbitrary exact-shell phase to a PhaseModel at every cap. It does not touch the forcing chain (T0–T8), RCL, or continuum limits; it only clears the finite-sum notation mismatch so the cutoff identity can close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.