Gravity Seven Gaps Measure Substrate Blocker Uniform Class Mass

The uniform decoy

In mathematics, a class of objects often comes with symmetries: relabelings that leave the object essentially the same. The framework's gravity program studies classes of bounded complexes, which are finite geometric shapes built from triangles, and it assigns each class a real number called its mass. The simplest possible assignment gives every class the same mass, namely 1. The declaration uniformClassMass is exactly that choice: a definition, not a theorem, that sets the mass of every class to 1.

The framework's ledger, a discrete record of events, requires that mass obey a stricter rule called normalized gauge counting. The rule says that a class's mass, multiplied by the number of ways to relabel a representative while preserving it, must equal the number of distinct labeled copies in that class. This is a precise balancing condition: it forces the mass of a class to be the reciprocal of the size of its automorphism group, written 1/|Aut|. A class with two symmetries gets mass 1/2, one with three gets 1/3, and so on.

The uniform choice fails this rule. The machine-checked theorem uniformClassMass_not_gaugeCounting proves that for any bound B of at least 2, the uniform mass does not satisfy normalized gauge counting. The counterexample is the two-point class, which has two labeled copies and one relabeling witness, so its required mass is 1/2, not 1. This failure is not a gap in the proof; it is the point. The theorem shows that the invariance axioms alone, which allow the uniform mass, do not force the correct counting behavior.

The framework's library, a machine-checked collection of formal theorems, packages this result as a blocker certificate. It proves three facts together: the counting-defined mass satisfies the rule, the rule is equivalent to assigning 1/|Aut| to every class, and the uniform mass fails it. What remains open is a derivation of normalized gauge counting from richer ledger structure. The uniform class mass is therefore not a proposed physical law but a live decoy, one that the framework's own theorems eliminate.

/-- Uniform mass on quotient classes. This is the live decoy admitted by
the weaker invariance requirements. -/
def uniformClassMass {B : ℕ} : TriangulationClass B → ℝ :=
  fun _ => 1

/-- The quotient-uniform decoy fails normalized gauge counting on the
two-point class, where the required mass is `1/2`. This proves that the
extra principle is discriminating and does not restate class invariance. -/
theorem uniformClassMass_not_gaugeCounting (B : ℕ) (hB : 2 ≤ B) :
    ¬ GaugeCountingPrinciple
      (uniformClassMass : TriangulationClass B → ℝ) := by
  intro h
  have hmu :=
    (gaugeCountingPrinciple_iff_mu_on_representatives
      (uniformClassMass : TriangulationClass B → ℝ)).mp h
      (MeasureInvarianceNoGo.twoPointComplex B hB)
  unfold uniformClassMass at hmu
  rw [MeasureInvarianceNoGo.mu_twoPointComplex B hB] at hmu
  norm_num at hmu

/-- **Certified blocker package.** Gauge counting exists and selects
`1/|Aut|`; the quotient-uniform decoy fails it. What remains is precisely a
ledger theorem supplying `GaugeCountingPrinciple`, not more invariance. -/
theorem substrate_measure_blocker_certificate (B : ℕ) (hB : 2 ≤ B) :
    GaugeCountingPrinciple
        (gaugeOrbitMass : TriangulationClass B → ℝ) ∧
      (∀ ν : TriangulationClass B → ℝ,
        GaugeCountingPrinciple ν ↔
          ∀ K : BoundedComplex B,
            ν (Quotient.mk (relabelSetoid B) K) = mu K) ∧
      ¬ GaugeCountingPrinciple
        (uniformClassMass : TriangulationClass B → ℝ) :=
  ⟨gaugeOrbitMass_satisfies,
    gaugeCountingPrinciple_iff_mu_on_representatives,
    uniformClassMass_not_gaugeCounting B hB⟩

What this page does not claim

This does not claim that uniform mass is the correct physical mass for any class. This does not claim that normalized gauge counting has been derived from first principles; that derivation remains open. This does not claim that the failure of uniform mass disproves the invariance axioms, only that those axioms do not select the counting rule.

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/MeasureSubstrateBlocker.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: