uniformMeasure
plain-language theorem explainer
The uniform weight assigns the constant real value 1 to every bounded combinatorial complex at fixed lattice scale B. It is Candidate 2 among the path-sum weight functions that satisfy the named invariance axioms (relabeling class function, positivity, per-config bound, empty-unit). Gravity and path-sum authors cite it as the explicit second witness that invariance alone does not single out 1/|Aut|. The body is the constant function.
Claim. For each bound $B \in \mathbb{N}$, the uniform weight is the map $w_B : \{\text{bounded complexes of size}\le B\} \to \mathbb{R}$ defined by $w_B(K) = 1$ for every configuration $K$.
background
Lane D1 of the Seven Gaps gravity stack studies whether relabeling invariance plus elementary positivity and normalization axioms fix the path-sum weight on combinatorial triangulations. Configurations are BoundedComplex B: at most B vertices, edges, and tetrahedra, with abstract incidence and no metric field (CDT-style equilateral mesh at fixed lattice scale).
The automorphism group of a labeled complex is the set of self-relabelings. The symmetry-factor candidate is $w(K)=1/|\mathrm{Aut}(K)|$. The module names a fixed axiom package (class function under relabeling, strict positivity, $w(K)\le 1$, and $w(\emptyset)=1$) and asks whether that package determines the weight uniquely.
The uniform weight is the constant function 1. Together with the symmetry factor and its square, it supplies concrete, unequal solutions of the same axiom list.
proof idea
Pure definition: the weight is the constant real function sending every bounded complex to 1. No lemmas are applied; the body is fun _ => 1.
why it matters
This candidate is the second arm of the kernel no-go against the killed claim that invariance forces $\mu=1/|\mathrm{Aut}|$. Downstream, uniformMeasure_satisfies shows it meets every named invariance axiom; muMeasure_lt_uniform_at_witness and muMeasure_ne_uniformMeasure separate it from the symmetry factor at the two-point edgeless complex (where $|\mathrm{Aut}|=2$, so $1/2<1$); and the headline mu_not_determined_by_invariance packages both satisfaction and inequality. Existential packaging (invariance_underdetermines_measure) and status grounding also quote it. The open frontier remains a richer substrate derivation (gluing, orbit-stabilizer, or asymmetric structure) that could restore uniqueness; this definition only supplies the uniform witness inside the named axiom set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.