MeasureInvarianceNoGoStatus
plain-language theorem explainer
Status record bundling Boolean flags for the measure-invariance no-go on path-sum weights. Each true flag is grounded by a kernel theorem (named axioms, two distinct measures satisfying them, infinite family, separation); the RED flags stay false for open substrate and continuum questions. Gravity auditors cite it to read the lane's closed vs open ledger at a glance. It is a plain structure definition, not a proved claim.
Claim. A status record with Boolean fields: whether the named invariance axioms (relabeling class function, strict positivity, $w(K)\le 1$, $w(\emptyset)=1$) are stated; whether the symmetry-factor measure $\mu=1/|\mathrm{Aut}|$ and the uniform weight $1$ both satisfy them; whether those measures are separated and an infinite family is exhibited; whether a disjoint-union factorization axiom is stateable on the existing bounded-complex machinery; and two open RED flags (substrate derivation of a unique measure; $Z_{\mathrm{RS}}$ continuum limit).
background
Lane D1 of the Seven Gaps program asks whether relabeling invariance alone forces the path-sum weight on bounded complexes. The killed positive claim was that positivity, normalization, and invariance under the relabeling setoid single out $\mu=1/|\mathrm{Aut}|$. This module refutes that determination claim as a kernel no-go.
The named axiom package InvarianceAxioms requires four properties of a weight $w$: it is constant on relabeling-equivalent configurations, strictly positive, bounded by $1$ on every configuration, and equals $1$ on the empty complex. Concrete witnesses include the empty complex and the two-vertex edgeless complex (automorphism group of order $2$), so $\mu=1/2$ there while the uniform weight is $1$.
The module also exhibits $\mu^2=1/|\mathrm{Aut}|^2$ and a countable power family, all satisfying the same axioms. A richer package (gluing/factorization, orbit-stabilizer, substrate structure) might restore uniqueness; that remains the open frontier flagged below.
proof idea
No proof body: this is a structure type whose fields are Booleans with doc-comments pointing at the kernel theorems that ground each flag. The companion definition measureInvarianceNoGoStatus fills the record with true for the five closed items (axioms stated; $\mu$ and uniform satisfy them; measures separated; infinite family exhibited) and leaves the factorization-stateability and two RED substrate/continuum flags as the honesty ledger. Downstream code reads the record rather than re-proving the no-go.
why it matters
Gives a single machine-readable ledger for Lane D1: invariance underdetermines the path-sum measure. The parent value is the canonical instance measureInvarianceNoGoStatus, which sets the closed flags true and keeps substrate derivation and the $Z_{\mathrm{RS}}$ continuum limit false. That matches the module headline mu_not_determined_by_invariance and the infinite-family witness.
In the broader Recognition stack this blocks any shortcut that would derive the symmetry-factor measure from class-function axioms alone, forcing later gravity and path-sum work to supply genuine substrate or factorization structure. The RED flags mark exactly those open questions: no unique measure from the present substrate, and no continuum-limit identification of the RS partition function yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.