mu_emptyComplex
plain-language theorem explainer
The symmetry-factor weight equals 1 on the empty path-sum configuration at any vertex cap B. Anyone verifying that 1/|Aut| meets the unit-normalization clause of the named invariance package cites this fact. The argument unfolds the definition, rewrites by the empty automorphism count, and finishes by arithmetic.
Claim. For every natural number $B$, the symmetry-factor measure of the empty configuration with vertex cap $B$ equals one: $\mu(\emptyset_B)=1$.
background
Lane D1 of the Seven Gaps program asks whether relabeling invariance, together with positivity and normalization, forces the path-sum weight to be the symmetry factor $1/|\mathrm{Aut}|$. The module answers no: a named axiom package InvarianceAxioms (class-function under relabeling, strict positivity, per-configuration bound $w(K)\le 1$, and unit normalization on the empty configuration) is satisfied by infinitely many distinct weights.
The symmetry-factor measure is $\mu(K)=1/|\mathrm{Aut}(K)|$. The empty configuration at cap $B$ has no vertices or incidences, so its automorphism group is trivial. Unit normalization $w(\emptyset)=1$ is one of the four named axioms; this theorem discharges that clause for $\mu$.
A sibling computation shows the two-vertex edgeless complex has $|\mathrm{Aut}|=2$, hence $\mu=1/2$ there, separating $\mu$ from the uniform weight $1$.
proof idea
Term-mode proof in three steps. Unfold the definition of the symmetry-factor measure (so the goal becomes a reciprocal of an automorphism cardinality). Rewrite that cardinality by the already-proved fact that the empty configuration has automorphism count $1$. Close with norm_num, which reduces $1/1=1$.
why it matters
This is the unit-normalization conjunct in every "measure satisfies the axioms" package in the module. Downstream, muMeasure_satisfies, muSqMeasure_satisfies, and muPowMeasure_satisfies each quote it as the fourth field of InvarianceAxioms. The same fact is reused in ZqPhaseStructure.mu_out_emptyClass to pin the representative of the empty quotient class at weight $1$.
In the broader no-go, the headline is that invariance alone underdetermines the path-sum measure: $\mu$, the uniform weight, and the countable power family $1/|\mathrm{Aut}|^{n+1}$ all obey the named axioms and disagree on the two-point witness. Unit normalization on the empty complex is the shared baseline that makes that separation meaningful. The module leaves open whether a richer package (gluing, orbit-stabilizer, substrate structure) could restore uniqueness; that is the stated substrate-derivation frontier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.