uniformMeasure_satisfies
plain-language theorem explainer
The constant weight w ≡ 1 on bounded complexes satisfies all four named invariance axioms: relabeling class-function, strict positivity, per-configuration bound ≤ 1, and unit weight on the empty complex. Anyone citing the measure-invariance no-go needs this as one of the two distinct witnesses against uniqueness of 1/|Aut|. The proof is a four-field structure constructor; each field is reflexivity or the elementary facts 0 < 1 and 1 ≤ 1.
Claim. For every natural number $B$, the constant weight $w(K)=1$ on bounded complexes of cap $B$ satisfies the named invariance axioms: it is invariant under relabeling equivalence, strictly positive on every configuration, bounded by $w(K)\le 1$, and equals $1$ on the empty complex.
background
Lane D1 of the Seven Gaps gravity work kills the claim that relabeling invariance plus positivity and normalization uniquely fix the path-sum weight $\mu=1/|\mathrm{Aut}|$. The module scopes the attack to a named axiom bundle on weights $w:\mathrm{BoundedComplex},B\to\mathbb{R}$.
Those axioms are: (i) relabeling class-function behavior ($K\sim K'$ implies $wK=wK'$), (ii) strict positivity $0<wK$, (iii) per-configuration bound $wK\le 1$, and (iv) unit normalization $w(\emptyset)=1$ on the canonical empty complex. The constant candidate is the uniform weight $w\equiv 1$.
The automorphism group $\mathrm{Aut}(K)$ is the set of self-relabelings of a labeled complex; it is used elsewhere to define the competing symmetry-factor measure, but is invisible to the constant weight.
proof idea
Term-mode structure constructor with one proof obligation per axiom field. Relabeling invariance is rfl because the weight ignores its argument. Positivity is one_pos ($0<1$). The bound $\le 1$ is reflexivity of $\le$ at $1$. Unitality on the empty complex is again rfl. No configuration-level case analysis and no appeal to automorphism cardinality.
why it matters
This is Candidate 2 in the explicit witness set that refutes "mu-from-invariance". The headline mu_not_determined_by_invariance conjoins satisfaction for both $\mu=1/|\mathrm{Aut}|$ and the uniform weight, then exhibits the strict inequality at the two-point edgeless complex (where $|\mathrm{Aut}|=2$). The existential packaging invariance_underdetermines_measure likewise uses this theorem as the second arm.
Status bookkeeping records a dedicated flag that this theorem grounds: the grounding theorem ties uniform_satisfies_axioms = true to $\forall B,,\mathrm{InvarianceAxioms},B,(\mathrm{uniformMeasure},B)$. The no-go is deliberately scoped; richer axioms (gluing, orbit-stabilizer, substrate structure) might restore uniqueness, and that remains the open substrate-derivation frontier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.