Gravity Seven Gaps Exact Shell Gauge Preflight Gauge Preflight Grounded

What the preflight proves

In discrete gravity, one often sums over triangulations of space, and a standard convention divides each contribution by the size of its symmetry group, written 1/|Aut|. The declaration gaugePreflight_grounded is a machine-checked theorem in the Recognition Science library that derives this factor from a more basic counting idea, rather than postulating it. The derivation is a piece of pure combinatorics: it counts labeled copies of a complex and the relabelings between them, and shows that the ratio of these two counts is exactly 1/|Aut|.

The counting works as follows. For a given triangulation K, the orbit size counts how many distinct labeled complexes are equivalent to K by relabeling. The pair count counts all pairs (K', r) where K' is in that orbit and r is a concrete relabeling from K to K'. The theorem proves that the number of relabelings between two equivalent complexes equals the number of symmetries of either one, a standard orbit-stabilizer result. Consequently, the pair count factorizes as the orbit size times |Aut|, and the ratio orbit size divided by pair count simplifies to 1/|Aut|. This is the measure the framework calls mu, and the theorem states that the counting-defined mass equals mu for every class.

The theorem also proves uniqueness: any mass assignment that satisfies the counting property, where mass times pair count equals orbit size, must be exactly this one. This pins down the measure as the unique solution to the counting principle. A corollary rewrites the labeled path sum as a sum over equivalence classes, each weighted by orbit size times the counting mass, which is the form used in subsequent gravity calculations.

What the theorem does not claim is just as important. The counting principle itself, the choice that each labeled copy carries equal weight and that physical mass is labeled copies divided by gauge volume, is a MODEL premise, not a derived result. The framework's own status flag for this premise is explicitly false: the counting principle is not derived from the ledger cost function, and a separate theorem proves that the cost route cannot supply it. The derivation is therefore conditional, and the flag remains false on purpose.

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

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

/-- 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 theorem does not derive the counting principle from the ledger cost function. The theorem does not prove that the 1/|Aut| measure is physically correct, only that it follows from the stated counting premise. The theorem does not compute any numerical values or make contact with measured physical constants.

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: