Encyclopedia Gravity Gravity Seven Gaps Measure Invariance No Go Mu Not Determined By Invariance

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Measure Invariance No Go Mu Not Determined By Invariance

A natural symmetry requirement does not uniquely fix how to weigh configurations in a path-sum; the framework's machine-checked library proves this with explicit counterexamples.

Verify this page

Invariance alone underdetermines the measure

In the Recognition Science framework, a path-sum measure assigns a weight to each possible discrete configuration of a system. The most natural candidate is the symmetry-factor measure, written mu = 1/|Aut|, which divides 1 by the number of symmetries (automorphisms) of the configuration. A configuration with two symmetries gets weight 1/2; a configuration with only one gets weight 1. The question is whether this measure is the only one that respects basic invariance: the requirement that relabeling the parts of a configuration does not change its weight.

The framework's machine-checked library of formal theorems proves that invariance alone does not determine the measure. The theorem mu_not_determined_by_invariance shows that at least two different weight functions satisfy all the named invariance axioms: the symmetry-factor measure and a uniform measure that assigns weight 1 to every configuration. These two are unequal, and the theorem exhibits a concrete witness: a two-vertex configuration with no edges, whose automorphism group has cardinality exactly 2, so the symmetry-factor measure assigns it weight 1/2 while the uniform measure assigns weight 1. The library further proves that this is not a two-way tie: there is a countably infinite family of distinct measures, each of the form 1/|Aut|^n for n = 1, 2, 3, ..., all satisfying the same axioms.

The named axioms are modest: relabeling invariance, strict positivity, that no configuration outweighs the reference weight 1, and that the empty configuration has weight exactly 1. The no-go result is scoped to exactly this set. A strictly richer axiom set, for instance one that includes a gluing or factorization rule, could in principle restore uniqueness. That richer set is the open substrate-derivation frontier: the library records that no substrate axiom set in the existing machinery forces a unique measure, and that deriving the symmetry-factor measure from more basic recognition-ledger axioms remains open. The continuum limit of the path-sum measure is also open.

The practical consequence is a sharp boundary on what symmetry arguments can achieve. Relabeling invariance, positivity, and normalization are not enough to single out the symmetry-factor measure. Any future derivation of that measure must invoke additional structure, and the library names the missing piece: a disjoint-union or gluing axiom, which the current machinery cannot even state because its configuration class carries no such operation. The theorem does not claim the symmetry-factor measure is wrong; it claims that its justification cannot rest on invariance alone.

THEOREM mu_not_determined_by_invariance · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean
mu_not_determined_by_invariance · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean:297 
/-- **HEADLINE (KILL + WITNESS).**  The named invariance axioms do NOT
determine the path-sum measure: the symmetry-factor measure `1/|Aut|`
and the uniform weight 1 BOTH satisfy every named axiom, yet they are
unequal, with the pointwise strict inequality exhibited at the concrete
two-point witness (where `|Aut| = 2`).  This is the kernel refutation of
the killed "mu-from-invariance" determination claim; the substrate
derivation of a unique measure remains OPEN. -/
theorem mu_not_determined_by_invariance (B : ℕ) (hB : 2 ≤ B) :
    InvarianceAxioms B (muMeasure B) ∧
    InvarianceAxioms B (uniformMeasure B) ∧
    muMeasure B ≠ uniformMeasure B ∧
    muMeasure B (twoPointComplex B hB) <
      uniformMeasure B (twoPointComplex B hB) :=
  ⟨muMeasure_satisfies B, uniformMeasure_satisfies B,
    muMeasure_ne_uniformMeasure B hB,
    muMeasure_lt_uniform_at_witness B hB⟩
THEOREM mu_twoPointComplex · autCard_twoPointComplex · muMeasure_lt_uniform_at_witness · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean
mu_twoPointComplex · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean:191 
/-- **THEOREM.**  The symmetry-factor measure of the two-point witness is
exactly `1/2`. -/
theorem mu_twoPointComplex (B : ℕ) (hB : 2 ≤ B) :
    mu (twoPointComplex B hB) = 1 / 2 := by
  unfold mu
  rw [autCard_twoPointComplex B hB]
  norm_num
autCard_twoPointComplex · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean:180 
/-- **THEOREM.**  `|Aut(twoPoint)| = 2` exactly (the identity and the
vertex swap). -/
theorem autCard_twoPointComplex (B : ℕ) (hB : 2 ≤ B) :
    Nat.card (Aut (twoPointComplex B hB)) = 2 := by
  rw [Nat.card_congr (twoPointAutEquiv B hB), Nat.card_eq_fintype_card,
    Fintype.card_prod, Fintype.card_prod,
    Fintype.card_equiv (Equiv.refl (Fin 2)),
    Fintype.card_equiv (Equiv.refl (Fin 0)),
    Fintype.card_fin 2, Fintype.card_fin 0]
  norm_num [Nat.factorial]
muMeasure_lt_uniform_at_witness · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean:254 
/-- **Pointwise strict separation.**  At the two-point witness the
symmetry-factor measure is strictly below the uniform weight:
`1/2 < 1`. -/
theorem muMeasure_lt_uniform_at_witness (B : ℕ) (hB : 2 ≤ B) :
    muMeasure B (twoPointComplex B hB) <
      uniformMeasure B (twoPointComplex B hB) := by
  show mu (twoPointComplex B hB) < 1
  rw [mu_twoPointComplex B hB]
  norm_num
THEOREM invariance_admits_infinite_measure_family · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean
invariance_admits_infinite_measure_family · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean:340 
/-- **HEADLINE (strengthened form).**  The named invariance axioms admit a
countably INFINITE injective family of measures `1/|Aut|^(n+1)`: the
underdetermination is not a two-point accident. -/
theorem invariance_admits_infinite_measure_family (B : ℕ) (hB : 2 ≤ B) :
    (∀ n : ℕ, InvarianceAxioms B (muPowMeasure B n)) ∧
      Function.Injective (muPowMeasure B) :=
  ⟨muPowMeasure_satisfies B, muPowMeasure_injective B hB⟩
THEOREM measureInvarianceNoGoStatus · measureInvarianceNoGoStatus_grounded · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean
measureInvarianceNoGoStatus · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean:373 
/-- The canonical status record. -/
def measureInvarianceNoGoStatus : MeasureInvarianceNoGoStatus where
  named_axioms_stated := true
  mu_satisfies_axioms := true
  uniform_satisfies_axioms := true
  measures_separated := true
  infinite_family_exhibited := true
  factorization_axiom_stateable := false
  substrate_measure_derived := false
  Z_RS_continuum_limit := false
measureInvarianceNoGoStatus_grounded · IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean:384 
/-- **Grounding theorem.**  Every `true` status flag is tied to a kernel
statement; the RED flags remain false. -/
theorem measureInvarianceNoGoStatus_grounded :
    (measureInvarianceNoGoStatus.named_axioms_stated = true ∧
      ∀ B : ℕ, ∃ w : BoundedComplex B → ℝ, InvarianceAxioms B w) ∧
    (measureInvarianceNoGoStatus.mu_satisfies_axioms = true ∧
      ∀ B : ℕ, InvarianceAxioms B (muMeasure B)) ∧
    (measureInvarianceNoGoStatus.uniform_satisfies_axioms = true ∧
      ∀ B : ℕ, InvarianceAxioms B (uniformMeasure B)) ∧
    (measureInvarianceNoGoStatus.measures_separated = true ∧
      ∀ B : ℕ, 2 ≤ B → muMeasure B ≠ uniformMeasure B) ∧
    (measureInvarianceNoGoStatus.infinite_family_exhibited = true ∧
      (∀ B n : ℕ, InvarianceAxioms B (muPowMeasure B n)) ∧
      ∀ B : ℕ, 2 ≤ B → Function.Injective (muPowMeasure B)) ∧
    measureInvarianceNoGoStatus.factorization_axiom_stateable = false ∧
    measureInvarianceNoGoStatus.substrate_measure_derived = false ∧
    measureInvarianceNoGoStatus.Z_RS_continuum_limit = false :=
  ⟨⟨rfl, fun B => ⟨uniformMeasure B, uniformMeasure_satisfies B⟩⟩,
    ⟨rfl, muMeasure_satisfies⟩,
    ⟨rfl, uniformMeasure_satisfies⟩,
    ⟨rfl, muMeasure_ne_uniformMeasure⟩,
    ⟨rfl, fun B n => muPowMeasure_satisfies B n, muPowMeasure_injective⟩,
    rfl, rfl, rfl⟩

What this page does not claim

The theorem does not claim the symmetry-factor measure is the unique measure satisfying the axioms. The theorem does not claim that a richer axiom set, such as one with a gluing rule, cannot restore uniqueness. The theorem does not claim anything about the continuum limit of the path-sum measure.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND