Gravity Seven Gaps Class Pushforward Class Mass Eq Fiber Card Mul Mu

The class mass identity

In mathematics, when you want to sum a function over a large collection, it is often useful to group the collection into classes of objects that are considered equivalent. The quotient is the set of these classes. A basic question is how to express the total sum over all objects in terms of a sum over the classes. The answer, when the function is constant on each class, is a simple identity: the total sum equals the sum over classes of the number of objects in that class, multiplied by the function's value on any representative of the class.

This identity is what the Recognition Science declaration classMass_eq_fiberCard_mul_mu establishes, in a specific setting. The setting involves a finite collection of labeled complexes, which are grouped into classes by relabeling. The declaration states that for any such class q, the class mass, which is the sum of the measure mu over all complexes in the class, is equal to the number of complexes in that class (the fiber cardinality) multiplied by the measure of a chosen representative. In symbols, classMass q = fiberCard q * mu (rep q). This is a proved theorem, not a definition or a choice.

The importance of this identity is that it clarifies a potential ambiguity. A naive guess might be that the class mass is simply the measure of a representative, or perhaps that it is the measure divided by the number of symmetries of the representative. The theorem shows the correct formula includes the full count of objects in the class. The pack even exhibits a concrete case at B = 2 where two distinct labeled complexes are equivalent under relabeling, so the fiber has cardinality greater than one, and the class mass is strictly larger than the measure of either single complex. This confirms that the fiber cardinality factor is not optional.

In the framework's own usage, this identity is the backbone of how a certain path sum Z is decomposed into a sum over classes. The declaration Z_eq_classPushforward uses it to rewrite the total labeled sum as a sum over classes, each weighted by the class mass. This is a structural fact about how the sum is organized. It is not a statement about any particular physical value, nor does it imply anything about a continuum limit or about the origin of the measure mu itself.

What the declaration does not claim is as important as what it does. It does not claim that the class mass is simply 1/|Aut| per class; the fiber cardinality is an essential multiplier. It does not apply to a different, quotient-first convention where a path sum is defined directly on classes with per-class weights; the pack explicitly notes these are different conventions, not a contradiction. It does not derive the measure mu from any invariance principle; the 1/|Aut| convention is a model input. And it makes no claim about a continuum limit or about bridging to other gaps in the framework; those remain open targets.

/-- **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

/-- **T3 FORK VERDICT (non-singleton fiber; C1 landmine detonated).**
There exist two distinct labeled complexes that are equivalent: the
quotient fibers of `TriangulationClass` are NOT all singletons, so the
labeled pushforward mass `classMass = |fiber| · (1/|Aut|)` genuinely
differs from the per-class `1/|Aut|` weight.  Explicit witness at
`B = 2`. -/
theorem exists_nonSingleton_fiber :
    ∃ K K' : BoundedComplex 2, K ≠ K' ∧ Equivalent K K' :=
  ⟨edgeAB, edgeBA, edgeAB_ne_edgeBA, ⟨edgeSwapRelabel⟩⟩

/-- **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)

/-- **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]

What this page does not claim

This identity does not claim the class mass is simply 1/|Aut| per class; the fiber cardinality is an essential multiplier. This identity does not apply to the quotient-first convention where a path sum is defined directly on classes with per-class 1/|Aut| weights. This identity does not derive the measure mu from any invariance principle; the 1/|Aut| convention is 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/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: