Gravity Seven Gaps Class Pushforward Exists Non Singleton Fiber

The fiber that is not alone

In the Recognition Science framework, a recognition is a discrete event that the universe records, and a ledger is the record of those events. When the framework counts physical configurations, it sometimes groups them into classes of objects that are the same up to relabeling. The declaration exists_nonSingleton_fiber proves, in the machine-checked library of formal theorems, that at least one such class contains more than one distinct labeled object. Specifically, it exhibits two different labeled complexes, called edgeAB and edgeBA, each consisting of a single edge between two vertices, that are related by swapping the two vertex labels. The proof shows they are distinct as labeled objects yet equivalent under relabeling, so the fiber of the quotient map that sends each labeled complex to its relabeling class has cardinality greater than one.

This fact matters because of how sums over configurations are computed. The framework defines a path sum Z over labeled complexes, and a theorem Z_eq_classPushforward shows that when a weight function is constant on relabeling classes, this sum can be re-expressed as a sum over classes, where each class contributes its class mass times the weight of a representative. The class mass is not simply the symmetry factor 1/|Aut| of a representative; it is the size of the fiber times that factor. The declaration mu_lt_classMass_edgeClass proves numerically that for the class of edgeAB, the measure of the single labeled complex is strictly less than the class mass, confirming that the fiber has more than one element. This shows that the labeled sum and the inequivalent-class sum with per-class 1/|Aut| weights differ already at the smallest nontrivial size, B = 2.

In Recognition Science, this result is a kernel fact, not a modeling choice. It is proved with zero axioms beyond the standard three, and it forces the class decomposition of the standing path sum to carry the fiber cardinality factor. The framework does not claim that this is the only possible convention; it records that the exact-shell wave Z_RS_uv uses a different quotient-sum convention, and the two are not in contradiction. The declaration also does not establish any continuum limit, does not derive the 1/|Aut| convention from first principles, and does not bridge any gap to a physical theory of gravity. It is a precise, narrow statement about how to count labeled objects when grouping them into equivalence classes.

For the general reader, the upshot is that when you decide to identify objects that differ only by renaming, you must remember that a class can contain many distinct labeled members. The proof shows this happens already with the simplest possible complex, a single edge. This is a concrete, checkable fact that any future construction in the framework must respect: if you sum over labeled objects, you cannot simply replace each class by a single representative with a symmetry weight, because the fiber size changes the sum. The framework's library has now made this explicit and machine-checked, so the counting rule is no longer an assumption but a proved theorem.

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

The declaration does not establish any continuum limit or prepare convergence for the path sum. It does not derive the 1/|Aut| convention from invariance and normalization; that remains a model input. It does not apply to the exact-shell wave Z_RS_uv, which uses a different quotient-sum convention.

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: