classMu_pos
plain-language theorem explainer
Every equivalence class of exact complexes at fixed complexity carries strictly positive per-class measure (reciprocal automorphism order). Path-sum and shell-mass arguments in the seven-gaps gravity stack cite it to keep shell masses and modulus bounds non-vacuous. Proof: destructure the Σ-class and run quotient induction onto the labeled positivity lemma.
Claim. For every $n \in \mathbb{N}$ and every class $c$ in the exact complexity shell of level $n$, the per-class measure satisfies $0 < \mu(c)$.
background
This module builds cap-free exact complexity shells for the Recognition path-sum configuration space and studies a Gaussian-UV-regulated shell series. An exact path class at level $n$ is a shell signature together with a quotient of labeled exact complexes by global relabeling equivalence; no bounded-complex cap appears in the type.
The per-class measure on a shell element is the descent of the labeled measure $\mu(K)=1/|\mathrm{Aut}(K)|$. Upstream, labeled positivity is already proved: the automorphism monoid of any exact complex is inhabited, so its cardinality is a positive natural, and the reciprocal is positive. The present statement lifts that fact from labeled complexes to quotient classes.
Local honesty constraints still apply: the regulator $\exp(-\rho n^2)$ is inserted by hand, the phase is an arbitrary class-invariant parameter, and regulator removal ($\rho\to 0^+$) remains a named open.
proof idea
Term-mode, three steps. Unpack the shell class as a dependent pair (signature, quotient element). Apply Quotient.inductionOn to the quotient component, reducing the goal to a labeled exact complex $K$. Discharge with the upstream lemma that $0<\mu(K)$ for every labeled exact complex (via $1/|\mathrm{Aut}(K)|$ and positive automorphism cardinality). No new arithmetic is introduced.
why it matters
Stage-2 bookkeeping in the exact-shell UV module: positivity of class measure is the ingredient that makes every shell mass strictly positive (sum of positive terms over a nonempty finite type) and feeds the modulus bound on regulated shell terms used for summability of the Gaussian series.
Downstream parents: the shell-mass positivity theorem (every shell has positive total measure via the isolated-vertex witness), the regulated-shell modulus bound ($|Z_n|\le e^{-\rho n^2}\cdot|\mathrm{shell}|$), and the cube-signature comparison in the regulator-removal no-go module (cube sum bounded by full shell mass because every class measure is positive).
It does not touch continuum limits, physical actions, or the open HasZRSRegulatorRemoval flag; those stay red by module protocol. Framework role is combinatorial measure hygiene inside the gravity seven-gaps stack, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.