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

The mass equality theorem

The theorem restMass_eq_predictedMass_of_massAdmissible states a precise equality: for any light pattern that is both stable and carries a factorized topology load density, the pattern's rest mass equals its predicted mass. The rest mass is the mass the pattern has when it is not moving; the predicted mass is the value the framework's mass law assigns to that pattern's topology and load. The theorem is proved in the machine-checked library of formal theorems, meaning the equality follows from the framework's definitions and prior theorems with no unverified assumptions.

The theorem's condition matters as much as its conclusion. A pattern must be mass-admissible: it must be a stable closed light pattern, and it must carry a factorized topology load density, which is evidence that the pattern's site loads realize the mass law's target. The framework proves this equality for such admissible patterns. It also proves that any pattern satisfying a stronger physical stability predicate is admissible, so the equality extends to those patterns as well.

The framework does not claim this equality for every stable pattern. A separate theorem shows that if two stable patterns share the same topology but carry different integrated loads, then not every stable pattern can be mass-admissible. The refined carrier thus exists precisely because the raw stable pattern class is too broad: it permits amplitude variation at fixed topology, which the mass equality cannot accommodate. The theorem's reach is therefore bounded by its admissibility condition, and extending it to all physically stable patterns remains an open construction problem.

theorem restMass_eq_predictedMass_of_massAdmissible
    {ψ : LightPattern Λ}
    (hψ : MassAdmissibleStablePattern ψ) :
    restMass ψ = predictedMass ψ :=
  stable_factorizedTopologyLoadDensity_restMass_eq_predictedMass
    ψ hψ.stable hψ.factorized_density

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

What this page does not claim

The theorem does not apply to every stable closed light pattern, only to those with the required factorized density evidence. The framework does not claim to have constructed any specific physical pattern satisfying the admissibility condition. The equality does not by itself assign numerical values to any particle's 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/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: