Masses Mass Genesis Load Rigidity Stable Topology Load Rigid At

Load rigidity

In the Recognition Science framework, a light pattern is a discrete record of events on a substrate. A pattern is stable when it persists under the framework's dynamics. The declaration StableTopologyLoadRigidAt states a local rigidity property: if one stable pattern is given, then every other stable pattern with the same topology, meaning the same connectivity structure of events, has the same integrated neutral load. The load is a scalar quantity attached to the pattern, and the declaration says this quantity is fixed by the topology alone, not by the pattern's detailed geometry.

The statement is a conditional promise. It does not assert that any stable pattern exists, nor that any particular topology is realized. It only says that if two stable patterns share a topology, then their loads agree. The proof in the framework's machine-checked library of formal theorems establishes this implication. A companion definition, FactorizedSameTopologyRepresentative, asks for a representative pattern in the same topology whose load density has already been written in a factorized form.

The two pieces combine into a theorem: given a stable pattern, if it is load-rigid and a factorized representative exists in its topology, then the pattern's rest mass equals its predicted mass. The same theorem has a global version: if every stable pattern on a substrate is load-rigid and every stable topology has a factorized representative, then the equality holds for all patterns. The framework presents this as a reduction. The difficult problem of deriving the mass law for all patterns splits into two easier tasks: proving rigidity within each topology, and constructing one factorized example per topology.

What the declaration does not claim is as important as what it proves. It does not prove that rigidity holds for any particular topology. It does not construct the factorized representative. It does not say what the load's numerical value is, nor does it compare that value to any measured particle mass. The theorem is a bridge: it shows how mass equality would follow from two premises, but it leaves both premises as targets for further work.

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

StableTopologyLoadRigidAt does not prove that any stable pattern exists. It does not construct a factorized representative for any topology. It does not identify the numerical value of the load or compare it to any measured 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/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: