Gravity Seven Gaps Exact Shell Gauge Preflight Gauge Counting Mass Unique

The counting principle

In discrete gravity, a spacetime is often built from labeled building blocks, such as triangles glued into a complex. Many labelings describe the same physical geometry, so a path sum over labeled complexes overcounts. The standard fix is to divide by the size of each complex's symmetry group, the automorphism group, writing the weight as 1/|Aut|. That factor has usually been put in by hand as a convention.

The framework's machine-checked library of formal theorems instead derives that factor from a counting principle. The derivation starts with two plain quantities. The first, orbitCard, counts how many labeled complexes are equivalent to a given one, its relabeling orbit. The second, pairCount, counts pairs of a complex in that orbit together with a concrete relabeling witness, the gauge volume of the orbit. The gauge mass of a class is then defined as labeled copies per unit of gauge volume, orbitCard divided by pairCount.

The key theorem, gaugeCountingMass_unique, proves that any class mass satisfying the counting property, mass times pairCount equals orbitCard, must equal that quotient. In other words, the counting principle pins the measure uniquely. A companion theorem, gaugeOrbitMass_eq_mu, shows that this counting-defined mass equals the conventional 1/|Aut| factor. The derivation rests on orbit-stabilizer: for equivalent complexes, the relabeling witnesses form a torsor over the automorphism group, so pairCount factorizes as orbitCard times |Aut|.

In Recognition Science, this means the symmetry factor is not an extra assumption but a consequence of a more basic choice: that gauge volume is the (copy, witness) pair count. The counting principle itself remains a model premise, not a derived fact. A different premise, such as per-labeled-copy weighting, would give a different measure. The library's status flag for deriving the counting principle from the ledger cost function stays false on purpose, and a separate theorem shows the cost route cannot supply it.

What the theorem does not claim is that the counting principle is forced by deeper physics. It proves a conditional: given the counting principle, the 1/|Aut| measure follows uniquely. The principle's justification, label indifference, is a modeling choice about how to weight labeled configurations, not a consequence of the cost function. The path-sum corollary shows the payoff: for any relabeling-invariant weight, the labeled path sum equals a sum over classes weighted by orbitCard times gauge mass, giving a clean way to compute without overcounting.

/-- **THEOREM (uniqueness).**  Any class-mass assignment satisfying the
normalized gauge-divided counting property (`ν c * pairCount c =
orbitCard c` for every class) equals `gaugeOrbitMass`.  Given the counting
principle (the explicit MODEL premise of this module), the measure is
unique; combined with `gaugeOrbitMass_eq_mu`, it is forced to be
`1/|Aut|`. -/
theorem gaugeCountingMass_unique (ν : TriangulationClass B → ℝ)
    (hν : ∀ c, ν c * (pairCountClass c : ℝ) = (orbitCardClass c : ℝ))
    (c : TriangulationClass B) : ν c = gaugeOrbitMass c := by
  have hp : (pairCountClass c : ℝ) ≠ 0 := by
    exact_mod_cast (pairCountClass_pos c).ne'
  unfold gaugeOrbitMass
  rw [eq_div_iff hp]
  exact hν c

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

/-- **THEOREM (pair-count factorization).**  The gauge volume of the orbit
is the orbit size times the automorphism count: every fiber of the
projection `(K', r) ↦ K'` is a torsor over `Aut K`. -/
theorem pairCount_eq_orbitCard_mul_autCard (K : BoundedComplex B) :
    pairCount K = gaugeOrbitCard K * Nat.card (Aut K) := by
  have e : (Σ K' : {K' : BoundedComplex B // Equivalent K K'}, Relabel K K'.val)
      ≃ {K' : BoundedComplex B // Equivalent K K'} × Aut K :=
    Equiv.sigmaEquivProdOfEquiv fun K' =>
      (torsorEquiv (Classical.choice K'.property)).symm
  unfold pairCount gaugeOrbitCard
  rw [Nat.card_congr e, Nat.card_prod]

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

/-- 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; it is a named model premise. The theorem does not prove that the 1/|Aut| factor is physically necessary, only that it follows from the counting principle. The derivation does not compute any cardinalities numerically; it works symbolically with finite types.

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: