muMeasure
plain-language theorem explainer
Defines the symmetry-factor path-sum weight on bounded complexes of size bound B by sending each configuration K to 1/|Aut(K)|. Gravity and path-sum workers cite it as Candidate 1 among weights that obey the named invariance axioms. The body is a one-line eta-expansion of the existing scalar mu.
Claim. For each natural number $B$, define a real-valued weight on bounded complexes of bound $B$ by $w(K) = 1/|\mathrm{Aut}(K)|$, the reciprocal of the automorphism-group order of $K$.
background
Lane D1 of the Seven Gaps gravity program asks whether relabeling invariance, positivity, and normalization alone force a unique path-sum measure on the scoped configuration class BoundedComplex B. The module kills the prior positive claim that those axioms single out the symmetry factor: it names a finite axiom package (InvarianceAxioms) and exhibits several distinct weights that all satisfy it.
The standing candidate is the classical symmetry-factor weight $\mu(K) = 1/|\mathrm{Aut}(K)|$. Upstream, mu is already defined on the path-sum configuration type and is known to be a class function for the relabeling setoid, strictly positive, at most one, and equal to 1 on the empty complex. The two-point edgeless complex is the concrete witness later: its automorphism group has order exactly 2, so $\mu = 1/2$ there.
This definition simply packages that scalar as a named weight function of type BoundedComplex B → ℝ, so it can sit beside the uniform weight 1 and the squared factor $1/|\mathrm{Aut}|^2$ in the no-go statements.
proof idea
Definitional one-liner: muMeasure B is the function fun K => mu K. No tactics, no new arithmetic; it re-exports the existing symmetry-factor scalar at the measure-function type expected by InvarianceAxioms.
why it matters
This is Candidate 1 in the kernel no-go that invariance alone underdetermines the path-sum measure. Downstream, muMeasure_satisfies shows it meets every named axiom; muMeasure_lt_uniform_at_witness and muMeasure_ne_uniformMeasure separate it from the uniform weight at the two-point complex; and the headline mu_not_determined_by_invariance packages both satisfaction and strict inequality. Existential packaging (invariance_underdetermines_measure) and the status grounding theorem also name it explicitly.
In the broader RS gravity story this keeps the substrate-derivation frontier honest: uniqueness of the path-sum weight, if it exists, must come from richer structure (gluing, orbit-stabilizer, or substrate axioms), not from the thin invariance package alone. The killed "mu-from-invariance" determination claim stays dead.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.