Encyclopedia Gravity Gravity Seven Gaps Class Pushforward Mu Lt Class Mass Edge Class

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Class Pushforward Mu Lt Class Mass Edge Class

In a discrete ledger, swapping two labels can change a counted mass, and a kernel-checked theorem shows exactly where the difference first appears.

Verify this page

A matter of bookkeeping

A ledger, a discrete record of events, often groups its entries into classes. In the Recognition Science framework, a triangulation class collects labeled complexes that differ only by relabeling. The declaration mu_lt_classMass_edgeClass is a theorem about one such class: it proves that the measure of a single labeled complex, mu edgeAB, is strictly less than the total class mass of its equivalence class, classMass (Quotient.mk (relabelSetoid 2) edgeAB), at size B = 2.

The statement is a kernel fact about bookkeeping, not a claim about physics. It shows that when a path sum is organized by classes, the weight carried by a class is the number of labeled complexes in it times a symmetry factor, not just the symmetry factor alone. The theorem classMass_eq_fiberCard_mul_mu makes this explicit: classMass q = (fiberCard (relabelSetoid B) q) * mu (Quotient.out q). The strict inequality at B = 2 is the first concrete instance where the labeled sum and the inequivalent-class sum with weights 1/|Aut| differ.

The proof exhibits two distinct labeled complexes, edgeAB and edgeBA, related by a vertex swap, and shows their quotient fiber has cardinality greater than one. This is a theorem about the labeled path sum Z of PathSumMeasure only. It does not apply to the exact-shell Z_RS_uv of the ExactShellGaugeUV wave, which uses a different quotient-sum convention. The two are different conventions, not a contradiction.

What the declaration does not claim is as important as what it proves. It does not establish that the continuum limit of Z exists, that the 1/|Aut| convention is derived from invariance plus normalization, or that the gap1 bridge is derived. Those flags remain red in the framework's status structure. The theorem is a precise, narrow result about how a labeled sum decomposes over classes, and it earns its place by making the distinction between labeled and quotient-sum conventions undeniable at the smallest possible example.

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)
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 · one_lt_fiberCard_edgeClass · 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⟩⟩
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 classPushforwardStatus_flags · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
classPushforwardStatus_flags · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean:367 
theorem classPushforwardStatus_flags :
    classPushforwardStatus.generic_fiber_decomposition_proved = true ∧
    classPushforwardStatus.classMass_defined = true ∧
    classPushforwardStatus.Z_eq_classPushforward_proved = true ∧
    classPushforwardStatus.classMass_is_fiberCard_mul_mu = true ∧
    classPushforwardStatus.nonSingleton_fiber_exhibited = true ∧
    classPushforwardStatus.Z_is_invAut_class_sum = false ∧
    classPushforwardStatus.quotient_first_object_constructed = false ∧
    classPushforwardStatus.Z_RS_continuum_limit = false ∧
    classPushforwardStatus.substrate_measure_derived = false ∧
    classPushforwardStatus.gap1_bridge_derived = false :=
  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩

What this page does not claim

The declaration does not prove that the continuum limit of Z exists. The declaration does not derive the 1/|Aut| convention from invariance plus normalization. The declaration does not apply to the exact-shell Z_RS_uv wave, which uses a different 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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND