Gravity Seven Gaps Measure Invariance No Go Mu Measure Ne Uniform Measure

The underdetermination result

A measure, in this context, is a rule that assigns a weight to each configuration in a discrete collection, and the path-sum measure is the rule used to weigh the contributions of configurations in a sum over paths. The declaration muMeasure_ne_uniformMeasure is a proved theorem in the framework's machine-checked library of formal theorems. It states that two specific measures, the symmetry-factor measure and the uniform measure, are not equal. The symmetry-factor measure weights a configuration by the reciprocal of the size of its automorphism group, the group of relabelings that leave the configuration unchanged. The uniform measure simply assigns weight 1 to every configuration.

The theorem is a no-go result: it kills a prior attempt to derive the symmetry-factor measure from invariance principles alone. The named axioms, called InvarianceAxioms, require that a measure be invariant under relabeling, strictly positive, normalized so no configuration outweighs weight 1, and unital on the empty configuration. The theorem proves that both the symmetry-factor measure and the uniform measure satisfy all four axioms, and yet they are unequal. A concrete witness exhibits the difference: a configuration with two vertices and no edges has an automorphism group of size 2, so the symmetry-factor measure assigns it weight 1/2, while the uniform measure assigns weight 1.

The result is stronger than a single counterexample. The library also proves that a countably infinite family of measures, the powers of the symmetry factor, all satisfy the same axioms and are all distinct from one another. This establishes that the named invariance axioms underdetermine the measure: they do not single out any one rule. The theorem does not claim that no axiom set could ever determine a unique measure. A richer set of axioms, such as one including a gluing or factorization condition, might restore uniqueness, and deriving the measure from deeper substrate axioms remains an open target in the framework.

What the result changes is the status of a derivation claim. The positive claim that invariance fixes the symmetry-factor measure is refuted, not supported. The theorem does not derive the symmetry-factor measure from recognition-ledger substrate axioms; that derivation remains unformalized and open. It also does not concern the continuum limit of the theory, which is likewise open. The no-go is scoped precisely to the axioms named in the library, and that scope is part of the theorem's meaning.

/-- The two candidate measures are unequal as functions. -/
theorem muMeasure_ne_uniformMeasure (B : ℕ) (hB : 2 ≤ B) :
    muMeasure B ≠ uniformMeasure B := fun h =>
  absurd (congrFun h (twoPointComplex B hB))
    (ne_of_lt (muMeasure_lt_uniform_at_witness B hB))

/-- **THEOREM.**  `1/|Aut|` satisfies every named invariance axiom. -/
theorem muMeasure_satisfies (B : ℕ) : InvarianceAxioms B (muMeasure B) :=
  ⟨fun _ _ h => mu_congr h, fun K => mu_pos K, fun K => mu_le_one K,
    mu_emptyComplex B⟩

/-- **THEOREM.**  The uniform weight 1 satisfies every named invariance
axiom. -/
theorem uniformMeasure_satisfies (B : ℕ) :
    InvarianceAxioms B (uniformMeasure B) :=
  ⟨fun _ _ _ => rfl, fun _ => one_pos, fun _ => le_refl 1, rfl⟩

/-- **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]

/-- **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

/-- **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⟩

/-- **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⟩

What this page does not claim

The theorem does not derive the symmetry-factor measure from deeper substrate axioms. The theorem does not concern the continuum limit of the theory. The theorem does not claim that no axiom set could ever determine a unique 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: