Gravity Seven Gaps Exact Shell Gauge Preflight Gauge Orbit Mass Mul Pair Count

The gauge mass identity

In discrete gravity, one often assigns to each triangulation a weight of 1 divided by the size of its automorphism group, the group of relabelings that leave the complex unchanged. That factor, the symmetry factor, corrects for overcounting when summing over labeled complexes. In the Recognition Science framework's machine-checked library of formal theorems, the declaration gaugeOrbitMass_mul_pairCount proves that this factor is not an ad hoc convention but follows from a counting principle.

The theorem states a simple identity. For any equivalence class of triangulations under relabeling, the gauge orbit mass, defined as the number of labeled copies in the class divided by the pair count, times the pair count, equals the number of labeled copies. The pair count is the number of pairs consisting of a labeled complex in the class and a concrete relabeling witness connecting it to a reference complex. This identity, gaugeOrbitMass times pairCount equals orbitCard, is proved in Lean with no axioms beyond the standard three. It is the key step in showing that the counting-defined mass equals the symmetry factor 1 divided by the size of the automorphism group.

The theorem does not claim that the counting principle itself is derived from deeper physics. The principle, that each labeled copy and witness pair carries equal weight, is a named premise of the module. The framework's own status flag for deriving this principle from the ledger cost function is set to false. What the theorem proves is conditional: given that principle, the symmetry factor follows by orbit-stabilizer counting. The theorem also does not claim that the pair count carries information about the incidence structure of the complex; a separate premise identifies it as the order of the relabeling group of the size sector.

What the identity changes is the status of the symmetry factor in this framework. It becomes a derived consequence of a stated counting principle rather than a postulate. The uniqueness theorem that accompanies it shows that any class mass satisfying the counting property must equal the gauge orbit mass, so the counting principle pins the measure completely. This gives a clean foundation for the path-sum formula, where the labeled sum over complexes equals a weighted sum over classes.

/-- **THEOREM (existence).**  `gaugeOrbitMass` itself satisfies the
normalized gauge-divided counting property; together with
`gaugeCountingMass_unique` this pins the measure (existence + uniqueness,
not uniqueness alone). -/
theorem gaugeOrbitMass_mul_pairCount (c : TriangulationClass B) :
    gaugeOrbitMass c * (pairCountClass c : ℝ) = (orbitCardClass c : ℝ) := by
  have hp : (pairCountClass c : ℝ) ≠ 0 := by
    exact_mod_cast (pairCountClass_pos c).ne'
  unfold gaugeOrbitMass
  rw [div_mul_cancel₀ _ hp]

/-- **THEOREM (the derivation).**  The counting-defined class mass equals
the postulated symmetry-factor measure: GIVEN the pair-counting principle,
`1/|Aut|` follows from orbit-stabilizer (`pairCount = orbitCard * |Aut|`)
rather than being written into the definition. -/
theorem gaugeOrbitMass_eq_mu (K : BoundedComplex B) :
    gaugeOrbitMass (Quotient.mk (relabelSetoid B) K) = mu K := by
  have ho : (gaugeOrbitCard K : ℝ) ≠ 0 := by
    exact_mod_cast (gaugeOrbitCard_pos K).ne'
  unfold gaugeOrbitMass mu
  rw [orbitCardClass_mk, pairCountClass_mk, pairCount_eq_orbitCard_mul_autCard,
    Nat.cast_mul, div_mul_eq_div_div, div_self ho]

/-- OPEN (retracted 2026-07-26): the counting principle remains this
module's named premise and is not derived from the ledger. -/
theorem status_counting_principle_open :
    gaugePreflightStatus.counting_principle_derived_from_ledger = false := rfl

What this page does not claim

The counting principle is not derived from the ledger cost function or any deeper principle within the framework. The pair count does not depend on the incidence structure of the triangulation; it is fixed by the size sector alone. The theorem does not compute any numerical value for the gauge orbit mass or pair count.

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