Masses Mass Genesis Load Rigidity

Load rigidity

In physics, a particle's mass is a number you measure. In Recognition Science, mass is a consequence of a deeper structure: a stable pattern of recognition events. The framework's MassLaw states that the rest mass of such a pattern equals a predicted mass derived from its internal load. The difficulty is proving this for every possible stable pattern. The ledger, a discrete record of recognition events, can hold patterns of many shapes, and each shape might seem to carry its own load.

Load rigidity is the property that kills that worry. A stable pattern is load-rigid if every other stable pattern with the same topology, the same way its parts connect, has the same integrated neutral load. The module proves a reduction: if one can show load rigidity holds, and if one can construct a single representative pattern in each topology class whose load density already has the factorized MassLaw form, then every stable pattern with that topology realizes the MassLaw load. The theorem is massLawLoadRealized_of_rigidity_and_factorized_representative.

The payoff is a two-step route to the mass law. First, prove that stable closed dynamics is load-rigid inside a topology class. Second, construct one factorized representative in that same class. The module proves that these two steps together imply the rest mass equals the predicted mass, for both a single pattern and, in the global version, for every stable pattern on a finite substrate. No known mass enters the statement or the proof; the mass is forced by the topology and the load.

This matters because it turns a global problem into a local one. Instead of checking every possible pattern, the framework needs only to check one representative per topology class, plus the rigidity property. The module packages this reduction into a certificate, LoadRigidityReductionCert, which bundles the local and global closure theorems. The remaining work, proving rigidity and constructing the representatives, is a concrete target for the framework, not an open-ended search.

/-- Local rigidity target: once `ψ` is stable, every stable pattern with the
same topology has the same integrated neutral load. -/
def StableTopologyLoadRigidAt (ψ : LightPattern Λ) : Prop :=
  StableClosedLightPattern ψ →
    ∀ χ : LightPattern Λ,
      StableClosedLightPattern χ →
      SameTopology ψ χ →
      integratedMeaningLoad ψ = integratedMeaningLoad χ

theorem massLawLoadRealized_of_rigidity_and_factorized_representative
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ)
    (hrigid : StableTopologyLoadRigidAt ψ)
    (hrep : FactorizedSameTopologyRepresentative ψ) :
    MassLawLoadRealized ψ := by
  rcases hrep with ⟨χ, hχdensity, hχstable, htop⟩
  have hχrealized : MassLawLoadRealized χ :=
    factorizedTopologyLoadDensity_realizes χ hχdensity
  unfold MassLawLoadRealized at hχrealized ⊢
  calc
    integratedMeaningLoad ψ = integratedMeaningLoad χ :=
      hrigid hψ χ hχstable htop
    _ = predictedMass χ := hχrealized
    _ = predictedMass ψ := (predictedMass_eq_of_sameTopology htop).symm

theorem restMass_eq_predictedMass_of_rigidity_and_factorized_representative
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ)
    (hrigid : StableTopologyLoadRigidAt ψ)
    (hrep : FactorizedSameTopologyRepresentative ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_load_realized ψ hψ
    (massLawLoadRealized_of_rigidity_and_factorized_representative
      ψ hψ hrigid hrep)

theorem massLawLoadRealized_of_rigidity_and_factorized_representative
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ)
    (hrigid : StableTopologyLoadRigidAt ψ)
    (hrep : FactorizedSameTopologyRepresentative ψ) :
    MassLawLoadRealized ψ := by
  rcases hrep with ⟨χ, hχdensity, hχstable, htop⟩
  have hχrealized : MassLawLoadRealized χ :=
    factorizedTopologyLoadDensity_realizes χ hχdensity
  unfold MassLawLoadRealized at hχrealized ⊢
  calc
    integratedMeaningLoad ψ = integratedMeaningLoad χ :=
      hrigid hψ χ hχstable htop
    _ = predictedMass χ := hχrealized
    _ = predictedMass ψ := (predictedMass_eq_of_sameTopology htop).symm

What this page does not claim

This module does not prove that load rigidity holds for any particular topology class. This module does not construct the factorized representative for any specific topology. This module does not define what a light pattern or its topology is in physical terms.

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: