exactMu_pos
plain-language theorem explainer
For any exact-size combinatorial complex K, the symmetry-factor measure μ(K) = 1/|Aut K| is strictly positive. Discrete-gravity and path-sum arguments cite this to guarantee that every labeled configuration contributes a positive weight before quotienting to classes. The proof unfolds the definition and applies positivity of the automorphism count together with positivity of real division.
Claim. For every exact combinatorial complex $K$ with fixed vertex, edge, and tetrahedron counts, the symmetry-factor measure satisfies $0 < \mu(K)$, where $\mu(K) = 1/|\mathrm{Aut}(K)|$.
background
This module builds exact complexity shells for the Recognition Science path-sum configuration space: complexes with fixed counts $(v,e,t)$ of vertices, edges, and tetrahedra, and no size caps. An ExactComplex carries only incidence data (edge endpoints and tet vertices). Relabelings are bijections of the three index sets that commute with incidence; the automorphism group of $K$ is the set of relabelings of $K$ onto itself.
The symmetry-factor measure is the standard discrete-gravity weight $\mu(K) = 1/|\mathrm{Aut} K|$. Because the identity relabeling always exists, that group is nonempty and finite, so its cardinality is a positive natural number. The module then lifts $\mu$ to equivalence classes and inserts a hand-chosen Gaussian UV regulator $\exp(-\rho n^2)$ on shell complexity $n$; regulator removal remains an open named hypothesis.
proof idea
Unfold $\mu(K)$ to $1/|\mathrm{Aut} K|$. Invoke exactAutCard_pos, which is Nat.card_pos from nonemptiness of the automorphism type (the identity relabeling), to obtain $0 < |\mathrm{Aut} K|$ as a natural number. Cast that inequality to $\mathbb{R}$, then apply div_pos with numerator $1 > 0$. Six-line tactic proof; no algebraic content beyond positivity of reciprocal.
why it matters
Stage-2 of the exact-shell UV module needs every class weight positive before summing regulated shell terms. Downstream, classMu_pos obtains $0 < \mathrm{classMu}, c$ by quotient induction and this lemma, so the per-class measure on ExactPathClass n never vanishes. That positivity feeds the modulus bound on regulated shell terms and the summability proof for every $\rho > 0$.
Within the Seven Gaps gravity program this is bookkeeping, not new physics: the measure is the conventional $1/|\mathrm{Aut}|$ model, the Gaussian regulator is inserted by hand, and continuum/regulator-removal flags stay red. It closes a small proved tier item (positive class measure) required before any claim about $Z_{\mathrm{RS,uv}}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.