at
plain-language theorem explainer
Flags that the phase-structure results for the quotient-first path sum Z_q hold only at a fixed complexity shell B, not in any continuum limit. Gravity workers on Seven Gaps lane D3 cite it to keep finite-cap bounds separate from open continuum questions. The declaration is essentially a scope marker tied to the shell coordinate complexity; no continuum argument is supplied.
Claim. All phase-structure statements for the quotient-first sum $Z_q$ in this module are theorems at a fixed complexity cap $B\in\mathbb{N}$ (shell coordinate $\mathrm{complexity}(K)=\max(n_V,n_E,n_T)$). They are not continuum-limit statements.
background
Lane D3 of Seven Gaps works on the quotient-first object $Z_q$ (from QuotientFirstZ): a finite sum over triangulation classes of bounded complexes at complexity cap $B$. Complexity is the shell coordinate, the max of vertex, edge, and tetrahedron counts on a bounded complex.
This module equips that sum with an explicit oscillatory phase model: a real phase on labeled configurations, relabeling-invariant so it descends to triangulation classes, with phased weight $e^{i\theta}$ of unit modulus. Boundedness at fixed $B$ gives $|Z_q|\le\mathrm{totalClassMass}(B)\le|\mathrm{TriangulationClass}(B)|$.
The module status line is explicit: structure theorems at fixed complexity cap; the continuum limit stays open. Measure-invariance no-go material is imported alongside the quotient-first setup, so finite-cap arithmetic is the intended regime.
proof idea
No proof body is attached in the extract (zero body lines; status other). The declaration depends only on the shell coordinate complexity from ExactShellGaugeUV, i.e. $\max(n_V,n_E,n_T)$ on a bounded complex. Treat it as a scope annotation that every phased $Z_q$ identity in the module is finite-sum arithmetic at fixed $B$, not a limiting argument. Upstream complexity is a plain definition, not a lemma chain.
why it matters
Keeps the Seven Gaps gravity ledger honest: phased well-definedness, norm bounds versus total class mass, and conditional pairing cancellation (exact opposite summands under a stated injection) are all finite-cap facts. Downstream use list is empty here; the parent narrative is the module itself (boundedness, pairing decomposition, and the $B=2$ non-vacuity witness that beats the triangle inequality).
Framework role is local to the gravity path-sum side, not a T0–T8 forcing step. It prevents reading fixed-$B$ modulus improvements as continuum cancellation. The continuum limit for $Z_q$ remains the open question the module status flags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.