Masses Mass Genesis Canonical Load Factorization Canonical Primitive Load Factor

A sufficient condition for mass factorization

In the Recognition Science framework, a particle's mass is not a free parameter but a value that must be realized by a specific load distribution over a discrete set of sites. The declaration canonicalPrimitiveLoadFactorizes_of_neutralUnit_and_supportCard_eq_factorized establishes a sufficient condition for this factorization to hold. It states that if a light pattern has a neutral unit load on its support and the number of occupied sites equals the factorized mass law load, then the pattern's canonical primitive load factorizes. In plain terms: if the load is evenly distributed and the support has exactly the right size, the mass is determined by the topology alone.

The theorem is one of several routes to the same conclusion. The machine-checked library of formal theorems also proves factorization from a topology-scaled CP6 load and from a support-averaged factorized load. What makes this particular declaration notable is its directness: it bypasses the need to verify the load at each site individually. Instead, it relies on two global conditions: a neutral unit load on the support and a support cardinality that matches the factorized mass law load. The proof is short because it uses an equivalence that reduces factorization to an equality between the integrated meaning load and the factorized mass law load.

What the declaration does not claim is equally important. It does not assert that every stable closed light pattern factorizes. In fact, the same module contains a theorem showing that two patterns with the same topology but different integrated loads cannot both factorize. This is the obstruction: raw amplitudes can vary at fixed topology, so factorization is not automatic. The declaration also does not claim that the neutral unit load condition is necessary; it is sufficient. A pattern could factorize without meeting this exact condition, though the library does not currently prove such a case.

The practical consequence is a certificate: when the two conditions hold, the pattern's rest mass equals its predicted mass. This is the bridge from the abstract load formalism to the measurable particle mass. The declaration provides one clean, checkable path to that bridge, while the obstruction theorem marks the boundary of what the current formalism can prove.

theorem canonicalPrimitiveLoadFactorizes_of_neutralUnit_and_supportCard_eq_factorized
    (ψ : LightPattern Λ)
    (hunit : NeutralUnitLoadOnSupport ψ)
    (hcard : (ψ.support.card : ℝ) = factorizedMassLawLoad ψ) :
    CanonicalPrimitiveLoadFactorizes ψ := by
  apply
    (canonicalPrimitiveLoadFactorizes_iff_integratedMeaningLoad_eq_factorized ψ).2
  rw [integratedMeaningLoad_eq_supportCard_of_neutralUnitLoad ψ hunit]
  exact hcard

theorem not_allStableCanonicalPrimitiveLoadFactorizes_of_sameTopology_different_load
    {ψ χ : LightPattern Λ}
    (hψ : StableClosedLightPattern ψ)
    (hχ : StableClosedLightPattern χ)
    (htop : SameTopology ψ χ)
    (hload : integratedMeaningLoad ψ ≠ integratedMeaningLoad χ) :
    ¬ (∀ η : LightPattern Λ,
        StableClosedLightPattern η →
          CanonicalPrimitiveLoadFactorizes η) := by
  intro Hall
  have hψR : MassLawLoadRealized ψ :=
    (canonicalPrimitiveLoadFactorizes_iff_massLawLoadRealized ψ).1
      (Hall ψ hψ)
  have hχR : MassLawLoadRealized χ :=
    (canonicalPrimitiveLoadFactorizes_iff_massLawLoadRealized χ).1
      (Hall χ hχ)
  exact sameTopology_different_load_obstructs_both_realized
    hψ hχ htop hload ⟨hψR, hχR⟩

theorem restMass_eq_predictedMass_of_stable_and_canonicalPrimitiveLoadFactorizes
    (ψ : LightPattern Λ)
    (hstable : StableClosedLightPattern ψ)
    (hfactor : CanonicalPrimitiveLoadFactorizes ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_load_realized ψ hstable
    ((canonicalPrimitiveLoadFactorizes_iff_massLawLoadRealized ψ).1 hfactor)

What this page does not claim

The declaration does not prove that every stable closed light pattern factorizes. The declaration does not claim the neutral unit load condition is necessary for factorization. The declaration does not address the physical bridge from recognition to linking.

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