totalClassMass
plain-language theorem explainer
Defines the total per-class mass at complexity cap B as the sum of configuration masses over all triangulation classes. It is the quotient-side triangle bound for unit-modulus phased path sums: any phased Zq has modulus at most this quantity. Downstream boundedness, pairing, and B=2 witness theorems cite it as the baseline before cancellation improves the estimate.
Claim. For each complexity cap $B \in \mathbb{N}$, the total class mass is the real number $\sum_{q} \mu(\mathrm{out}(q))$, summed over all triangulation classes $q$ at cap $B$, where $\mathrm{out}(q)$ is a labeled representative of the class and $\mu$ is the per-configuration mass (positive and at most one).
background
Lane D3 of the Seven Gaps program studies phase structure on the quotient-first path sum $Z_q$. Configurations of complexity at most $B$ are quotiented by relabeling to triangulation classes; each class contributes a mass $\mu$ of a chosen labeled representative. The module equips this quotient with an explicit oscillatory phase model: a real phase on labeled configurations that is relabeling-invariant, hence descends to classes, and yields unit-modulus phased weights $\mathrm{e}^{i\theta}$.
Under unit-modulus weights the triangle inequality bounds $|Z_q|$ by the sum of the absolute summands. That sum is exactly the total class mass defined here. Sibling facts record that each $\mu$ is strictly positive and at most one, so the total is positive (the empty-complex class is always present) and at most the class cardinality.
proof idea
Pure definition: unfold to a finite sum over the fintype of triangulation classes at cap $B$, evaluating $\mu$ on Quotient.out of each class. No proof obligations beyond the ambient noncomputable real arithmetic and the existence of representatives.
why it matters
This scalar is the baseline triangle bound in the module's structure theorems. Boundedness and well-definedness of phased $Z_q$ at fixed cap are stated as $|Z_q| \le \mathrm{totalClassMass}, B \le #(\mathrm{TriangulationClass}, B)$. Conditional pairing theorems improve the bound to total class mass minus paired mass whenever an exact-opposite pairing hypothesis holds, and the $B=2$ witness chain discharges that hypothesis on an explicit phase model (phase $0$ on the empty class, $\pi$ elsewhere), giving $|Z_q| \le \mathrm{totalClassMass}, 2 - 2 < \mathrm{totalClassMass}, 2$ with the improved remainder nonnegative.
It therefore separates the purely arithmetic content of cancellation (finite-sum opposite pairs) from the continuum limit, which the module leaves open. In the gravity Seven Gaps lane it is the quantitative yardstick against which genuine phase cancellation is measured, not a dynamical mass formula from the $\phi$-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.