totalClassMass_pos
plain-language theorem explainer
At any complexity cap B, the total mass summed over triangulation classes is strictly positive. The empty-complex class is always present and carries positive gauge mass, so the sum cannot vanish. Anyone bounding the phased quotient-first path sum Zq cites this to keep modulus comparisons meaningful. The proof unfolds the sum and applies Finset.sum_pos with the empty-complex witness.
Claim. For every natural number $B$, the total class mass is strictly positive: $0 < \mathrm{totalClassMass}(B)$. Equivalently, $\sum_q \mu(q) > 0$, where the sum runs over all triangulation classes at cap $B$ and $\mu(q)$ is the positive class mass (gauge volume) of class $q$.
background
Lane D3 of the Seven Gaps program equips the quotient-first path sum $Z_q$ with an explicit oscillatory phase model on labeled configurations that descends to triangulation classes. At fixed complexity cap $B$, $Z_q$ is a finite sum over those classes; its modulus is controlled by the total class mass
$$\mathrm{totalClassMass}(B) := \sum_{q \in \mathrm{TriangulationClass}(B)} \mu(q).$$
Each summand $\mu(q)$ is the class mass coming from the Gap-2 gauge-volume construction; the upstream fact mu_pos states $\mu(q) > 0$ for every class. The empty complex is always a legal labeled configuration at any $B$, so its relabeling class sits in the finite universe of classes. The module proves boundedness $|Z_q| \le \mathrm{totalClassMass}(B) \le |\mathrm{TriangulationClass}(B)|$ and, under pairing hypotheses, stricter cancellation bounds that subtract paired mass from this total.
proof idea
Term-mode proof in three steps. Unfold totalClassMass to the Finset sum of $\mu$ over the universe of triangulation classes. Apply Finset.sum_pos: every summand is positive by mu_pos (Gap2 gauge volume). Nonemptiness of the index set is witnessed by the quotient class of the empty complex at cap $B$, which is a member of Finset.univ. No further arithmetic is required.
why it matters
Without strict positivity the modulus bound $|Z_q| \le \mathrm{totalClassMass}(B)$ and the improved pairing bound $\mathrm{totalClassMass} - \mathrm{pairedMass}$ would be vacuous or could collapse to a zero ceiling. The module uses this fact implicitly in the $B=2$ non-vacuity witness chain (phased_Zq_witness_chain, two_le_totalClassMass_two) and in the general comparisons Zq_norm_le_totalClassMass and Zq_pairing_beats_triangle. Those results sit on the quotient-first path toward a controlled continuum limit of the gravitational path sum; that continuum limit remains open. The declaration is pure finite-sum positivity, not a dynamical derivation of cancellation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.