measureInvarianceNoGoStatus_grounded
plain-language theorem explainer
Grounds the Lane D1 status record: every green flag is witnessed by a kernel theorem, and the three red flags stay false. Anyone citing the invariance no-go for the path-sum weight can point here for the honest boundary. The proof is a pure packaging term: `rfl` on each status bit plus the already-proved satisfaction, separation, and infinite-family lemmas.
Claim. The measure-invariance no-go status record is grounded: the named axioms are stated and, for every bound $B$, some weight $w$ on bounded complexes satisfies them; both the symmetry-factor weight $\mu=1/|\mathrm{Aut}|$ and the uniform weight $1$ satisfy those axioms for every $B$; for every $B\ge 2$ those two weights differ; the countable family $\mu_n=1/|\mathrm{Aut}|^{n+1}$ all satisfy the axioms and is injective for $B\ge 2$; and the three open flags (factorization axiom stateable, substrate measure derived, $Z_{\mathrm{RS}}$ continuum limit) remain false.
background
Lane D1 of the Seven Gaps program asks whether relabeling invariance alone fixes the path-sum configuration weight. The prior positive claim that invariance forces the symmetry-factor measure $\mu=1/|\mathrm{Aut}|$ is killed here as a kernel no-go.
InvarianceAxioms B w packages four properties of a candidate weight $w$ on complexes capped at $B$: it is constant on relabeling equivalence classes, strictly positive, normalized by $w(K)\le 1$, and unital on the empty complex ($w(\emptyset)=1$). The no-go is scoped exactly to this named set.
Three concrete families already satisfy those axioms: the symmetry factor muMeasure, the constant weight uniformMeasure, and the powers muPowMeasure B n = 1/|Aut|^{n+1}. Separation is witnessed on the two-point edgeless complex, whose automorphism group has order 2, so $\mu=1/2\neq 1$. Upstream packaging theorems invariance_underdetermines_measure and invariance_admits_infinite_measure_family record the two-point and countable underdetermination.
proof idea
Pure term-mode packaging of already-proved facts. Each green status bit is discharged by rfl against the canonical status record, paired with the corresponding kernel lemma: existence of some invariant weight via uniformMeasure_satisfies; muMeasure_satisfies and uniformMeasure_satisfies for the two named candidates; muMeasure_ne_uniformMeasure for separation when $B\ge 2$; and muPowMeasure_satisfies together with muPowMeasure_injective for the infinite injective family. The three red flags are likewise rfl to false. No new mathematics is proved; the term only ties status bits to witnesses.
why it matters
This is the honesty seal on the Lane D1 kill. The module headline mu_not_determined_by_invariance already shows two distinct invariant weights; the strengthened form exhibits a countably infinite injective family. The grounding theorem makes the status record citeable: green means a kernel proof exists, red means the corresponding positive claim is still open.
Downstream consumers (none yet wired in the graph) that need a single certificate that the no-go is fully witnessed, rather than a checklist of separate lemmas, land here. Framework-wise this sits in the gravity path-sum layer, not in the T0–T8 forcing chain: it constrains how the configuration measure may be chosen once the eight-tick and $D=3$ structure are fixed, without claiming a continuum $Z_{\mathrm{RS}}$ limit or a substrate derivation of $\mu$.
The open frontier named by the red flags is explicit: a richer axiom set (gluing/factorization, orbit-stabilizer, substrate structure) might restore uniqueness. Until those are stated and proved, invariance alone underdetermines the path-sum measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.