Gravity Seven Gaps Quotient First Z Mu Out Eq Of Mk Eq

A well-defined sum

In mathematics, a triangulation is a way of cutting a surface into triangles. These notes concern a sum over all triangulations of a given surface, where each triangulation contributes a number. A natural question is whether this sum is well-defined: if two triangulations are related by a relabeling of their vertices, they are considered the same object, but the sum must not accidentally count them twice or depend on the particular representative chosen.

The declaration mu_out_eq_of_mk_eq addresses exactly this. It states that if two triangulations are equivalent under relabeling, then a certain measure, written mu, assigns them the same value. In plain language, the measure is invariant under relabeling, so the sum over equivalence classes is well-defined. The proof is short: it uses the fact that the measure respects the equivalence relation, and the theorem is checked by the machine-checked library of formal theorems.

This is a foundational step, not a complete theory. The library explicitly records that the sum over classes is not unconditionally equal to the sum over labeled triangulations. A separate term, called the fiber excess, measures the difference, and it vanishes only under additional hypotheses. The declaration mu_out_eq_of_mk_eq does not prove that the quotient sum equals the labeled sum, nor does it establish an orbit-stabilizer theorem for the full set of triangulations. Those remain open targets, with the relevant status flags set to false.

What the theorem does give is a clean starting point. With a well-defined measure on equivalence classes, one can begin to ask meaningful questions about averages over triangulations, knowing that the answer does not depend on arbitrary choices. The next steps, such as deriving the measure from first principles or proving the missing orbit-stabilizer theorem, are precisely the open problems that this theorem makes it possible to state.

/-- The representative symmetry factor is independent of the chosen
representative of a triangulation class. -/
theorem mu_out_eq_of_mk_eq {B : ℕ} {K : BoundedComplex B}
    (q : TriangulationClass B) (hK : Quotient.mk (relabelSetoid B) K = q) :
    mu (Quotient.out q) = mu K := by
  exact mu_congr (PathSum.equivalent_of_mk_eq ((Quotient.out_eq q).trans hK.symm))

/-- **Exact relation.**  The labeled class-constant path sum is the
quotient-first path sum plus the labeled-fiber excess.  This is the honest
replacement for the killed unconditional claim `Z = Σ_q wq/|Aut q|`. -/
theorem labeledZ_eq_Zq_plus_fiberExcess (B : ℕ)
    (wq : TriangulationClass B → ℂ) :
    Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) =
      Zq B wq + fiberExcess B wq := by
  classical
  rw [labeledZ_eq_sum_fiberCard_mul_mu, Zq, fiberExcess, ← Finset.sum_add_distrib]
  refine Finset.sum_congr rfl fun q _ => ?_
  let f : ℂ := fiberCard (relabelSetoid B) q
  let m : ℂ := mu (Quotient.out q)
  let z : ℂ := wq q
  calc
    (((fiberCard (relabelSetoid B) q : ℂ) * (mu (Quotient.out q) : ℂ)) * wq q)
        = (f * m) * z := rfl
    _ = m * z + ((f - 1) * m) * z := by ring
    _ = (mu (Quotient.out q) : ℂ) * wq q +
        ((((fiberCard (relabelSetoid B) q : ℂ) - 1) *
          (mu (Quotient.out q) : ℂ)) * wq q) := rfl

What this page does not claim

This theorem does not prove that the quotient sum equals the labeled sum. This theorem does not establish an orbit-stabilizer theorem for the full bounded setoid. This theorem does not derive the measure mu from first principles.

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