sum_shellsUpTo_eq_exactComplexityCutoff
plain-language theorem explainer
The phased sum of class measures over the disjoint union of exact path classes in shells 0 through B equals the exact-shell complexity cutoff at B. Seven-Gaps gravity authors cite this when transporting capped quotient sums onto shell cutoffs. The proof splits the sigma-type sum and reindexes Fin(B+1) to Finset.range(B+1).
Claim. For any real phase assignment on exact path classes and any $B \in \mathbb{N}$, $$\sum_{n=0}^{B}\sum_{[c]\,:\,\mathrm{ExactPathClass}\,n} \mu([c])\,e^{i\,\mathrm{phase}_n([c])} = \mathrm{exactComplexityCutoff}(\mathrm{phase},B).$$ The outer range is $B+1$, so shell $B$ is included.
background
Module P2.3 builds the carrier bridge behind CapShellCompatibility: at cap $B$, bounded complexes correspond bijectively (on quotients) to exact complexes in shells $n \le B$, preserving incidence, relabeling witnesses, and automorphism cardinality, hence the class measure $1/|\mathrm{Aut}|$.
ShellsUpTo B is the sigma type $\Sigma n : \mathrm{Fin}(B+1),,\mathrm{ExactPathClass},n$, the off-by-one-safe carrier for shells $0,\ldots,B$. The summand multiplies the complexified class measure by a pure phase $e^{i\theta}$ drawn from an arbitrary exact-shell phase family.
No continuum limit, substrate phase, or physical interpretation is assumed; the equality is purely finite reindexing of the exact-shell cutoff whose shell range is $B+1$.
proof idea
Term-mode, three steps. First Fintype.sum_sigma splits the sum over the sigma carrier into an outer sum on Fin(B+1) of per-shell amplitudes. A change identifies that outer sum with $\sum_{n:\mathrm{Fin}(B+1)}\mathrm{exactShellAmplitude},\mathrm{phase},n$. The local lemma sum_fin_eq_sum_range then converts the Fin sum into a Finset.range(B+1) sum, which is the definition of the exact complexity cutoff. No measure or phase identities are needed beyond the carrier split.
why it matters
Immediate parent is the headline finite-sum reindexing phasedZq_eq_exactComplexityCutoff: the phased capped quotient sum transported from any exact-shell phase equals its exact-shell cutoff through shell $B$. That equality is the last arithmetic step of the CapShellBridge, discharging the carrier half of CapShellCompatibility in the Seven Gaps Zq continuum blocker.
Within Recognition gravity, the bridge lets capped quotient sums (the Zq side) speak the same language as exact-shell cutoffs without assuming convergence or a physical continuum. It sits downstream of the eight-tick and forcing-chain scaffolding only as ambient imports; the content here is pure finite reindexing of class-measure sums.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.