Masses Mass Genesis Factorized Load Density Factorized Mass Law Load Pos

The positivity theorem

The declaration factorizedMassLawLoad_pos is a theorem in the framework's machine-checked library of formal theorems. It states that for any light pattern, the value of a certain predicted mass, written as a product of three factors, is strictly greater than zero. In plain terms, the framework proves that the quantity it associates with a particle's mass can never be zero or negative; it is always a positive real number.

The proof is short and direct. The framework first shows that its factorized expression for the mass is exactly equal to its previously defined predicted mass. It then invokes an earlier theorem, predictedMass_pos, which already established that the predicted mass is positive. The new theorem is therefore a corollary: it transfers the known positivity of the predicted mass to the new, factorized form.

The factorized form itself is a definitional choice, not a derived result. The framework writes the predicted mass as a product of three pieces: a sector geometry factor, a power of the golden ratio whose exponent combines a rung index and a charge-gap correction, and a base-two power from the sector's topology. This decomposition is useful because each piece comes from a different part of the framework's structure, but the framework does not yet prove that this particular factorization is forced by the underlying dynamics.

What the theorem does not claim is just as important as what it proves. It does not prove that any actual physical density realizes this factorized load. The framework defines a structure, FactorizedTopologyLoadDensity, that would provide such a density, and it proves that if such a density exists, then the mass law is realized. But the existence of that density is left open; the theorem only states the positivity of the target value, not its attainability.

In Recognition Science, this theorem is a stepping stone. It confirms that the factorized target is a well-formed positive quantity, which is a necessary condition for any future proof that a physical load density sums to it. The positivity itself is not the destination; it is a sanity check on the path. The framework's own documentation states that the next theorem must derive a site load density summing to this exact factorized expression, and that derivation is not yet complete.

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

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

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

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

/-- 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 ψ)

What this page does not claim

It does not prove that any physical density realizes the factorized load. It does not derive the factorized form from underlying dynamics; the form is a definitional choice. It does not establish that the golden ratio exponent is the unique or forced exponent for the mass law.

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: