Gravity Seven Gaps Exact Shell Gauge Preflight Status Measure Derived

The measure, derived

In discrete gravity, one often sums over many similar geometric objects, and must decide how much each one contributes. A standard convention gives each object a weight of 1 divided by the size of its symmetry group, written 1/|Aut|. The declaration status_measure_derived records that this convention has been derived from a more basic idea: counting labeled copies and gauge witnesses.

The derivation starts with two countable quantities. The first, gaugeOrbitCard, counts how many labeled complexes are equivalent to a given one by relabeling. The second, pairCount, counts pairs consisting of an equivalent complex and a concrete relabeling witness. The ratio of these two numbers defines a mass for each equivalence class. A theorem proves this ratio equals the standard 1/|Aut| factor, using the orbit-stabilizer theorem: the witnesses form a torsor over the automorphism group, so their count factorizes as the orbit size times the group size.

This derivation rests on one explicit premise, the counting principle: each labeled copy and witness pair carries equal weight. The framework does not claim this principle follows from the ledger cost function. A flag, counting_principle_derived_from_ledger, remains false, and a separate theorem shows the cost route cannot supply label indifference. The measure is derived from the counting principle, not from the ledger.

What the declaration does not claim is as important as what it does. It does not establish that the counting principle is a physical law. It does not claim the measure applies outside the discrete-gravity setting. And it does not claim the ledger cost function forces the symmetry factor. The derivation is a mathematical consequence of a chosen premise, not an independent physical fact.

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

What this page does not claim

The counting principle is not derived from the ledger cost function. The measure is not claimed to be a physical law independent of the counting principle. The declaration does not claim the measure applies outside the discrete-gravity setting.

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: