IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo
No-go module for path-sum weights on bounded configuration complexes: relabeling invariance, positivity, and normalization do not select a unique measure. Gravity workers on the Seven Gaps path-sum lane cite it to block pure-invariance uniqueness claims. The argument builds explicit finite complexes (empty and two-point), computes automorphism counts, and exhibits several distinct axiom-satisfying measures.
claimOn the scoped class of bounded incidence complexes at complexity cap $B$, the axiom package of relabeling invariance, positivity, and normalization does not uniquely determine a path-sum weight $w$. Finite model complexes (empty complex; two-point complex) admit multiple distinct normalized positive Aut-invariant measures, including the uniform measure and powers of a base counting measure $\mu$.
background
Lane 2 of the Seven Gaps gravity program works with a scoped configuration class BoundedComplex B: finite incidence data with an explicit complexity cap. The upstream path-sum measure module proves that this class is a Fintype via a coding equivalence, so sums and normalizations are ordinary finite arithmetic rather than measure-theoretic limits.
A candidate path-sum weight $w$ is asked to obey a named package of invariance axioms: invariance under complex automorphisms (relabeling), positivity on admissible configurations, and normalization of the total mass. The module isolates exactly that axiom set; nothing beyond it is assumed.
Concrete test objects are the empty complex and a two-point complex, together with their automorphism groups and cardinalities. Several explicit measures are defined on these objects: a base counting measure $\mu$, the uniform measure, and powered variants $\mu^2$ and $\mu^k$.
proof idea
Definition-first layout, then finite counter-models. The module names the invariance axiom package, then builds the empty complex and a two-point complex with an explicit automorphism equivalence. Automorphism cardinalities and the values of $\mu$ on those complexes are computed by direct enumeration (subsingleton automorphism group on the empty complex; order-two symmetry on the two-point complex).
Several candidate measures (uniform, $\mu$-squared, $\mu$-powered) are shown to satisfy the same invariance, positivity, and normalization axioms while disagreeing as functions. That multiplicity is the no-go: the axiom set does not pin down a unique path-sum weight on the scoped class.
why it matters in Recognition Science
This module is the exact substrate blocker for uniqueness-from-invariance in the path-sum lane. Downstream, MeasureSubstrateBlocker quotes it directly: relabeling invariance, positivity, and normalization do not select a path-sum measure, so any uniqueness claim must import extra structure (e.g. a gauge-density or shell principle).
ZqPhaseStructure imports the same no-go when it moves to the quotient-first object and adds an oscillatory phase model; the continuum limit remains open, but at fixed complexity cap the phase layer sits on top of a non-unique measure substrate.
In the broader Recognition gravity stack this closes a naive route to a canonical $Z_{\mathrm{RS}}$ weight and forces later lanes to state their selection principles explicitly rather than hide them inside invariance language.
scope and limits
- Does not claim every conceivable axiom package fails; only the named invariance-positivity-normalization set.
- Does not address continuum or infinite-complexity limits; all models are finite at fixed cap B.
- Does not construct the physical RS path-sum weight; it only blocks uniqueness from these axioms.
- Does not rule out uniqueness after adding gauge-density, shell, or phase selection principles.
- Does not treat complexes outside the scoped BoundedComplex class.
used by (2)
depends on (1)
declarations in this module (26)
-
structure
InvarianceAxioms -
instance
instSubsingletonAutEmpty -
theorem
autCard_emptyComplex -
theorem
mu_emptyComplex -
abbrev
twoPointComplex -
def
twoPointAutEquiv -
theorem
autCard_twoPointComplex -
theorem
mu_twoPointComplex -
def
muMeasure -
def
uniformMeasure -
def
muSqMeasure -
def
muPowMeasure -
theorem
muMeasure_satisfies -
theorem
uniformMeasure_satisfies -
theorem
muSqMeasure_satisfies -
theorem
muPowMeasure_satisfies -
theorem
muMeasure_lt_uniform_at_witness -
theorem
muMeasure_ne_uniformMeasure -
theorem
muSqMeasure_separations -
theorem
mu_not_determined_by_invariance -
theorem
invariance_underdetermines_measure -
theorem
muPowMeasure_injective -
theorem
invariance_admits_infinite_measure_family -
structure
MeasureInvarianceNoGoStatus -
def
measureInvarianceNoGoStatus -
theorem
measureInvarianceNoGoStatus_grounded