Gravity Seven Gaps Measure Substrate Blocker Gauge Orbit Mass Satisfies

The gauge counting principle

In mathematics, when objects are grouped into classes by symmetry, a natural question is how to assign a number, a mass, to each class. The Recognition Science framework approaches this through a ledger, a discrete record of events, and asks what mass assignments are forced by basic consistency requirements. The theorem gaugeOrbitMass_satisfies establishes that a specific mass assignment, called gaugeOrbitMass, satisfies a principle known as normalized gauge counting.

Normalized gauge counting states a balance: the mass of a class, multiplied by the number of pairs consisting of a labeled copy and a relabeling witness, must equal the number of labeled copies in that class. The theorem proves this balance holds for gaugeOrbitMass. This mass assigns to each class the value one divided by the size of its automorphism group, the group of symmetries of a representative object. For example, a class whose objects each have two symmetries receives mass one half.

The theorem's significance is that this principle is not merely one option among many. A companion equivalence theorem shows that any mass assignment satisfying normalized gauge counting must equal gaugeOrbitMass. The framework's machine-checked library of formal theorems proves this uniqueness. The principle is discriminating: a simpler assignment that gives every class mass one fails the balance on a two-point class, where the required mass is one half. This shows the principle carries real content beyond mere symmetry invariance.

What the theorem does not claim is that normalized gauge counting itself is derived from more basic principles. The theorem takes the counting principle as a premise, a definitional choice within the framework. The framework's library identifies this premise as a remaining task, a substrate to be derived from richer ledger structure. The theorem certifies that if one accepts normalized gauge counting, then the mass assignment is forced, but it does not prove the principle from the ledger axioms alone.

/-- The counting-defined mass satisfies normalized gauge counting. -/
theorem gaugeOrbitMass_satisfies {B : ℕ} :
    GaugeCountingPrinciple (gaugeOrbitMass :
      TriangulationClass B → ℝ) :=
  gaugeOrbitMass_mul_pairCount

/-- The exact extra principle used by the gauge-counting derivation: class
mass times gauge-witness volume equals labeled orbit size. -/
def GaugeCountingPrinciple {B : ℕ}
    (ν : TriangulationClass B → ℝ) : Prop :=
  ∀ c, ν c * (pairCountClass c : ℝ) = (orbitCardClass c : ℝ)

/-- Normalized gauge counting selects exactly the counting-defined mass.
This packages existence and uniqueness in one equivalence. -/
theorem gaugeCountingPrinciple_iff_eq_gaugeOrbitMass {B : ℕ}
    (ν : TriangulationClass B → ℝ) :
    GaugeCountingPrinciple ν ↔ ν = gaugeOrbitMass := by
  constructor
  · intro hν
    funext c
    exact gaugeCountingMass_unique ν hν c
  · intro hν
    subst hν
    exact gaugeOrbitMass_satisfies

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

What this page does not claim

The theorem does not derive the normalized gauge counting principle from the ledger axioms; it takes the principle as a premise. The theorem does not assign physical mass to any specific particle or object; it concerns abstract symmetry classes of triangulated spaces. The theorem does not prove that the uniform mass assignment is the only alternative; it only shows it fails the counting principle.

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: