Encyclopedia Gravity Gravity Seven Gaps Class Pushforward Sum Eq Quotient Sum Class Mass

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Class Pushforward Sum Eq Quotient Sum Class Mass

A theorem about summing over equivalence classes shows how a labeled sum can be rewritten as a sum over classes, with a weight that counts how many labels collapse into each class.

Verify this page

The class pushforward sum

In mathematics, when you group objects into equivalence classes, you often want to rewrite a sum over all objects as a sum over the classes. The theorem sum_eq_quotient_sum_classMass in the framework's machine-checked library of formal theorems proves this can be done cleanly. For any finite set with an equivalence relation, and any function that assigns the same value to equivalent objects, the sum over all objects equals the sum over classes, where each class contributes the number of objects in it times the function's value on a representative. This is a general bookkeeping fact: it requires no group structure, only the basic notion of a quotient set.

This generic theorem is then applied to a specific case in the framework's gravity work. There, the objects are labeled simplicial complexes representing discrete geometries, and the equivalence relation identifies complexes related by relabeling their vertices. The function classMass (the total weight of a class) is defined as the sum of the measures of all complexes in that class. The theorem Z_eq_classPushforward then shows that the framework's partition function, a sum over all labeled complexes, can be rewritten as a sum over relabeling classes, with each class weighted by its classMass.

The key subtlety, and the main thing the theorem clarifies, is what this classMass weight actually is. A separate theorem proves that classMass equals the number of complexes in the class times a symmetry factor of 1/|Aut|, where |Aut| is the size of the automorphism group of a representative. This is not simply 1/|Aut| per class. The theorem mu_lt_classMass_edgeClass demonstrates this difference concretely: for a simple two-vertex complex, the measure of a single labeled complex is strictly less than the classMass of its class, because the class contains two distinct labeled complexes that are related by swapping the vertices. This shows the labeled sum and a sum over inequivalent classes with only 1/|Aut| weights are genuinely different objects, even in the simplest case.

In Recognition Science, this distinction matters because it pins down which convention the framework's partition function uses. The theorem proves that the labeled sum carries the full fiber cardinality weight, not just the symmetry factor. It does not claim that this is the only possible convention. The framework explicitly records that a quotient-first object, defined directly on classes with per-class 1/|Aut| weights, is a model for future work, not something constructed here. The theorem also does not claim anything about a continuum limit, nor does it derive the 1/|Aut| convention from more basic principles; those remain open targets.

THEOREM sum_eq_quotient_sum_classMass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
sum_eq_quotient_sum_classMass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean:126 
/-- **THEOREM (T1, class-constant collapse).**  If `f` is constant on
classes (mk-equality hypothesis), the fiber sum collapses:
`Σ_{a : α} f a = Σ_{q} fiberCard(q) • f (rep q)` where `rep q = q.out`. -/
theorem sum_eq_quotient_sum_classMass {α : Type*} [Fintype α] (s : Setoid α)
    {M : Type*} [AddCommMonoid M] (f : α → M)
    (hf : ∀ a b, Quotient.mk s a = Quotient.mk s b → f a = f b) :
    ∑ a : α, f a = ∑ q : Quotient s, fiberCard s q • f (Quotient.out q) := by
  rw [sum_fiberwise_quotient s f]
  refine Finset.sum_congr rfl fun q _ => ?_
  have hconst : ∀ a ∈ classFiber s q, f a = f (Quotient.out q) := by
    intro a ha
    exact hf a (Quotient.out q)
      (((mem_classFiber s q a).mp ha).trans (Quotient.out_eq q).symm)
  rw [Finset.sum_congr rfl hconst, Finset.sum_const]
  rfl
THEOREM Z_eq_classPushforward · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
Z_eq_classPushforward · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean:179 
/-- **T2 (headline).**  For any weight `w` constant on classes (explicit
hypothesis `hw`; note `unitaryWeight S` is class-constant only when `S`
is), the labeled path sum `Z` equals its class pushforward:
`Z B w = Σ_{q : TriangulationClass B} classMass(q) · w(rep q)`.
HONEST SCOPE: `classMass q = |fiber(q)| · (1/|Aut(rep q)|)`
(see `classMass_eq_fiberCard_mul_mu`), NOT `1/|Aut|` per class; this
theorem does NOT equate `Z` with the inequivalent-class sum with weights
`1/|Aut|` (the two weights are separated as a kernel fact by
`mu_lt_classMass_edgeClass`, built on `exists_nonSingleton_fiber`). -/
theorem Z_eq_classPushforward (B : ℕ) (w : BoundedComplex B → ℂ)
    (hw : ∀ K K', Equivalent K K' → w K = w K') :
    Z B w = ∑ q : TriangulationClass B,
      (classMass q : ℂ) * w (Quotient.out q) := by
  unfold Z
  rw [FiniteQuotient.sum_fiberwise_quotient (relabelSetoid B)
    (fun K => (mu K : ℂ) * w K)]
  refine Finset.sum_congr rfl fun q _ => ?_
  have hmem : ∀ K ∈ classFiber (relabelSetoid B) q, Equivalent K (Quotient.out q) := by
    intro K hK
    exact equivalent_of_mk_eq
      (((mem_classFiber (relabelSetoid B) q K).mp hK).trans (Quotient.out_eq q).symm)
  calc ∑ K ∈ classFiber (relabelSetoid B) q, (mu K : ℂ) * w K
      = ∑ K ∈ classFiber (relabelSetoid B) q, (mu K : ℂ) * w (Quotient.out q) := by
        refine Finset.sum_congr rfl fun K hK => ?_
        rw [hw K (Quotient.out q) (hmem K hK)]
    _ = (∑ K ∈ classFiber (relabelSetoid B) q, (mu K : ℂ)) * w (Quotient.out q) := by
        rw [← Finset.sum_mul]
    _ = (classMass q : ℂ) * w (Quotient.out q) := by
        unfold classMass
        rw [Complex.ofReal_sum]
THEOREM classMass_eq_fiberCard_mul_mu · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
classMass_eq_fiberCard_mul_mu · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean:165 
/-- **T3 (the fork detector, identity form).**  The pushforward class mass
is the labeled fiber cardinality times the symmetry factor of the class
representative: `classMass q = |fiber(q)| · μ(rep q)`.  Kernel-checked on
the actual carrier; uses `mu_congr` (μ is a class function). -/
theorem classMass_eq_fiberCard_mul_mu {B : ℕ} (q : TriangulationClass B) :
    classMass q = (fiberCard (relabelSetoid B) q : ℝ) * mu (Quotient.out q) := by
  unfold classMass
  have hconst : ∀ K ∈ classFiber (relabelSetoid B) q, mu K = mu (Quotient.out q) := by
    intro K hK
    exact mu_congr (equivalent_of_mk_eq
      (((mem_classFiber (relabelSetoid B) q K).mp hK).trans (Quotient.out_eq q).symm))
  rw [Finset.sum_congr rfl hconst, Finset.sum_const, nsmul_eq_mul]
  rfl
THEOREM mu_lt_classMass_edgeClass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
mu_lt_classMass_edgeClass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean:307 
/-- **T3 FORK VERDICT (numeric witness; the formalized detonation).**
At the `B = 2` edge class the labeled measure of a single representative
is STRICTLY BELOW the pushforward class mass:
`μ(edgeAB) < classMass(⟦edgeAB⟧)`.  Hence a path sum carrying weight
`classMass` per class is NOT the per-class `1/|Aut|` sum, as a kernel
fact (via `classMass_eq_fiberCard_mul_mu`, `one_lt_fiberCard_edgeClass`,
`mu_congr`, and `mu_pos`).  This concerns the LABELED `PathSum.Z` object
only. -/
theorem mu_lt_classMass_edgeClass :
    mu edgeAB < classMass (Quotient.mk (relabelSetoid 2) edgeAB) := by
  have hrep : mu (Quotient.out (Quotient.mk (relabelSetoid 2) edgeAB)) =
      mu edgeAB :=
    mu_congr (equivalent_of_mk_eq (Quotient.out_eq _))
  rw [classMass_eq_fiberCard_mul_mu, hrep]
  have hcard : (1 : ℝ) < (fiberCard (relabelSetoid 2)
      (Quotient.mk (relabelSetoid 2) edgeAB) : ℝ) := by
    exact_mod_cast one_lt_fiberCard_edgeClass
  calc mu edgeAB = 1 * mu edgeAB := (one_mul _).symm
    _ < _ * mu edgeAB := mul_lt_mul_of_pos_right hcard (mu_pos edgeAB)

What this page does not claim

The theorem does not prove that the 1/|Aut| convention is derived from invariance and normalization. The theorem does not apply to the exact-shell Z_RS_uv wave, which uses a different quotient-sum convention. The theorem does not establish any result about a continuum limit or convergence.

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/ClassPushforward.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