Gravity Seven Gaps Measure Substrate Blocker Gauge Counting Principle Iff Eq Gau

The gauge-counting equivalence

In the framework's account of gravity, physical quantities are built from classes of labeled objects, where two labels are equivalent if a relabeling connects them. A central question is how to assign a mass to each such class. The declaration gaugeCountingPrinciple_iff_eq_gaugeOrbitMass establishes a precise equivalence: a class mass satisfies normalized gauge counting if and only if it equals the gauge orbit mass, which assigns to each class the reciprocal of the size of its automorphism group, written 1 / |Aut|. The forward direction is a derivation from the orbit-stabilizer theorem; the reverse direction shows that no weaker unnamed condition hides inside the counting statement.

The principle itself is a definitional choice, not a proved consequence. It states that for every class, the class mass times the number of (labeled copy, relabeling witness) pairs equals the number of labeled copies. The theorem proves that this principle selects exactly one mass assignment: the one that gives each class a mass of 1 / |Aut|. The proof is machine-checked in the framework's library of formal theorems, with no unproved assumptions added.

The result has real content because a natural alternative fails. The uniform class mass, which assigns mass 1 to every class, satisfies the weaker invariance requirements but violates normalized gauge counting on the two-point class, where the required mass is 1/2. This shows the principle is discriminating and does not merely restate class invariance. The theorem therefore certifies a blocker: the remaining substrate task cannot be discharged by the invariance axioms or by renaming uniform quotient counting. It requires a derivation of normalized gauge counting from richer ledger structure, which remains open.

What the declaration does not claim is as important as what it proves. It does not prove that normalized gauge counting itself holds; it proves an equivalence between that principle and a specific mass assignment. The principle remains a MODEL premise, awaiting derivation from deeper structure. The theorem also does not claim that the uniform class mass is the correct assignment; it proves the opposite, that uniform mass fails the principle. The result is a sharp boundary marker, not a completed derivation.

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

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

What this page does not claim

The theorem does not prove that normalized gauge counting actually holds. The uniform class mass is not claimed to be correct; it is proved to fail the principle. The result does not derive the gauge orbit mass from deeper ledger structure.

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: