Masses Mass Genesis Load Rigidity Load Rigidity Reduction Cert

The load-rigidity certificate

The ledger, a discrete record of events, is the framework's starting point. In Recognition Science, a stable particle is a closed pattern of light on that ledger. The question is whether such a pattern's rest mass, its mass when at rest, must equal a value predicted by the framework's own mass law. The declaration LoadRigidityReductionCert is a machine-checked certificate that packages the answer: if two conditions hold, then the equality is forced.

The first condition is load rigidity. Once a stable pattern has a certain topology, the shape of its connections, every other stable pattern with that same topology carries the same integrated neutral load. The second condition is the existence of a factorized representative: at least one pattern in that topology class whose site density has already been derived in the factorized form the mass law requires. The certificate's theorem, proved in the machine-checked library of formal theorems, states that these two conditions together imply the mass law is realized for every stable pattern in the class. A second theorem then closes the loop: rest mass equals predicted mass.

The certificate itself is a structure, a bundle that holds these theorems together. It does not prove the two conditions for any particular topology. It proves only the reduction: if you can establish rigidity and find a factorized representative, then you get the mass equality for free. The certificate also carries a global version, for every stable topology on a substrate at once, with the same logical shape.

What the certificate does not claim is just as important. It does not assert that any actual particle's mass has been computed. It does not name a single measured mass. It does not prove that load rigidity holds for any real topology, nor that a factorized representative exists for one. Those are separate targets, left open. The certificate is a bridge, not a destination: it shows what a complete proof would need, and what it would deliver.

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

No actual particle mass is computed or compared with measurement. Load rigidity is not proved for any specific topology. A factorized representative is not constructed for any specific 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: