Masses Mass Genesis Canonical Load Factorization Rest Mass Eq Predicted Mass Of

The mass identity

The declaration restMass_eq_predictedMass_of_stable_and_canonicalPrimitiveLoadFactorizes is a theorem in the machine-checked library of formal theorems that Recognition Science uses. It states a conditional identity: if a light pattern is stable and its canonical primitive load factorizes, then its rest mass equals its predicted mass. In plain terms, it says that for a certain class of objects, the mass they actually have is the mass the framework's law says they should have.

The theorem does not say that every stable pattern has this property. It requires two premises: stability and load factorization. The library also records a separate theorem showing that stability alone is not enough, because raw amplitudes can vary at fixed topology. That obstruction theorem, not_allStableCanonicalPrimitiveLoadFactorizes_of_sameTopology_different_load, proves that two stable patterns with the same topology but different integrated loads cannot both factorize, so the extra premise is essential.

What the theorem provides is a bridge. It connects the abstract condition that a load factorizes, which is a statement about how the pattern's meaning is distributed, to a concrete equality of mass values. The proof route goes through an equivalence: canonical primitive load factorization holds exactly when the integrated meaning load equals the factorized mass law load, which is the same as saying the mass law is realized. The theorem then applies a prior result that a stable pattern with a realized mass law has rest mass equal to predicted mass.

The practical consequence is that for any pattern that meets the two premises, the framework's mass prediction is not a separate guess but a derived consequence. The identity turns a structural condition into a numerical fact. It does not, however, say which physical particles satisfy the premises; that remains a separate question about the empirical content of the framework.

theorem restMass_eq_predictedMass_of_stable_and_canonicalPrimitiveLoadFactorizes
    (ψ : LightPattern Λ)
    (hstable : StableClosedLightPattern ψ)
    (hfactor : CanonicalPrimitiveLoadFactorizes ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_load_realized ψ hstable
    ((canonicalPrimitiveLoadFactorizes_iff_massLawLoadRealized ψ).1 hfactor)

theorem not_allStableCanonicalPrimitiveLoadFactorizes_of_sameTopology_different_load
    {ψ χ : LightPattern Λ}
    (hψ : StableClosedLightPattern ψ)
    (hχ : StableClosedLightPattern χ)
    (htop : SameTopology ψ χ)
    (hload : integratedMeaningLoad ψ ≠ integratedMeaningLoad χ) :
    ¬ (∀ η : LightPattern Λ,
        StableClosedLightPattern η →
          CanonicalPrimitiveLoadFactorizes η) := by
  intro Hall
  have hψR : MassLawLoadRealized ψ :=
    (canonicalPrimitiveLoadFactorizes_iff_massLawLoadRealized ψ).1
      (Hall ψ hψ)
  have hχR : MassLawLoadRealized χ :=
    (canonicalPrimitiveLoadFactorizes_iff_massLawLoadRealized χ).1
      (Hall χ hχ)
  exact sameTopology_different_load_obstructs_both_realized
    hψ hχ htop hload ⟨hψR, hχR⟩

theorem canonicalPrimitiveLoadFactorizes_iff_integratedMeaningLoad_eq_factorized
    (ψ : LightPattern Λ) :
    CanonicalPrimitiveLoadFactorizes ψ ↔
      integratedMeaningLoad ψ = factorizedMassLawLoad ψ := by
  constructor
  · intro h
    rw [integratedMeaningLoad_eq_support_sum ψ]
    simpa [CanonicalPrimitiveLoadFactorizes, PrimitiveLoadFactorizes,
      canonicalPrimitiveSiteLoadLaw] using h
  · intro h
    rw [integratedMeaningLoad_eq_support_sum ψ] at h
    simpa [CanonicalPrimitiveLoadFactorizes, PrimitiveLoadFactorizes,
      canonicalPrimitiveSiteLoadLaw] using h

What this page does not claim

The theorem does not claim that every stable pattern has equal rest and predicted mass. The theorem does not identify which patterns are stable or which loads factorize. The theorem does not establish any numerical value for a specific particle mass.

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