is
plain-language theorem explainer
Packages the discrete-gravity convention that an orbit of exact labeled complexes carries measure equal to the symmetry factor of any representative: one over the order of its automorphism group. Authors of the seven-gaps regulator analysis cite it when converting labeled shell counts into quotient shell mass. Definitional typeclass with no proof obligations; it just names the identification with the upstream exact measure.
Claim. For an equivalence class $C$ of exact labeled complexes of signature $(v,e,t)$, the class measure equals $\mu(K)=1/|\mathrm{Aut}(K)|$ for every representative $K\in C$.
background
The ambient module is the seven-gaps regulator-removal no-go at zero phase. It studies the Gaussian-regulated quotient path sum built from exact shell complexes and shows that the $\rho\to 0^+$ limit fails when the action phase vanishes, because shell mass diverges.
The upstream quantity is the labeled symmetry-factor measure: for an exact complex $K$, $\mu(K)=1/|\mathrm{Aut}(K)|$ (the standard discrete-gravity convention). Quotient bookkeeping needs the same number attached to an entire relabeling orbit rather than to a single labeled complex. Relabeling triples act on exact complexes; orbits and automorphism groups are related by the orbit-stabilizer arithmetic developed in the sibling lemmas (torsor equivalence, orbit cardinality, fiberwise sums).
This declaration records that the class-level measure is exactly that labeled $\mu$ evaluated on any chosen representative, so later shell-mass identities can write a single $1/|\mathrm{Aut}|$ per class.
proof idea
No proof body: claim status is definition (typeclass / abbrev style). It aliases the class measure to the upstream exact labeled measure $\mu(K)=1/|\mathrm{Aut}(K)|$ on a representative. Well-definedness across representatives is the content of the surrounding relabeling-extensionality and orbit lemmas, not of this declaration itself.
why it matters
The module's shell-mass identity (Burnside / orbit-stabilizer route) equates the sum of per-class measures $1/|\mathrm{Aut}|$ over the quotient to the labeled count divided by the full relabeling gauge volume $v!\cdot e!\cdot t!$. That identity is the first pillar of the zero-phase no-go: once class measures are $\mu$ of a representative, restricting to signature $(n,n,n)$ yields the lower bound $\mathrm{shellMass},n\ge n^{3n}$, so shell mass is unbounded and the absolute-term route to regulator removal dies.
No downstream edges are recorded for this declaration itself; it is local scaffolding for those mass and no-go theorems. It does not touch oscillatory phases: the module explicitly leaves genuine action-phase cancellation open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.