Masses Mass Genesis Load Rigidity Factorized Representative For Every Stable Top

A shortcut to mass

In the Recognition Science account, the mass of a stable particle is not a free number. The framework's ledger, a discrete record of recognition events, assigns each stable closed pattern a load, and the MassLaw says that load equals the predicted mass. Proving that equality for every possible pattern is a large task. The declaration FactorizedRepresentativeForEveryStableTopology packages a shortcut: instead of checking every pattern directly, it asks for two smaller things to be true.

The first is rigidity. A stable pattern is load-rigid if every other stable pattern with the same topology, the same way its parts connect, carries the same integrated load. The second is a representative. For any stable pattern, there must exist one other stable pattern with the same topology whose load density has already been written in the special factorized form. The declaration states that both hold for every stable pattern on a given substrate. When they do, the theorems in the same module conclude that the MassLaw load is realized and that rest mass equals predicted mass for every stable pattern on that substrate.

This is a reduction, not a discovery of new physics. The declaration itself is a definition of a target property. The two theorems that use it, massLawLoadRealized_of_global_rigidity_and_representatives and restMass_eq_predictedMass_of_global_rigidity_and_representatives, are proved in the machine-checked library of formal theorems. They show that if the two premises hold, the mass conclusion follows. The premises themselves, rigidity and the existence of representatives, are not proved by this declaration. They remain targets for further work.

The value of the shortcut is practical. Proving rigidity for a topology class and constructing one factorized example is often easier than deriving the load for every pattern one by one. The declaration makes that route explicit. It also states the condition without any reference to a measured mass, so the reduction is purely structural. What it does not claim is that the premises hold for any real substrate, or that any specific particle mass has been derived. It establishes a conditional path, not an arrival.

/-- Global substrate-level representative target. -/
def FactorizedRepresentativeForEveryStableTopology
    (Λ : Type*) [Fintype Λ] [DecidableEq Λ] : Prop :=
  ∀ ψ : LightPattern Λ,
    StableClosedLightPattern ψ →
      FactorizedSameTopologyRepresentative ψ

theorem massLawLoadRealized_of_global_rigidity_and_representatives
    (hrigid : StableTopologyLoadRigidOn Λ)
    (hreps : FactorizedRepresentativeForEveryStableTopology Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ) :
    MassLawLoadRealized ψ :=
  massLawLoadRealized_of_rigidity_and_factorized_representative
    ψ hψ (hrigid ψ) (hreps ψ hψ)

theorem restMass_eq_predictedMass_of_global_rigidity_and_representatives
    (hrigid : StableTopologyLoadRigidOn Λ)
    (hreps : FactorizedRepresentativeForEveryStableTopology Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_load_realized ψ hψ
    (massLawLoadRealized_of_global_rigidity_and_representatives
      hrigid hreps ψ hψ)

What this page does not claim

This declaration does not prove that any real substrate satisfies the rigidity or representative premises. This declaration does not derive the mass of any specific particle. This declaration does not define what constitutes a stable pattern or a topology.

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