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

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Quotient First Z Labeled Z Eq Zq Plus Fiber Excess

A machine-checked theorem pins down the precise difference between two ways of summing over triangulations, and it refuses to paper over that difference.

Verify this page

The exact excess

In the Recognition Science framework's study of gravity, physicists need to add up contributions from many triangulations, the discrete building blocks of a curved space. There are two natural ways to organize this sum. The first, called the labeled path sum, treats each triangulation as a distinct object and adds its contribution directly. The second, the quotient-first path sum, groups triangulations into classes that are the same up to relabeling, then adds one term per class, weighted by a symmetry factor. The question is whether these two procedures give the same answer.

The theorem labeledZ_eq_Zq_plus_fiberExcess, proved in the framework's machine-checked library of formal theorems, gives the exact relationship. It states that the labeled path sum equals the quotient-first sum plus an explicit correction term, the fiber excess. That excess is a sum over classes of (|fiber q| - 1) times the measure times the weight, where |fiber q| counts how many distinct labeled triangulations sit inside the class q. If every class contained exactly one labeled triangulation, the excess would vanish and the two sums would agree. But the framework's own earlier results show this is not generally true: some classes contain more than one labeled triangulation, so the excess is generally nonzero.

This theorem matters because it replaces an earlier, unconditional claim that the two sums were equal. That claim was rejected by the framework's own review process. The new result is the honest replacement: it does not assert equality, it computes the difference. The framework models the quotient-first sum as the primary object, and the labeled sum as the quotient sum plus a correction. The correction is not assumed away; it is written down explicitly and kept as part of the bridge between the two conventions.

The theorem does not claim that the fiber excess is zero, and it does not claim that the two sums are equal in general. It also does not derive a general orbit-stabilizer theorem for the full bounded set of triangulation classes, which would be one way to simplify the excess. Those remain open targets. What the theorem does establish is a precise, checkable identity, one that keeps the framework honest about the gap between its two summation conventions.

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 fiberExcess · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
fiberExcess · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:99 
/-- The explicit excess by which the labeled class pushforward differs
from the quotient-first object.  It is zero only under additional
fiber/weight cancellation hypotheses; no such cancellation is assumed. -/
noncomputable def fiberExcess (B : ℕ) (wq : TriangulationClass B → ℂ) : ℂ :=
  ∑ q : TriangulationClass B,
    ((((fiberCard (relabelSetoid B) q : ℂ) - 1) * (mu (Quotient.out q) : ℂ))
      * wq q)
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 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 fiber excess is zero in general. The labeled and quotient-first sums are equal without extra conditions. A general orbit-stabilizer theorem for the full bounded setoid is derived here.

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