Masses Mass Genesis Factorized Load Density

The factorized load density

In the Recognition Science framework, a particle's predicted mass is not a free parameter. It is a value forced by the topology of a stable light pattern, the discrete record of recognition events that the framework uses to model physical structure. The module MassGenesis M7b takes that predicted mass and factors it into three pieces, each already derived or exposed in earlier steps of the framework's forcing chain.

The three factors are a sector geometry term, a rung exponent, and a charge-gap exponent. The sector term comes from the pattern's sector selection, the rung exponent subtracts 8 from the pattern's rung scale, and the charge-gap exponent is a logarithm of a topology-derived charge value. The product of the sector term and the golden ratio raised to the sum of the two exponents equals the predicted mass. This equality is a theorem in the framework's machine-checked library of formal theorems, proved by unfolding definitions.

The module then defines a factorized topology load density: a function on the pattern's support that is nonnegative, equals the site load at each point, and sums to the factorized mass. Any such density, when the pattern is stable, yields a rest mass equal to the predicted mass. This is a theorem, not a conjecture. The module also provides a simpler sufficient subtarget: if the site load is uniformly the factorized mass divided by the number of support points, the same conclusion follows.

What this establishes in plain language is a clean landing surface. The remaining open problem is not whether the density sums correctly, but whether stable light dynamics forces such a density to exist. The module removes the black box from the earlier step M7a by naming the exact expression the next theorem must derive. It does not prove that the dynamics forces the density; that remains a target.

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

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

The module does not prove that stable light dynamics forces the density to exist. The module does not assign numerical values to particle masses.

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: