Masses Mass Genesis Load Normalization

Load normalization

In the Recognition Science framework, a ledger (a discrete record of events) assigns to each occupied site a meaning load, a number representing the recognition cost at that site. The integrated load, the sum over all occupied sites, is what should become a particle's mass. The problem is that a simple unit normalization, setting every site's load to 1, captures only the direction of the pattern, not the amplitude scale needed for mass. This is the gap that load normalization addresses.

The module LoadNormalization.lean states the target precisely. Its central result is a theorem: if every occupied site carries the equal share of the topology-selected MassLaw value, then the rest mass equals the predicted mass. This is a sufficient condition, not the final physics of every pattern. The theorem is proved in the machine-checked library of formal theorems, meaning the logical derivation is verified step by step.

The module also defines a more general target: a topology-forced load density, a site load law whose sum equals the topology-derived MassLaw value. This is the next true bottom-up target. The current module does not derive this density from deeper constraints; it only proves that if such a density exists, the mass law is realized. The derivation from Q3/Rhat constraints remains an open problem.

What this establishes in plain language: the framework has a clear, formal statement of what must be proved next. It separates the easy part (unit normalization gives support cardinality) from the hard part (topology must force the right load density). The module is a landing surface, a precise target for future work, not a completed derivation of the mass spectrum.

theorem stable_supportAveraged_restMass_eq_predictedMass
    (ψ : LightPattern Λ)
    (hstable : StableClosedLightPattern ψ)
    (havg : SupportAveragedMassLawLoad ψ) :
    restMass ψ = predictedMass ψ := by
  have hsupp : ψ.support.Nonempty :=
    hstable.1
  exact restMass_eq_predictedMass_of_load_realized ψ hstable
    (supportAveragedMassLawLoad_realizes ψ hsupp havg)

/-- A topology-forced load density is a site load law whose sum is the
topology-derived MassLaw value. Future modules should derive this from Q3/Rhat
constraints, not assume it as an external calibration. -/
structure TopologyForcedLoadDensity (ψ : LightPattern Λ) where
  density : Λ → ℝ
  nonneg : ∀ x ∈ ψ.support, 0 ≤ density x
  equals_site_load : ∀ x ∈ ψ.support, density x = siteMeaningLoad ψ x
  sums_to_predicted : ψ.support.sum density = predictedMass ψ

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

What this page does not claim

The module does not derive the load density from deeper principles; it only proves a sufficient condition. The module does not establish the full mass spectrum; it sets a target for future work.

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: