Encyclopedia Gravity Gravity Seven Gaps Class Pushforward

ARTICLE 5 claims 5 theorems

Gravity Seven Gaps Class Pushforward

Gravity's path sum can be reorganized by symmetry classes, and the framework proves exactly how the weights must be counted.

Verify this page

The class pushforward

In Recognition Science, the path sum Z is a bookkeeping tool: it adds up weights over all labeled complexes, which are discrete geometric objects built from vertices, edges, and tetrahedra. The class pushforward is a way of regrouping that sum. Instead of adding one term per labeled complex, it groups complexes into classes of objects that are related by relabeling, then adds one term per class. The framework's library proves that this regrouping is exact: for any weight function that assigns the same value to relabeled complexes, the original sum equals the sum over classes of the class mass times the weight of a representative complex.

The class mass is not simply the weight of one representative. The framework proves that class mass equals the number of labeled complexes in the class times the symmetry factor 1/|Aut|, where |Aut| is the size of the automorphism group of a representative. This distinction matters. At B = 2, the framework exhibits two distinct labeled complexes, edgeAB and edgeBA, which are related by swapping the two vertices. The theorem one_lt_fiberCard_edgeClass proves that the class containing edgeAB has more than one member, and mu_lt_classMass_edgeClass proves that the class mass is strictly greater than the weight of edgeAB alone. So the class decomposition of the path sum carries the factor |fiber| · (1/|Aut|), not just 1/|Aut|.

This is a kernel fact, not a prose claim. The framework's machine-checked library of formal theorems proves the generic fiber decomposition for any finite set with an equivalence relation, and the specific class pushforward for the path sum. The library also records what is not established: the quotient-first object with per-class 1/|Aut| weights is not constructed, no continuum limit is claimed, and the 1/|Aut| convention itself is a model input, not a derived result. The framework's honesty organ keeps these flags red.

The practical consequence is a precise accounting rule. When you regroup a path sum by symmetry classes, you must multiply each class's representative weight by the number of labeled complexes in that class. The framework proves this rule holds for any weight constant on classes, and it exhibits a concrete case where the distinction changes the answer. This is the kind of bookkeeping that prevents overcounting when passing from labeled objects to unlabeled ones.

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 exists_nonSingleton_fiber · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
exists_nonSingleton_fiber · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean:282 
/-- **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⟩⟩
THEOREM one_lt_fiberCard_edgeClass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
one_lt_fiberCard_edgeClass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean:292 
/-- **T3 FORK VERDICT (count form).**  The fiber of the one-edge class at
`B = 2` has labeled cardinality strictly greater than 1: both `edgeAB`
and `edgeBA` lie in it. -/
theorem one_lt_fiberCard_edgeClass :
    1 < fiberCard (relabelSetoid 2) (Quotient.mk (relabelSetoid 2) edgeAB) := by
  have hmemAB : edgeAB ∈ classFiber (relabelSetoid 2)
      (Quotient.mk (relabelSetoid 2) edgeAB) :=
    (mem_classFiber (relabelSetoid 2) _ edgeAB).mpr rfl
  have hmemBA : edgeBA ∈ classFiber (relabelSetoid 2)
      (Quotient.mk (relabelSetoid 2) edgeAB) :=
    (mem_classFiber (relabelSetoid 2) _ edgeBA).mpr
      (Quotient.sound ⟨edgeSwapRelabel.symm⟩)
  exact Finset.one_lt_card.mpr
    ⟨edgeBA, hmemBA, edgeAB, hmemAB, fun h => edgeAB_ne_edgeBA h.symm⟩
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 quotient-first object with per-class 1/|Aut| weights is not constructed in this module. No continuum limit or convergence claim is made for the path sum. The 1/|Aut| convention is a model input, not a derived theorem.

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