mu_le_one
plain-language theorem explainer
For any size-bounded labeled complex K, the symmetry-factor weight μ(K)=1/|Aut K| is at most 1. Path-sum UV bounds and the measure-invariance no-go cite this to keep configuration weights in (0,1]. The proof unfolds μ and applies |Aut K|≥1 via the real division inequality.
Claim. Let $B\in\mathbb{N}$ and let $K$ be a bounded combinatorial complex with at most $B$ vertices, edges, and tetrahedra. Writing $\mathrm{Aut}(K)$ for the group of incidence-preserving relabelings of $K$ onto itself and $\mu(K)=1/|\mathrm{Aut}(K)|$, one has $\mu(K)\le 1$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure for the scoped recognition path integral $Z_{RS}$. Configurations are BoundedComplex B: combinatorial incidence data (vertex/edge/tet counts capped by $B$, edge and tet incidence maps) with the metric field dropped, CDT-style at fixed substrate mesh.
The automorphism group $\mathrm{Aut}(K)$ is the set of relabelings of $K$ onto itself. It is nonempty (identity relabeling) and finite, so the symmetry-factor measure is well-defined as $\mu(K)=1/|\mathrm{Aut}(K)|$. The companion positivity statement gives $0<\mu(K)$; together they pin weights in $(0,1]$.
The local path sum is $Z(B,w)=\sum_K \mu(K),w(K)$ over the finite labeled class. Unit-modulus weights then inherit explicit UV bounds from $\mu\le 1$.
proof idea
Unfold $\mu$ to the reciprocal $1/|\mathrm{Aut}(K)|$. From autCard_pos one has $|\mathrm{Aut}(K)|\ge 1$ as a positive natural, hence as a positive real. Rewrite the goal by div_le_one (valid under that positivity), reducing to $|\mathrm{Aut}(K)|\ge 1$, which is again autCard_pos by casting. No further structure of the complex is used.
why it matters
This is one of the two elementary measure axioms ($0<\mu\le 1$) that make the scoped $Z_{RS}$ honest: finite sum, modulus bounds, and relabeling invariance. Downstream, muMeasure_satisfies packages it into the full invariance-axiom bundle for $1/|\mathrm{Aut}|$; the squared and power families (muSqMeasure_satisfies, muPowMeasure_satisfies) reuse the same $\le 1$ fact via pow_le_one.
On the analytic side it feeds the UV-finiteness bounds Z_norm_le_card and the simplicial restriction Zsimp_norm_le_card (each term $|\mu,w|\le 1$), and the quotient mass bound totalClassMass_le_card (sum of class representatives $\le$ class count). In the Seven Gaps ledger this discharges the weight-normalization half of the assumed growth/admissibility interface for the labeled superclass; sharper exponential growth on exact simplicial subclasses remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.