mu
plain-language theorem explainer
Assigns each labeled bounded complex the classical symmetry factor 1/|Aut(K)| as its path-sum weight. Anyone writing or citing the finite Z_RS sum over BoundedComplex configurations uses this measure. The body is a one-line reciprocal of the automorphism-group cardinality (cast to reals).
Claim. For a size bound $B\in\mathbb{N}$ and a labeled bounded complex $K$ (at most $B$ vertices, edges, and tetrahedra, with abstract incidence data), the path-sum measure is $\mu(K)=1/|\mathrm{Aut}(K)|\in\mathbb{R}$, where $\mathrm{Aut}(K)$ is the set of relabelings of $K$ onto itself.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure for the scoped recognition partition function $Z_{RS}$. Configurations are BoundedComplex B: combinatorial, equilateral triangulations at fixed lattice scale (CDT-style), with caps $n_V,n_E,n_T\le B$ and incidence maps for edges and tetrahedra. The metric is dropped; geometry lives in the incidence data only.
An automorphism of a labeled complex $K$ is a relabeling of $K$ onto itself. The module proves that this automorphism set is finite and nonempty (identity always exists), so the classical group-order reciprocal is well-defined as a positive real. The uniform $1/|\mathrm{Aut}|$ convention is stated as MODEL; a substrate-derived nonuniform measure remains open.
The path sum is then $Z(B,w)=\sum_K \mu(K),w(K)$ over the finite labeled class, with modulus bounds and relabeling invariance proved downstream in the same module.
proof idea
Pure definition, not a theorem. The body is the real reciprocal of Nat.card (Aut K), i.e. one over the finite cardinality of the self-relabeling type. No lemmas are applied at the definition site; positivity, the bound $\mu\le 1$, and relabeling invariance are separate theorems that unfold this def.
why it matters
This is the weight that turns the finite labeled class into a genuine path-sum measure for scoped $Z_{RS}$. The module uses it to prove $0<\mu(K)\le 1$, congruence under relabeling, and the sum bounds $|Z|\le\sum\mu$ and $|Z|\le |\mathrm{BoundedComplex},B|$, plus unitary well-definedness when $w=e^{iS}$.
It discharges the symmetry-factor half of the Lane-2 claim: once the configuration class is a Fintype and Aut is finite nonempty, the standard $1/|\mathrm{Aut}|$ factor is available without new axioms. The remaining honesty tags stay open: nonuniform substrate measure, and sharper exponential-growth semantics for exact simplicial subclasses (count-finiteness of the superclass is already proved).
In the broader RS gravity stack this is the combinatorial measure input to the recognition path sum, not a continuum GR measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.