Masses Mass Genesis Load Normalization Topology Forced Load Density

The load density target

In the Recognition Science framework, mass is not a number attached to a particle; it is a property of a pattern's internal economy. The framework tracks a quantity called load, a discrete record of how much meaning each occupied site carries. The total load, summed over all sites, is what the framework identifies with mass. The open problem is to show that the topology of the pattern, its shape and connectivity, forces the right load distribution.

The declaration TopologyForcedLoadDensity is a precise statement of that target. It defines a structure: a function that assigns a nonnegative real number to each site, matches the site's actual load, and whose sum over the support equals the mass predicted by topology alone. The theorem topologyForcedLoadDensity_realizes proves that if such a density exists, then the mass law is realized: the integrated load equals the predicted mass. A companion theorem, stable_topologyForcedLoadDensity_restMass_eq_predictedMass, extends this to stable patterns, showing that the rest mass equals the predicted mass.

The declaration is a landing surface, not a derivation. It does not assert that such a density exists for every pattern. It does not say how topology forces the density. It only states what must be proved: that a site load law summing to the topology-derived value is the right target. The docstring is explicit that future modules should derive this from Q3/Rhat constraints, not assume it as an external calibration.

This matters because the framework's earlier normalization, CP6, fixes each occupied site to unit load. That makes the total load equal to the number of sites, a cardinality, not a mass. The new density target names the missing amplitude information: the size of each site's share, not just its presence. The theorem shows that if the right density can be found, the mass law follows. The work of finding it remains open.

theorem topologyForcedLoadDensity_realizes
    (ψ : LightPattern Λ) (ρ : TopologyForcedLoadDensity ψ) :
    MassLawLoadRealized ψ := by
  unfold MassLawLoadRealized
  rw [integratedMeaningLoad_eq_support_sum ψ]
  calc
    ψ.support.sum (fun x => siteMeaningLoad ψ x)
        = ψ.support.sum ρ.density := by
          apply Finset.sum_congr rfl
          intro x hx
          exact (ρ.equals_site_load x hx).symm
    _ = predictedMass ψ := ρ.sums_to_predicted

theorem stable_topologyForcedLoadDensity_restMass_eq_predictedMass
    (ψ : LightPattern Λ)
    (hstable : StableClosedLightPattern ψ)
    (ρ : TopologyForcedLoadDensity ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_load_realized ψ hstable
    (topologyForcedLoadDensity_realizes ψ ρ)

What this page does not claim

The declaration does not prove that a topology-forced load density exists for any pattern. It does not describe how topology forces the density. It does not claim that the mass spectrum is derived; that remains a target.

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