pairCountClass_pos
plain-language theorem explainer
Any triangulation class carries a strictly positive gauge-volume pair count. Discrete-gravity arguments that define orbit mass by dividing labeled-orbit size by that volume cite this positivity to justify the division. The proof is a one-line quotient induction reducing to positivity on labeled representatives.
Claim. For every equivalence class $c$ of bounded triangulations, the class-level gauge pair count (number of labeled-copy and relabeling-witness pairs) is strictly positive: $0 < N_{\mathrm{pair}}(c)$.
background
This module sits in the Seven Gaps gauge-preflight layer. PathSumMeasure postulates the discrete-gravity symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$. Here that factor is derived from pure counting: the labeled orbit size (how many complexes are gauge-equivalent to a representative) and the pair count (how many pairs of a labeled copy together with a concrete relabeling witness exist). The pair count is the gauge volume of the orbit; its definition mentions only equivalence and relabeling, never $\mu$ or $\mathrm{Aut}$.
Triangulation classes are the quotient of bounded complexes by gauge equivalence. Class-level orbit card and pair count are the well-defined lifts of the representative-level counts. The gauge-orbit mass of a class is then labeled copies per unit gauge volume: orbit card divided by pair count. Downstream existence and uniqueness theorems for that mass need the denominator nonzero, which is exactly the present claim.
On representatives, positivity of the pair count is already available (every complex has at least the identity self-relabeling in its own orbit). The class statement is the quotient transport of that fact.
proof idea
Term-mode one-liner. Apply quotient induction on the class $c$, reducing the goal to a labeled representative $K$. Invoke the already-proved representative lemma that the pair count of $K$ is strictly positive. No further algebraic work: the class function is defined so that its value on the class equals the representative value, and positivity transfers directly.
why it matters
This is the nonzero-denominator lemma for the counting derivation of the $1/|\mathrm{Aut}|$ measure. Two parent theorems use it immediately: the existence identity (gauge-orbit mass times pair count equals orbit card) cancels the pair-count factor after casting to reals, and the uniqueness theorem shows any class mass satisfying that normalized counting property equals the gauge-orbit mass, again by dividing by a nonzero pair count.
Together with the torsor/orbit-stabilizer factorization (pair count equals orbit card times automorphism order) and the equality of gauge-orbit mass with $\mu$, the module converts a model premise (gauge volume equals the copy-witness pair count) into the standard discrete-gravity measure. Without class-level positivity, the real division that defines the mass on the quotient would be ill-formed. The result is fully proved scaffolding for the Seven Gaps gravity path-sum, not an open interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.