pairCount_pos
plain-language theorem explainer
For any bounded complex K the gauge volume (count of labeled copies paired with concrete relabeling witnesses) is strictly positive. Discrete-gravity and Seven-Gaps authors cite this to keep the counting mass well-defined and nonzero on every orbit. The proof rewrites the volume as orbit size times |Aut| and multiplies two positivity facts.
Claim. For every bounded complex $K$ in the fixed universe $B$, the gauge volume $\mathrm{pairCount}(K)$ (number of pairs $(K',r)$ with $K'$ gauge-equivalent to $K$ and $r$ a concrete relabeling $K\to K'$) satisfies $0 < \mathrm{pairCount}(K)$.
background
This module derives the discrete-gravity symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ from pure gauge counting, without putting $\mu$ or $\mathrm{Aut}$ into the mass definition. Two raw counts are primary: the orbit cardinality (number of labeled complexes equivalent to $K$ inside the bounded universe) and the pair count (number of pairs consisting of an orbit representative together with a concrete relabeling witness). The pair count is the gauge volume of the orbit; its definition mentions only equivalence and relabeling.
Orbit-stabilizer in this setting gives the factorization $\mathrm{pairCount}(K)=\mathrm{gaugeOrbitCard}(K)\cdot|\mathrm{Aut},K|$: relabeling witnesses form a torsor over the automorphism group, so each labeled copy contributes exactly $|\mathrm{Aut},K|$ witnesses. Upstream positivity of the orbit card records that the orbit is nonempty; positivity of $|\mathrm{Aut},K|$ is the presence of the identity automorphism.
proof idea
One short term proof. Rewrite the pair count via the orbit-stabilizer identity pairCount_eq_orbitCard_mul_autCard, obtaining the product of orbit cardinality and automorphism-group order. Apply Nat.mul_pos to the two factors, using gaugeOrbitCard_pos (orbit nonempty) and autCard_pos (identity lies in Aut).
why it matters
Positivity of the labeled gauge volume is the first step toward a positive, well-defined counting mass on triangulation classes. Downstream, pairCountClass_pos lifts the inequality to the quotient by gauge equivalence via induction on representatives, so every class has strictly positive pair-count denominator.
That feeds the module's main derivation: the counting mass (orbit card over pair count) equals $\mu=1/|\mathrm{Aut}|$, and the counting identity $\nu\cdot\mathrm{pairCount}=\mathrm{orbitCard}$ characterizes the mass uniquely. Without pair-count positivity the reciprocal gauge mass would be undefined or zero on some orbits, blocking the Seven Gaps gauge-preflight path from pure counting to the standard discrete-gravity measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.