Masses Mass Genesis Rest Mass Equals Mass Law

The conditional bridge

In the Recognition Science framework, a ledger (a discrete record of recognition events) assigns to every stable closed light pattern two numbers. One is rest mass: the integrated neutral light load, the total amount of light-state content the pattern carries when at rest. The other is predicted mass: a value selected by topology-derived labels, read off from the pattern's shape alone. The natural question is whether these two always agree.

The framework's machine-checked library of formal theorems answers with a conditional bridge, not a blanket proof. The theorem restMass_eq_predictedMass_of_load_realized states: if a pattern is stable and closed, and if its integrated load realizes the mass-law value selected by its topology, then rest mass equals predicted mass. The proof is short: stability rewrites rest mass as the integrated load, and the realization condition supplies the equality. A second theorem, restMass_eq_predictedMass_of_canonical, packages the same result for canonical mass patterns, defined as stable closed patterns whose load is proved to realize the topology value.

The library also proves a no-smuggling obstruction. Two patterns with the same topology always share the same predicted mass; the topology alone fixes the prediction. But two such patterns can carry different rest masses, because the current light-pattern surface permits arbitrary light-state amplitudes with the same topology. The theorem sameTopology_different_restMass_obstructs_both_realized shows that if two same-topology patterns have different rest masses, they cannot both satisfy the mass-law equality. The missing condition is named exactly: MassLawLoadRealized, the predicate that the invariant neutral load realizes the mass-law value. It is not a proof; it is the remaining normalization theorem, left open as a target.

What this establishes matters for the framework's mass ladder. The topology-derived prediction is a clean function of the pattern's shape, but the realized rest mass depends on how light amplitudes are normalized. The conditional bridge says the mass law holds precisely when that normalization is fixed from the topology. The obstruction says arbitrary amplitudes cannot all satisfy it. The framework proves the exact boundary of what follows, and names the one missing piece that would turn the conditional bridge into a full equality.

theorem restMass_eq_predictedMass_of_load_realized
    (ψ : LightPattern Λ)
    (hstable : StableClosedLightPattern ψ)
    (hrealized : MassLawLoadRealized ψ) :
    restMass ψ = predictedMass ψ := by
  rw [restMass_eq_integratedMeaningLoad_of_stable ψ hstable]
  exact hrealized

theorem predictedMass_eq_of_sameTopology
    {ψ χ : LightPattern Λ} (h : SameTopology ψ χ) :
    predictedMass ψ = predictedMass χ := by
  unfold predictedMass
  rw [sectorOf_eq_of_sameTopology h,
      rungOf_eq_of_sameTopology h,
      ZOf_eq_of_sameTopology h]

theorem sameTopology_different_restMass_obstructs_both_realized
    {ψ χ : LightPattern Λ}
    (htop : SameTopology ψ χ)
    (hdiff : restMass ψ ≠ restMass χ) :
    ¬ (restMass ψ = predictedMass ψ ∧ restMass χ = predictedMass χ) := by
  intro hboth
  exact hdiff
    (sameTopology_realized_patterns_have_same_restMass htop hboth.1 hboth.2)

What this page does not claim

The full unconditional equality restMass = predictedMass is not proved for every stable pattern. The framework does not derive particle masses from this module alone. No claim is made that arbitrary light-state amplitudes can satisfy the mass law.

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/Masses/MassGenesis/RestMassEqualsMassLaw.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: