Encyclopedia Gravity Gravity Seven Gaps Quotient First Z Zq Eq Labeled Z Iff Fiber Excess Vanishes

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Quotient First Z Zq Eq Labeled Z Iff Fiber Excess Vanishes

A machine-checked theorem settles when two different ways of counting paths in a triangulation agree, and it is honest about when they do not.

Verify this page

Two ways to sum a path

In the Recognition Science framework's study of gravity, physicists sum over triangulations: discrete grids of triangles that approximate a curved space. There are two natural conventions for this sum. The first, called the quotient-first sum, groups triangulations into classes that are the same up to relabeling, and counts each class once, weighted by a symmetry factor. The second, the standing labeled sum, counts every labeled triangulation individually. The theorem Zq_eq_labeledZ_iff_fiberExcess_vanishes states the exact condition under which these two sums agree: they are equal precisely when a quantity called the fiber excess is zero.

The fiber excess is not an abstract invention. It is the explicit difference between the two sums, written as a sum over classes of (|fiber q| - 1) times a measure times a weight. Here |fiber q| is the number of labeled triangulations that map to the same class q. The theorem proves that the quotient-first sum equals the labeled sum if and only if this excess vanishes. A companion theorem shows a sufficient condition: if every fiber has exactly one element, the sums agree. But the framework's own library proves this condition is false in general: there exist classes with more than one labeled representative.

The theorem is a replacement for a stronger claim that was tried and rejected. An earlier panel killed the unconditional statement that the labeled sum equals a per-class sum with a 1/|Aut| symmetry factor. This file does not resurrect that claim by convention. Instead, it proves the exact relation: the labeled sum equals the quotient-first sum plus the fiber excess. The iff form is the honest boundary of what is known.

What the theorem does not claim is as important as what it proves. It does not derive an orbit-stabilizer theorem for the full bounded setoid of triangulation classes, and no such global relabeling group action is supplied in this wave. The 1/|Aut| measure remains a model input, not a derived result. The theorem also does not claim the two sums are equal in general; it gives the precise condition for equality, and the framework's own results show that condition fails in concrete cases.

THEOREM Zq_eq_labeledZ_iff_fiberExcess_vanishes · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
Zq_eq_labeledZ_iff_fiberExcess_vanishes · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:128 
/-- **IFF form of the exact relation.**  The quotient-first object equals
the standing labeled sum for a pulled-back class weight exactly when the
explicit fiber excess vanishes. -/
theorem Zq_eq_labeledZ_iff_fiberExcess_vanishes (B : ℕ)
    (wq : TriangulationClass B → ℂ) :
    Zq B wq = Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) ↔
      fiberExcess B wq = 0 := by
  rw [labeledZ_eq_Zq_plus_fiberExcess]
  constructor
  · intro h
    have h' : Zq B wq + fiberExcess B wq = Zq B wq + 0 := by
      simpa using h.symm
    exact add_left_cancel h'
  · intro h
    rw [h, add_zero]
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 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 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 theorem does not prove an orbit-stabilizer theorem for the full bounded setoid of triangulation classes. The theorem does not claim the two sums are equal in general. The theorem does not derive the 1/|Aut| measure; it remains a model input.

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