Gravity Seven Gaps Exact Shell Gauge Preflight Relabeling Count Eq Aut Card

The relabeling count

In discrete approaches to quantum gravity, one often sums over geometric objects such as triangulations, which are networks of vertices, edges, and triangles glued together. A central question is how to count these objects when many of them are physically the same, differing only in how their parts are labeled. The theorem relabelingCount_eq_autCard addresses this by establishing a precise relationship between two counts: the number of ways to relabel one object to match another, and the size of the object's own symmetry group, known as its automorphism group.

For two equivalent objects, the theorem proves that the number of relabelings from the first to the second is exactly equal to the number of symmetries of the first. This is a standard result in mathematics, often called the orbit-stabilizer theorem, and it holds here in a fully machine-checked form. The consequence is that when one counts pairs consisting of a copy of an object and a concrete relabeling, the total factorizes into the number of distinct copies times the size of the symmetry group. This factorization is what allows a measure on classes of objects to be expressed as one over the size of the automorphism group, a factor familiar from Feynman diagram calculations.

The theorem is proved without any new axioms, and it does not assume the symmetry factor as a postulate. Instead, it derives that factor from a more basic counting principle, which is itself a model choice: that each copy and relabeling pair carries equal weight. The theorem shows that, given this principle, the one-over-automorphism-group measure follows necessarily. It also shows that this measure is unique: any measure satisfying the same counting property must equal it.

What the theorem does not claim is that this counting principle is itself derived from deeper physics. Whether the principle follows from the ledger cost function, the framework's foundational structure, remains an open question. The machine-checked status explicitly marks this as not proved. The theorem's power is conditional: it shows what follows from a stated premise, not that the premise is forced.

/-- **THEOREM (orbit-stabilizer, cardinal form).**  For equivalent
complexes, the witness count equals the automorphism count. -/
theorem relabelingCount_eq_autCard {K K' : BoundedComplex B}
    (h : Equivalent K K') : relabelingCount K K' = Nat.card (Aut K) := by
  obtain ⟨r0⟩ := h
  unfold relabelingCount
  exact (Nat.card_congr (torsorEquiv r0)).symm

/-- **Grounding theorem.**  The status flags are backed by the actual
theorems: orbit-stabilizer, pair-count factorization, the derivation
`gaugeOrbitMass = mu`, and uniqueness. -/
theorem gaugePreflight_grounded (B : ℕ) :
    (∀ K K' : BoundedComplex B, Equivalent K K' →
        relabelingCount K K' = Nat.card (Aut K)) ∧
    (∀ K : BoundedComplex B,
        pairCount K = gaugeOrbitCard K * Nat.card (Aut K)) ∧
    (∀ K : BoundedComplex B,
        gaugeOrbitMass (Quotient.mk (relabelSetoid B) K) = mu K) ∧
    (∀ ν : TriangulationClass B → ℝ,
        (∀ c, ν c * (pairCountClass c : ℝ) = (orbitCardClass c : ℝ)) →
        ∀ c, ν c = gaugeOrbitMass c) :=
  ⟨fun _ _ h => relabelingCount_eq_autCard h,
   pairCount_eq_orbitCard_mul_autCard,
   gaugeOrbitMass_eq_mu,
   gaugeCountingMass_unique⟩

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

What this page does not claim

The counting principle is not derived from the ledger cost function. The theorem does not apply to objects that are not equivalent under relabeling. The theorem does not compute the size of any specific automorphism group.

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: