muPowMeasure
plain-language theorem explainer
Defines the countable family of path-sum weights w_n(K) = (1/|Aut(K)|)^{n+1} on bounded complexes of budget B. Anyone citing the measure-invariance no-go uses this family as the explicit infinite witness that the named invariance axioms underdetermine the measure. The body is a one-line pointwise power of the symmetry-factor measure mu.
Claim. For each budget $B \in \mathbb{N}$ and each exponent index $n \in \mathbb{N}$, define a real weight on bounded complexes of budget $B$ by $w_{B,n}(K) = \mu(K)^{n+1}$, where $\mu(K) = 1/|\mathrm{Aut}(K)|$ is the symmetry-factor measure.
background
Lane D1 of the Seven Gaps gravity work asks whether relabeling invariance plus positivity and normalization fix the path-sum measure on scoped configuration complexes. The module kills the claim that those axioms alone select $\mu = 1/|\mathrm{Aut}|$.
A BoundedComplex B is a labeled configuration with vertex budget $B$. Its automorphism group Aut K is the set of self-relabelings; the base measure is $\mu(K) = 1/|\mathrm{Aut}(K)|$. Named InvarianceAxioms package class-function behavior under the relabeling setoid, strict positivity, per-configuration bound $w(K) \le 1$, and $w(\emptyset) = 1$.
Sibling candidates already include $\mu$ itself, the uniform weight $1$, and $\mu^2$. This definition packages the full power tower $\mu^{n+1}$ so the underdetermination can be stated as a countably infinite injective family rather than a two-point accident.
proof idea
Pure definition: pointwise $K \mapsto \mu(K)^{n+1}$. No tactics. Downstream proofs that every member satisfies the axioms reduce to congruence and positivity of $\mu$ under powering; injectivity of the family is separated at the two-point edgeless complex where $\mu = 1/2$.
why it matters
Supplies the explicit infinite witness family for the strengthened headline invariance_admits_infinite_measure_family: every $w_n$ obeys the named invariance axioms, and distinct $n$ give distinct measures. Also feeds muPowMeasure_satisfies, muPowMeasure_injective, and the grounding status record measureInvarianceNoGoStatus_grounded.
In the Recognition gravity stack this keeps the path-sum measure from being fixed by symmetry bookkeeping alone; uniqueness, if recovered, must come from richer structure (gluing/factorization, orbit-stabilizer, substrate derivation), which the module flags as the open frontier. It does not touch T0–T8 forcing, RCL, or the $\varphi$-ladder mass formula; it is a local no-go inside the Seven Gaps measure story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.