two_le_totalClassMass_two
plain-language theorem explainer
At complexity cap 2, the total class mass is at least 2. The empty and one-point triangulation classes each carry unit measure and are distinct, so their contribution alone forces the lower bound. Anyone citing the B=2 pairing witness (improved modulus bound totalClassMass 2 - 2) needs this non-vacuity step. The proof is a two-term Finset sum compared to the full universe sum via nonnegativity of mu.
Claim. The total class mass at complexity cap $B=2$ satisfies $2 \le \mathrm{totalClassMass}(2)$. Equivalently, if $\mu$ is the class measure pulled back via quotient representatives, then $\sum_{q \in \mathrm{TriangulationClass}(2)} \mu(\mathrm{out}\, q) \ge 2$, since the empty class and the one-point class are distinct unit-mass classes.
background
This module equips the quotient-first path sum $Z_q$ with an explicit oscillatory phase model at fixed complexity cap $B$. Classes live in TriangulationClass B, the quotient of labeled triangulations by relabeling. The total class mass is the sum of the positive measure $\mu$ over all classes at that cap (via chosen representatives), and is the crude triangle bound on $|Z_q|$.
The empty complex and the one-point complex form two distinct classes at $B=2$, each with unit symmetry factor under $\mu$. The module's pairing theorems improve $|Z_q| \le \mathrm{totalClassMass}, B$ to $\mathrm{totalClassMass}, B - \mathrm{pairedMass}$ when opposite-phase pairs cancel. For that improved bound at $B=2$ (paired mass 2) to be nonnegative and meaningful, one needs $\mathrm{totalClassMass}, 2 \ge 2$.
Status is theorem-level at fixed cap; the continuum limit remains open.
proof idea
Restrict the sum defining total class mass to the two-element Finset ${\mathrm{emptyClass},\mathrm{pointClass}}$. Insert-and-singleton arithmetic plus the unit-mass lemmas for those two classes yields sum exactly 2 (after norm_num). That Finset sits inside the universe of all classes at cap 2, and every summand $\mu(\mathrm{out}, q)$ is nonnegative, so Finset subset comparison lifts the partial sum to the full sum. The full sum is definitionally totalClassMass 2.
why it matters
Closes the non-vacuity gap in the headline $B=2$ witness chain: $|Z_q, 2| \le \mathrm{totalClassMass}, 2 - 2 < \mathrm{totalClassMass}, 2$, with the improved remainder nonnegative. Without this inequality the subtracted pairing mass could overshoot and the "strictly better than triangle" claim would be empty.
It sits in Lane D3 of the Seven Gaps gravity program (phase structure on the quotient-first path sum). The continuum limit and a derived (not hypothesized) cancellation mechanism stay open; this lemma only certifies that the finite-cap arithmetic witness is numerically sensible. No direct T0–T8 forcing step, but it supports the discrete path-sum side of the gravity lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.