muPowMeasure_injective
plain-language theorem explainer
Distinct power exponents yield distinct path-sum weights in the family w_n = 1/|Aut|^{n+1}. Anyone citing the infinite underdetermination of the path-sum measure by invariance axioms needs this injectivity. The proof evaluates the family on the two-vertex edgeless complex (where |Aut|=2) and uses that n ↦ (1/2)^{n+1} is strictly decreasing, hence injective.
Claim. For every integer $B \ge 2$, the map $n \mapsto w_n$ sending each natural number $n$ to the configuration weight $w_n(K) = \mu(K)^{n+1}$ (with $\mu(K) = 1/|\mathrm{Aut}(K)|$) is injective as a map into real-valued weights on bounded complexes of width $B$.
background
Lane D1 of the Seven Gaps gravity program asks whether relabeling invariance, positivity, and normalization alone fix the path-sum measure on scoped configuration complexes. The module answers no: the named axiom package InvarianceAxioms is satisfied by many distinct weights, including the countable power family $w_n = \mu^{n+1}$ with $\mu = 1/|\mathrm{Aut}|$.
The separation witness is the two-vertex edgeless complex of width $B \ge 2$. Its automorphism group has order exactly 2, so $\mu = 1/2$ there, while the uniform weight is 1. That single numerical gap lets one distinguish the power family pointwise.
Upstream, $\mu$ on the two-point complex is already computed (mu_twoPointComplex), and the power family itself is the sibling definition muPowMeasure. Injectivity of the family is the remaining algebraic fact needed before packaging the infinite no-go.
proof idea
First evaluate the family on the two-point witness: for every $n$, $w_n(\mathrm{twoPoint}) = \mu(\mathrm{twoPoint})^{n+1}$. Rewrite via mu_twoPointComplex to get $(1/2)^{n+1}$.
Next record that $n \mapsto (1/2)^{n+1}$ is strictly antitone on $\mathbb{N}$ (base in $(0,1)$, exponents strictly increasing under successor). Strictly antitone maps are injective.
If $w_n = w_m$ as functions, their values at the two-point complex agree, so $(1/2)^{n+1} = (1/2)^{m+1}$, hence $n = m$ by the antitone injectivity. No other configurations are needed.
why it matters
This lemma is the second half of the strengthened headline invariance_admits_infinite_measure_family: not only does every power weight satisfy the named invariance axioms, the family is countably infinite and pairwise distinct. Without injectivity the infinite family could collapse to finitely many measures; with it, underdetermination is not a two-point accident.
It also feeds measureInvarianceNoGoStatus_grounded, which ties every true status flag to a kernel statement. In the broader RS gravity stack this keeps the path-sum measure on the open substrate-derivation frontier: invariance alone does not force $\mu = 1/|\mathrm{Aut}|$, so uniqueness (if any) must come from richer structure (gluing, orbit-stabilizer, or substrate axioms) still outside the named package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.