Masses Mass Genesis Refined Stable Carrier Rest Mass Eq Predicted Mass Of Physic

The mass identity

In the Recognition Science framework, mass is not a free parameter. It is a derived quantity: the rest mass of a stable closed light pattern equals the mass predicted by the framework's own mass law. The theorem restMass_eq_predictedMass_of_physicalStable states this identity for any pattern that is physically stable, meaning it satisfies a stronger condition than mere mathematical stability.

The framework models reality as a ledger: a discrete record of recognition events. A stable closed light pattern is a self-sustaining configuration of such events. The mass law assigns a predicted mass to any pattern based on its topology and load density. The theorem proves that for patterns meeting the physical stability condition, the actual rest mass equals this predicted mass.

The condition is central. The framework distinguishes between raw stability, which permits amplitude variation at fixed topology, and physical stability, which requires a factorized topology load density. This factorized density is proof evidence, not a reverse fit. The theorem holds only under this stronger carrier, which the framework calls TopologyNormalizedStablePattern.

What the theorem does not claim is equally important. It does not assert that every mathematically stable pattern satisfies the identity. The framework proves an obstruction: two stable patterns with the same topology but different loads cannot both be mass-admissible. It also does not claim that the physical stability condition itself has been derived from dynamics; that construction remains open. The theorem is conditional: given physical stability, the identity follows.

The identity has a concrete payoff. It unifies inertial and gravitational mass: for any stable load readout theory, both readouts equal the rest mass. This means the framework's mass law is internally consistent with the equivalence principle, at least for the patterns it can admit.

theorem restMass_eq_predictedMass_of_physicalStable
    {PhysicalStable : LightPattern Λ → Prop}
    (H : PhysicalStablePatternsAreMassAdmissible PhysicalStable)
    {ψ : LightPattern Λ}
    (hψ : PhysicalStable ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_massAdmissible (H.admissible ψ hψ)

/-- The old all-raw-stable construction target is impossible in the presence of
a same-topology stable pair with different load. -/
theorem not_allStableMassAdmissible_of_sameTopology_different_load
    {ψ χ : LightPattern Λ}
    (hψ : StableClosedLightPattern ψ)
    (hχ : StableClosedLightPattern χ)
    (htop : SameTopology ψ χ)
    (hload : integratedMeaningLoad ψ ≠ integratedMeaningLoad χ) :
    ((∀ η : LightPattern Λ,
        StableClosedLightPattern η →
          MassAdmissibleStablePattern η) → False) := by
  intro Hall
  have hψM : restMass ψ = predictedMass ψ :=
    restMass_eq_predictedMass_of_massAdmissible (Hall ψ hψ)
  have hχM : restMass χ = predictedMass χ :=
    restMass_eq_predictedMass_of_massAdmissible (Hall χ hχ)
  have hrest : restMass ψ = restMass χ :=
    sameTopology_realized_patterns_have_same_restMass htop hψM hχM
  rw [restMass_eq_integratedMeaningLoad_of_stable ψ hψ,
      restMass_eq_integratedMeaningLoad_of_stable χ hχ] at hrest
  exact hload hrest

theorem readout_identity
    (T : StableLoadReadoutTheory Λ)
    (Ψ : TopologyNormalizedStablePattern Λ) :
    T.readout.inertialMass Ψ.pattern =
        T.readout.gravitationalMass Ψ.pattern ∧
      T.readout.inertialMass Ψ.pattern = restMass Ψ.pattern ∧
      T.readout.gravitationalMass Ψ.pattern = restMass Ψ.pattern :=
  stableLoadReadoutTheory_identity T Ψ.pattern Ψ.stable

What this page does not claim

The theorem does not claim that every mathematically stable pattern satisfies the mass identity. The theorem does not claim that the physical stability condition has been derived from dynamics; that construction remains open. The theorem does not claim that the predicted mass values match experimentally measured particle masses.

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/RefinedStableCarrier.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: