Masses Mass Genesis Factorized Load Density Factorized Topology Load Density Rea

The factorized load target

The declaration factorizedTopologyLoadDensity_realizes is a theorem in the framework's machine-checked library of formal theorems. It states that if a recognition pattern, a discrete record of events, carries a load density that can be written as a product of three separate factors, then that pattern realizes the framework's mass law. The three factors are the sector geometry, the rung scale, and the charge gap. Each factor comes from a different part of the pattern's topology: the sector defines a yardstick, the rung gives an exponent, and the charge gap contributes another exponent through a logarithmic correction.

The theorem itself is a conditional statement. It does not prove that such a factorized density exists for any real pattern. Instead, it establishes a bridge: if you can exhibit a density with the right nonnegativity, site-load equality, and sum properties, then the pattern's rest mass equals the predicted mass. The proof is a chain of definitions and rewrites, all checked by the kernel. The final theorem, stable_factorizedTopologyLoadDensity_restMass_eq_predictedMass, adds the condition that the pattern is stable, a closed light pattern, and concludes the same equality.

What the declaration does not claim is just as important. It does not prove that stable light dynamics forces the density. The docstring is explicit: the next theorem must derive a site load density summing to this exact factorized expression. The factorized target is a landing surface, not a derivation. It also does not claim that the density is unique. A later proof may replace the equal-share version with a nonuniform density. The theorem only shows what happens if such a density is supplied.

In plain terms, the declaration removes a black box from the mass genesis story. It shows that the mass law's value can be decomposed into three meaningful pieces, each tied to a topological feature of the pattern. The remaining open question is whether those pieces actually arise from the dynamics. That is a target for future work, not a result this theorem delivers.

theorem factorizedTopologyLoadDensity_realizes
    (ψ : LightPattern Λ)
    (ρ : FactorizedTopologyLoadDensity ψ) :
    MassLawLoadRealized ψ :=
  topologyForcedLoadDensity_realizes ψ
    (topologyForcedLoadDensity_of_factorized ψ ρ)

/-- The factorized MassLaw load target, written as sector geometry times one
phi exponent assembled from rung and charge-gap pieces. -/
noncomputable def factorizedMassLawLoad (ψ : LightPattern Λ) : ℝ :=
  sectorLoadFactor ψ *
    Constants.phi ^ (rungLoadExponent ψ + chargeGapLoadExponent ψ)

theorem factorizedTopologyLoadDensity_realizes
    (ψ : LightPattern Λ)
    (ρ : FactorizedTopologyLoadDensity ψ) :
    MassLawLoadRealized ψ :=
  topologyForcedLoadDensity_realizes ψ
    (topologyForcedLoadDensity_of_factorized ψ ρ)

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 theorem does not prove that stable light dynamics forces the density. The theorem does not claim the factorized density is unique. The theorem does not derive the density from first principles; it only shows what follows if such a density is supplied.

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: