mu_twoPointComplex
plain-language theorem explainer
The symmetry-factor path-sum weight on the two-vertex edgeless configuration equals exactly 1/2. Anyone separating candidate measures under the named invariance axioms cites this evaluation as the concrete witness point. The proof unfolds mu = 1/|Aut| and substitutes the already-proved automorphism cardinality 2, then closes by arithmetic.
Claim. For every bound $B \ge 2$, if $K$ is the two-vertex edgeless configuration in the bounded complex class of size $B$, then the symmetry-factor measure satisfies $\mu(K) = 1/2$.
background
Lane D1 of the Seven Gaps program asks whether relabeling invariance, positivity, and normalization alone force the path-sum weight on scoped configuration classes. The module answers no: several genuinely different weights satisfy the named InvarianceAxioms, so uniqueness fails.
The standing candidate is the symmetry-factor measure $\mu(K) = 1/|\mathrm{Aut}(K)|$. The two-point witness is the edgeless complex on two vertices (inside the bound $B \ge 2$). Its automorphism group is the order-2 swap of the two vertices; that cardinality is already recorded as a sibling lemma via an explicit equivalence with the permutation triple.
This evaluation is the numerical hinge of the separation: at that witness one has $\mu = 1/2$, while the uniform weight is $1$ and the squared symmetry factor is $1/4$. The empty configuration still carries unit weight under all candidates, so the axioms do not force agreement elsewhere.
proof idea
Term-mode, three steps. Unfold the definition of the symmetry-factor measure (so the goal is $1/|\mathrm{Aut}| = 1/2$). Rewrite the automorphism cardinality by the sibling lemma that $|\mathrm{Aut}|$ of the two-point witness equals 2. Close with norm_num. No case split and no new group theory: the work sits in the prior automorphism-count lemma.
why it matters
This is the concrete numerical witness for the headline no-go that invariance alone underdetermines the path-sum measure. Downstream, the same module uses it to prove the pointwise strict inequality between the symmetry-factor measure and the uniform weight at the two-point configuration, and to prove injectivity of the countable power family of measures (distinct exponents separate at value $(1/2)^{n+1}$).
Outside the module it feeds the Gap-2 ledger-site-blindness results: the two-point and two-point-one-edge witnesses can agree on every ledger site-symmetry count while disagreeing on $\mu$, and any measure that factors through site-symmetry on two-vertex complexes fails gauge counting. It also supplies the control value in the hostile-probe theorem that the wrong labeled weight $1$ fails gauge counting, and blocks the uniform class-mass from being gauge-counting.
In the broader RS gravity stack this closes a killed positive claim ("mu-from-invariance") and keeps the open frontier exactly where the module places it: uniqueness would need richer structure (gluing, orbit-stabilizer, or substrate derivation), not the named invariance package alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.