muSqMeasure_satisfies
plain-language theorem explainer
The squared symmetry-factor weight w(K)=1/|Aut(K)|² satisfies all four named invariance axioms on bounded complexes at cap B. Anyone assembling the Seven Gaps no-go (invariance underdetermines the path-sum measure) cites this as one of the concrete alternative witnesses. The proof is a four-field structure constructor that squares the corresponding facts for μ=1/|Aut|: congruence, positivity, bound ≤1, and unit value on the empty complex.
Claim. For every natural number $B$, the weight $w(K)=\mu(K)^2$ on bounded complexes of cap $B$, where $\mu(K)=1/|\mathrm{Aut}(K)|$, satisfies: relabeling invariance ($K\sim K'$ implies $w(K)=w(K')$), strict positivity $w(K)>0$, per-configuration normalization $w(K)\le 1$, and unit normalization $w(\emptyset_B)=1$ on the canonical empty configuration.
background
Lane D1 of the Seven Gaps program asks whether relabeling invariance plus elementary positivity and normalization fixes the path-sum weight on the scoped configuration class. The module answers no: a named axiom package InvarianceAxioms is satisfied by several genuinely different weights, so invariance alone underdetermines the measure.
The axiom package has four fields on a candidate weight $w$: it is a class function for the relabeling setoid; it is strictly positive; no configuration outweighs the reference weight 1; and the canonical empty complex has weight exactly 1. The baseline symmetry-factor measure is $\mu(K)=1/|\mathrm{Aut}(K)|$. The squared variant studied here is $w(K)=\mu(K)^2$.
Upstream facts already available for $\mu$ include congruence under equivalence (mu_congr), strict positivity (mu_pos), the bound $\mu\le 1$ (mu_le_one), and the empty-complex evaluation $\mu(\emptyset_B)=1$ (mu_emptyComplex). The two-point edgeless complex, with $|\mathrm{Aut}|=2$, is the concrete separator used elsewhere in the module.
proof idea
Construct the four-field structure by discharging each axiom from the corresponding property of $\mu$, after squaring.
Relabeling: reduce the goal to $\mu(K)^2=\mu(K')^2$ and rewrite by mu_congr on the given equivalence. Positivity: apply pow_pos to mu_pos K at exponent 2. Normalization $\le 1$: apply pow_le_one₀ to the nonnegativity of mu_pos and to mu_le_one K. Unital on empty: reduce to $\mu(\emptyset_B)^2=1$, rewrite by mu_emptyComplex B, and finish with norm_num.
No new combinatorial work; the argument is pure transfer of the $\mu$-facts under $x\mapsto x^2$ on $(0,1]$.
why it matters
This declaration supplies one of the three explicit witnesses (alongside the plain symmetry factor and the uniform weight 1) that every named invariance axiom holds for a weight other than $\mu$ itself. Together with the countable family muPowMeasure, it feeds the headline no-go: invariance alone does not single out $1/|\mathrm{Aut}|$ as the path-sum measure.
In the Recognition gravity stack this closes a false uniqueness route for the gauge-volume / path-sum weight. The module doc is explicit that a richer axiom set (gluing, factorization, orbit-stabilizer, substrate structure) might restore uniqueness; that remains the open substrate-derivation frontier. No T0–T8 forcing step is claimed here; the result is a local obstruction inside the gravity measure layer, not a derivation of $D=3$ or of $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.