Masses Mass Genesis Factorized Load Density Support Averaged Factorized Load Rea

The equal-share density

In the Recognition Science framework, a mass value is not a free parameter: it is a prediction that must be realized by a load density, a function assigning a nonnegative real number to each site of a light pattern. The declaration supportAveragedFactorizedLoad_realizes establishes one sufficient way to achieve that realization. If every site in a nonempty pattern carries the same share of the factorized mass-law load, then the pattern realizes the mass law. The equal-share condition is a definitional choice, not a derived necessity; the framework's own documentation calls it a simple sufficient landing surface for closing the mass genesis gap.

The factorized load itself is a composite object, built from three pieces already proved or exposed upstream: sector geometry via the yardstick, closed-pattern rung scale via rungOf, and charge gap via ZOf and the mass-law gap correction. The theorem factorizedMassLawLoad_eq_predictedMass shows this factorized expression equals the predicted mass by definition, and factorizedMassLawLoad_pos proves it is strictly positive. The equal-share density then splits that total uniformly across the support, and the theorem supportAveragedFactorizedLoad_realizes converts that uniform split into a certificate that the mass law is realized. A companion theorem, stable_factorizedTopologyLoadDensity_restMass_eq_predictedMass, extends the result to stable closed light patterns, where rest mass equals the predicted mass.

The declaration does not claim that stable light dynamics forces this density. The framework's own documentation states this plainly: the next theorem must derive a site load density summing to this exact factorized expression. The equal-share version is explicitly a stand-in, one that a later proof may replace with a nonuniform density. It is a sufficient subtarget, not the derived target itself. The framework has removed the black box from the mass genesis problem: the missing object is now named, factored, and given a concrete sufficient realization, but the forcing argument that would close the gap remains open.

theorem supportAveragedFactorizedLoad_realizes
    (ψ : LightPattern Λ)
    (hsupp : ψ.support.Nonempty)
    (havg : SupportAveragedFactorizedLoad ψ) :
    MassLawLoadRealized ψ :=
  supportAveragedMassLawLoad_realizes ψ hsupp
    (supportAveragedFactorizedLoad_to_masslaw_average ψ havg)

theorem factorizedMassLawLoad_eq_predictedMass
    (ψ : LightPattern Λ) :
    factorizedMassLawLoad ψ = predictedMass ψ := by
  rfl

theorem factorizedMassLawLoad_pos (ψ : LightPattern Λ) :
    0 < factorizedMassLawLoad ψ := by
  rw [factorizedMassLawLoad_eq_predictedMass ψ]
  exact predictedMass_pos ψ

theorem stable_factorizedTopologyLoadDensity_restMass_eq_predictedMass
    (ψ : LightPattern Λ)
    (hstable : StableClosedLightPattern ψ)
    (ρ : FactorizedTopologyLoadDensity ψ) :
    restMass ψ = predictedMass ψ :=
  stable_topologyForcedLoadDensity_restMass_eq_predictedMass ψ hstable
    (topologyForcedLoadDensity_of_factorized ψ ρ)

What this page does not claim

Stable light dynamics forces the equal-share density. The equal-share density is the unique realization of the mass law. The factorized load expression is derived from dynamics rather than assembled from proved pieces.

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