Encyclopedia Gravity Gravity Seven Gaps Quotient First Z Zq Eq Labeled Z Of Singleton Fibers

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Quotient First Z Zq Eq Labeled Z Of Singleton Fibers

A formal theorem pins down exactly when two different ways of summing over triangulations agree, and the answer is a simple condition on symmetry classes.

Verify this page

The singleton-fiber bridge

In the Recognition Science framework's study of gravity, two different sums over triangulations appear. One sum, the labeled path sum, adds a contribution for every individual triangulation. The other, the quotient-first path sum, first groups triangulations into symmetry classes and then adds one contribution per class, weighted by a symmetry factor. The theorem Zq_eq_labeledZ_of_singleton_fibers states a precise condition under which these two sums are equal: when every symmetry class contains exactly one triangulation, the two sums agree.

The condition is called the singleton-fiber condition. A fiber here is the set of triangulations that belong to the same symmetry class. When each fiber has size one, the quotient-first sum and the labeled sum give the same result. The theorem is proved in the machine-checked library of formal theorems, and it follows from a more general exact relation: the labeled sum always equals the quotient-first sum plus an explicit excess term that measures the contribution of classes with more than one member. When that excess is zero, the two sums coincide.

The theorem does not claim the two sums are equal in general. In fact, the library also contains a proof that non-singleton fibers exist: for a specific triangulation class, the fiber has more than one element. This is why the unconditional equality was abandoned. The quotient-first object is a definitional choice, a model of how to sum over classes, and the per-class symmetry factor is an input to that model, not a derived result.

What the theorem changes is the status of the bridge between the two summation conventions. Instead of an unconditional equality, the framework now has a precise, provable condition for when the bridge holds. This makes the relationship between the labeled and quotient-first sums explicit and auditable, and it marks clearly where further work would be needed to connect them in the general case.

THEOREM Zq_eq_labeledZ_of_singleton_fibers · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
Zq_eq_labeledZ_of_singleton_fibers · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:144 
/-- A sufficient singleton-fiber condition under which the quotient-first
object agrees with the labeled sum.  `ClassPushforward` proves this
condition is false in general (`PathSum.one_lt_fiberCard_edgeClass`). -/
theorem Zq_eq_labeledZ_of_singleton_fibers (B : ℕ)
    (wq : TriangulationClass B → ℂ)
    (hfiber : ∀ q : TriangulationClass B,
      fiberCard (relabelSetoid B) q = 1) :
    Zq B wq = Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) := by
  rw [Zq_eq_labeledZ_iff_fiberExcess_vanishes]
  unfold fiberExcess
  refine Finset.sum_eq_zero fun q _ => ?_
  rw [hfiber q]
  norm_num
THEOREM labeledZ_eq_Zq_plus_fiberExcess · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
labeledZ_eq_Zq_plus_fiberExcess · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:107 
/-- **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
THEOREM quotientFirstStatus_grounded · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
quotientFirstStatus_grounded · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:189 
/-- **Grounding theorem.**  The status flags are tied to the constructed
object and kernel bridges.  The RED flags remain false, and the inherited
non-singleton fiber theorem records why the unconditional labeled/quotient
equality is not available. -/
theorem quotientFirstStatus_grounded :
    (quotientFirstStatus.quotient_first_object_constructed = true ∧
      ∀ B : ℕ, ∀ wq : TriangulationClass B → ℂ,
        Zq B wq = ∑ q : TriangulationClass B,
          (mu (Quotient.out q) : ℂ) * wq q) ∧
    (quotientFirstStatus.labeled_bridge_has_fiber_factor = true ∧
      ∀ B : ℕ, ∀ wq : TriangulationClass B → ℂ,
        Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) =
          ∑ q : TriangulationClass B,
            (((fiberCard (relabelSetoid B) q : ℂ) * (mu (Quotient.out q) : ℂ))
              * wq q)) ∧
    (quotientFirstStatus.exact_excess_relation_proved = true ∧
      ∀ B : ℕ, ∀ wq : TriangulationClass B → ℂ,
        Zq B wq = Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) ↔
          fiberExcess B wq = 0) ∧
    (quotientFirstStatus.nonSingleton_fiber_inherited = true ∧
      1 < fiberCard (relabelSetoid 2)
        (Quotient.mk (relabelSetoid 2) PathSum.edgeAB)) ∧
    quotientFirstStatus.bounded_orbit_stabilizer_derived = false ∧
    quotientFirstStatus.Z_RS_continuum_limit = false ∧
    quotientFirstStatus.substrate_measure_derived = false ∧
    quotientFirstStatus.gap1_bridge_derived = false :=
  ⟨⟨rfl, fun _ _ => rfl⟩,
    ⟨rfl, labeledZ_eq_sum_fiberCard_mul_mu⟩,
    ⟨rfl, Zq_eq_labeledZ_iff_fiberExcess_vanishes⟩,
    ⟨rfl, PathSum.one_lt_fiberCard_edgeClass⟩,
    rfl, rfl, rfl, rfl⟩

What this page does not claim

The two sums are equal in general, without any condition on fibers. The per-class symmetry factor is derived from a more basic principle; it is a model input. A full orbit-stabilizer theorem for the bounded triangulation class setoid is proved.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND