Gravity Seven Gaps Class Pushforward One Lt Fiber Card Edge Class

The two-edge example

In the Recognition Science framework, a ledger is a discrete record of events, and one of its central objects is a sum over all possible labeled geometries, called the path sum. The declaration one_lt_fiberCard_edgeClass is a proved theorem about a tiny piece of that sum: it establishes that in the simplest nontrivial case, with two vertices and one edge, there exist two distinct labeled complexes that are nevertheless equivalent under relabeling. Specifically, the complexes edgeAB and edgeBA, which differ only in which vertex is called 0 and which is called 1, belong to the same equivalence class. The theorem proves that this class contains more than one labeled complex; its fiber cardinality is greater than 1.

This fact matters because of how the path sum is decomposed. A separate theorem, Z_eq_classPushforward, proves that when a weight function is constant on equivalence classes, the sum over all labeled complexes equals a sum over classes, where each class contributes its total mass. The total mass of a class, classMass, is not simply the mass of one representative. By classMass_eq_fiberCard_mul_mu, it equals the number of labeled complexes in the class multiplied by the mass of a single representative. The theorem mu_lt_classMass_edgeClass then shows numerically that for the class containing edgeAB, the class mass is strictly greater than the mass of edgeAB alone. This is a concrete demonstration that the class decomposition carries the full labeled count, not just a single representative's weight.

The framework's library, a machine-checked collection of formal theorems, proves this with no unproved assumptions. The proof of one_lt_fiberCard_edgeClass explicitly exhibits the two distinct members of the class and shows they are equivalent via a vertex swap. This is not a claim about a continuum limit, nor a derivation of the 1/|Aut| convention from first principles. The theorem concerns only the labeled path sum PathSum.Z, not the quotient-first object defined directly on classes. The distinction is a matter of convention, not a contradiction: the two sums are different objects, and the theorem proves a fact about one of them.

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

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

What this page does not claim

This theorem does not apply to the quotient-first object Z_RS_uv, which uses a different summation convention. This theorem does not derive the 1/|Aut| convention from invariance and normalization; that remains a model input. This theorem does not establish any continuum limit or prepare convergence for the path sum.

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: