module module high

`IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo`

Relabeling invariance, positivity, and normalization do not uniquely select a path-sum weight on the bounded configuration class. The module exhibits finite complexes (empty and two-point) that carry several distinct normalized positive Aut-invariant measures. Seven-Gaps gravity authors cite it as the exact substrate blocker for Gap-2 measure selection. The argument is by explicit finite models and Aut-cardinality computations.

claimOn the scoped class of bounded complexes at complexity cap $B$, the axiom package of Aut-relabeling invariance, positivity, and normalization does not determine a unique path-sum weight $w$. Explicit counter-models include the empty complex and a two-point complex, each admitting multiple distinct measures (uniform, squared, and power measures) that satisfy the same axioms.

background

Gap-2 of the Seven Gaps gravity program asks for a canonical path-sum measure on configuration space for the recognition ledger $Z_{RS}$. Upstream, PathSumMeasure shows that the scoped class BoundedComplex at cap $B$ is a finite type via an explicit coding equivalence, so discrete probability weights are well-defined on a finite set of incidence configurations.

This module isolates a named axiom package for a candidate weight $w$: invariance under automorphisms (relabelings of the complex), positivity, and normalization. The no-go theorem is scoped exactly to that package. Sibling constructions introduce the empty complex and a two-point complex, compute their automorphism groups and cardinalities, and define several Aut-invariant measures on them (uniform $1/|\mathrm{Aut}|$, squared, and power variants).

proof idea

The module is an explicit counterexample factory, not an abstract uniqueness obstruction. It packages the named invariance axioms, then builds two finite test objects: the empty complex (trivial Aut) and a two-point complex with a nontrivial Aut group, together with equivalences that fix $|\mathrm{Aut}|$. On these objects it defines several measures (uniform, squared, power) and checks that each satisfies the same invariance, positivity, and normalization axioms. Distinct weights meeting one axiom set yield the no-go. Downstream blockers quote that non-uniqueness directly.

why it matters in Recognition Science

MeasureSubstrateBlocker cites this module as the theorem that relabeling invariance, positivity, and normalization do not select a path-sum measure, and pairs it with the gauge-counting preflight that $|\mathrm{Aut}|^{-1}$ mass needs an extra MODEL premise. GaugeCountingInevitableReasons and InsertionAsymmetryInevitableReasons import it into necessary-reasons censuses for Gap-2 targets (physical mass $\nu=1/|\mathrm{Aut}|$, or asymmetric birth/death rate laws). Hostile-probe and $Z_q$ phase-structure modules also depend on the no-go as substrate. In the Seven Gaps gravity lane it forces the framework past pure invariance toward gauge-counting or insertion-asymmetry principles whenever a unique physical measure is required.

scope and limits

Does not claim uniqueness fails for axiom packages strictly larger than the named invariance set.
Does not build continuum or infinite-complex counterexamples; scope is finite BoundedComplex at cap B.
Does not refute gauge-counting mass 1/|Aut| as a separate selection principle.
Does not treat dynamical or temporal path-sum weights outside the static configuration class.
Does not prove existence of a preferred physical measure; only non-uniqueness under the named axioms.

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureDerivationHostileProbe module_import
IndisputableMonolith.Gravity.SevenGaps.GaugeCountingInevitableReasons module_import
IndisputableMonolith.Gravity.SevenGaps.InsertionAsymmetryInevitableReasons module_import
IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker module_import
IndisputableMonolith.Gravity.SevenGaps.ZqPhaseStructure module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure module_import

declarations in this module (26)

structure InvarianceAxioms L99
instance instSubsingletonAutEmpty L126
theorem autCard_emptyComplex L134
theorem mu_emptyComplex L140
abbrev twoPointComplex L154
def twoPointAutEquiv L167
theorem autCard_twoPointComplex L182
theorem mu_twoPointComplex L193
def muMeasure L202
def uniformMeasure L205
def muSqMeasure L208
def muPowMeasure L212
theorem muMeasure_satisfies L216
theorem uniformMeasure_satisfies L222
theorem muSqMeasure_satisfies L227
theorem muPowMeasure_satisfies L240
theorem muMeasure_lt_uniform_at_witness L257
theorem muMeasure_ne_uniformMeasure L265
theorem muSqMeasure_separations L271
theorem mu_not_determined_by_invariance L304
theorem invariance_underdetermines_measure L316
theorem muPowMeasure_injective L324
theorem invariance_admits_infinite_measure_family L343
structure MeasureInvarianceNoGoStatus L353
def measureInvarianceNoGoStatus L374
theorem measureInvarianceNoGoStatus_grounded L386