mu_pos
plain-language theorem explainer
The symmetry-factor measure on any bounded labeled complex is strictly positive: μ(K) = 1/|Aut K| > 0. Path-sum and class-mass arguments cite this whenever they cancel, divide by, or squeeze μ. The proof unfolds the definition and applies nonemptiness of the automorphism group.
Claim. For every bound $B \in \mathbb{N}$ and every bounded combinatorial complex $K$ of size at most $B$, the symmetry-factor measure satisfies $0 < \mu(K)$, where $\mu(K) = 1/|\mathrm{Aut}(K)|$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure for the scoped recognition configuration class. Configurations are BoundedComplex B: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps and no metric field. The substrate fixes edge length at the minimum mesh, so the class is combinatorial and equilateral (CDT-style).
The measure on a labeled complex is the classical symmetry factor $\mu(K) = 1/|\mathrm{Aut}(K)|$. The automorphism type is finite; a sibling lemma records that its cardinality is at least one (the identity always exists). The path sum is then $Z_B(w) = \sum_K \mu(K), w(K)$ over the finite labeled class.
This positivity fact is the lower half of the elementary bound $0 < \mu(K) \le 1$ stated in the module header; the matching upper bound is the companion theorem that uses $|\mathrm{Aut} K| \ge 1$ the other way.
proof idea
One short tactic proof. Unfold $\mu$ to $1/|\mathrm{Aut} K|$. Cast the sibling lemma that $|\mathrm{Aut} K| \ge 1$ (as a natural) into a strict positivity statement over $\mathbb{R}$. Finish with the standard fact that a positive real divided by a positive real is positive (div_pos of one_pos and that cast).
why it matters
Positivity of $\mu$ is the workhorse inequality under almost every later estimate in the Seven Gaps gravity lane. Downstream it is used to squeeze the labeled Freudenthal-torus summands to zero (tendsto_mu_freudenthal_zero, tendsto_labeledSummand_zero), to bound single labeled summands by $N^{-3}$, and to compare labeled measure against pushforward class mass at the $B=2$ edge class (mu_lt_classMass_edgeClass), which is the numeric T3 fork verdict that classMass is not the same object as per-class $1/|\mathrm{Aut}|$.
It also appears in the gauge-volume layer: the RS measure can be cancelled precisely because it is strictly positive, and the gauge-counting principle is characterized as unit cross-sector fugacity. Together with $\mu \le 1$ and relabeling invariance, this closes the elementary measure package that makes the honest scoped $Z_{\mathrm{RS}}$ well-defined (finite sum, modulus bounds, unitary weights).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.