Masses Mass Genesis Factorized Load Density Support Averaged Factorized Load To

A sufficient subtarget

In the Recognition Science framework, a recognition event is a discrete record of something being recognized, and the framework's ledger, a discrete record of such events, assigns numerical loads to sites in a pattern. A central goal is to show that a pattern's total load equals a predicted mass value derived from the framework's constants. The declaration supportAveragedFactorizedLoad_to_masslaw_average establishes a sufficient condition for reaching that goal: if every site in the pattern's support carries the same share of the total predicted load, then the pattern's average site load equals the average predicted load.

This is a formal theorem in the framework's machine-checked library of formal theorems, not a physical derivation. It says that a uniform distribution of the total load, one where each site gets an equal fraction, is enough to make the average match. The theorem also implies that such a uniform distribution realizes the mass law: if the pattern's support is nonempty and the uniform condition holds, then the mass law is realized for that pattern. This is a concrete, checkable target for a later proof to aim at.

The declaration does not claim that stable light dynamics actually forces this uniform distribution. It does not prove that any physical process produces such a density. It merely states that if one assumes this distribution, the mass law follows. The framework's own documentation says the next theorem must derive a site load density summing to the exact factorized expression, and that the uniform version is a simple sufficient landing surface, not the final answer.

What this changes is the shape of the remaining work. Instead of needing to derive a complicated nonuniform density, a later proof can aim for the simpler uniform condition, and the theorem guarantees that this is enough to close the gap. The uniform condition is a sufficient subtarget, not a necessary one, and the framework explicitly allows a later proof to replace it with a nonuniform density.

theorem supportAveragedFactorizedLoad_to_masslaw_average
    (ψ : LightPattern Λ)
    (havg : SupportAveragedFactorizedLoad ψ) :
    SupportAveragedMassLawLoad ψ := by
  intro x hx
  rw [havg x hx, factorizedMassLawLoad_eq_predictedMass ψ]

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

What this page does not claim

Stable light dynamics forces the uniform load distribution. The uniform distribution is the only way to realize the mass law. The factorized load expression is derived from first principles in this module.

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: