Zcap
plain-language theorem explainer
Defines the panel-locked exact-shell complexity cutoff: the complex sum of unregulated phased amplitudes over all exact quotient shells with index strictly below B. Gravity and continuum-gap authors cite it as the finite partial sum whose Cauchy property is equivalent to uniform late-shell cancellation. The body is a one-line Finset sum of shell amplitudes.
Claim. Given a phase assignment $\mathrm{phase}_n$ on exact path classes of complexity $n$, and a natural number $B$, the cutoff sum is $Z_{\mathrm{cap}}(\mathrm{phase},B)=\sum_{n=0}^{B-1} A_n(\mathrm{phase})$, where $A_n$ is the unregulated phased amplitude of the exact complexity-$n$ shell. Shells included have complexities strictly below $B$; this is a complexity cutoff, not mesh refinement.
background
Module P2-a isolates analytic obligations for removing the complexity cutoff from the phased quotient path sum. The fixed-cap API yields a sequence of finite quotient sums; completeness of $\mathbb{C}$ makes existence of a limit equivalent to the Cauchy criterion. The cap-free exact-shell API replaces that with a panel-locked form.
An exact path class at complexity $n$ is a nonduplicating quotient shell. The unregulated phased shell amplitude $A_n(\mathrm{phase})$ sums, over classes $c$ at level $n$, the complex weight $\mu(c),e^{i,\mathrm{phase}_n(c)}$. The cutoff object stacks those shells for $n\in{0,\ldots,B-1}$.
Local convention: all limits here remove a complexity cutoff. They make no claim about mesh refinement, continuum geometry, rates, derived measures, or the full-theory ledger. A remaining bridge equates capped triangulation sums with exact-shell sums at each cap.
proof idea
Definitional one-liner: expand as the Finset sum of exactShellAmplitude phase n over n in Finset.range B. No lemmas, tactics, or algebraic rewriting; the meaning is entirely the sum of those shell amplitudes.
why it matters
This is the binding finite object for the C1 continuum-cutoff blocker. Downstream, Cauchy-ness of the sequence $B\mapsto Z_{\mathrm{cap}}(\mathrm{phase},B)$ is proved equivalent to the oscillatory-tail predicate (every sufficiently late contiguous block of shell amplitudes uniformly small). That IFF feeds the residual DAG entry equating cap-free Cauchy with oscillatory tail, the composition package identifying ordered exact cutoffs with a successor evaluation of this sum, and the FullTheoryLedger pillar certifying the gap-2 cutoff-limit blocker.
In the Seven Gaps gravity program it is the exact partial sum a substrate-derived phase must make Cauchy. Zero phase fails the tail condition, so the criterion is discriminating. It does not itself close continuum geometry or measure; it only packages the complexity-cutoff half of gap 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.