exactMu_le_one
plain-language theorem explainer
For any exact-size combinatorial complex K, the symmetry-factor measure μ(K) = 1/|Aut K| is at most 1. Discrete-gravity and path-sum arguments cite this to bound per-class weights before shell summation. The proof unfolds the definition and uses positivity of the automorphism count (the identity always exists).
Claim. Let $K$ be an exact combinatorial complex with fixed vertex, edge, and tetrahedron counts. Writing $\mu(K) = 1/|\mathrm{Aut}(K)|$ for the reciprocal of the order of its automorphism group, one has $\mu(K) \le 1$.
background
This module builds exact complexity shells for the quotient-class path-sum configuration space: labeled complexes with fixed counts $(v,e,t)$ and no size caps, then a Gaussian UV regulator $\exp(-\rho n^2)$ on the shell series. The honesty protocol keeps the regulator and the phase/action as mathematical parameters; regulator removal and continuum limits stay open.
An ExactComplex v e t is a cap-free incidence structure: edge endpoints in $\mathrm{Fin},v$ and tetrahedron vertices $\mathrm{Fin},4\to\mathrm{Fin},v$. An exact relabeling is a triple of bijections on the index sets commuting with incidence; ExactAut K is the monoid of self-relabelings, always nonempty via the identity. The symmetry-factor measure is the standard discrete-gravity weight $\mu(K)=1/|\mathrm{Aut},K|$.
Upstream, exactAutCard_pos records $|\mathrm{Aut},K|\ge 1$ (equivalently positive cardinality) from the identity automorphism.
proof idea
Unfold $\mu(K)=1/|\mathrm{Aut},K|$. Cast exactAutCard_pos to obtain $0 < |\mathrm{Aut},K|$ in $\mathbb{R}$, so div_le_one reduces the claim to $1\le |\mathrm{Aut},K|$. That inequality is again exactAutCard_pos (for natural numbers, positive cardinality means at least one). Purely arithmetic; no structure theory of the automorphism group is used beyond existence of the identity.
why it matters
Stage 2 of the exact-shell UV module needs the per-class measure bounded by 1 so that regulated shell terms admit a modulus bound and the Gaussian series is summable for every $\rho>0$. Downstream, classMu_le_one lifts the labeled inequality to equivalence classes by quotient induction: every ExactPathClass representative satisfies $\mathrm{classMu},c\le 1$.
Together with positivity and global-equivalence invariance of $\mu$, this closes the elementary measure axioms on exact shells. It does not touch continuum limits, regulator removal (HasZRSRegulatorRemoval remains false), or any FullTheoryLedger flag. The bound is the discrete-gravity convention that each orbit contributes at most unit weight before the UV factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.