Masses Mass Genesis Rest Mass Equals Mass Law Same Topology Different Load Obstr

The obstruction theorem

In the Recognition Science framework, a ledger (a discrete record of events) assigns to each stable pattern of light a rest mass and a predicted mass. The predicted mass comes from the pattern's topology, its shape and connectivity. The rest mass comes from the integrated neutral light load, the total amount of light-like activity in the pattern. The framework's mass law says these two numbers should be equal for a physically realized particle.

The theorem sameTopology_different_load_obstructs_both_realized establishes a precise obstruction. Take two stable closed patterns with the same topology but different integrated loads. Then at most one of them can satisfy the mass law; they cannot both be realized. The argument is short and exact: if both satisfied the equality, their rest masses would both equal the same predicted mass (since the topology is the same), forcing the rest masses to be equal, which contradicts the different loads.

This is a boundary result, not a construction. The framework does not yet show that any pattern satisfies the mass law. The missing piece is a realization predicate, a proof that the load is actually determined by the topology in the way the mass law requires. The theorem shows what would have to be true for that missing piece to exist: the load must be a function of the topology alone, at least for realized patterns.

For the reader, the consequence is a clear target. The framework's mass genesis is not complete; it has a conditional bridge and an obstruction. The obstruction tells you exactly what a future theorem must establish: that the load normalization is fixed by the topology. Until then, the equality between rest mass and predicted mass remains a conditional claim, not a proved law.

theorem sameTopology_different_load_obstructs_both_realized
    {ψ χ : LightPattern Λ}
    (hψstable : StableClosedLightPattern ψ)
    (hχstable : StableClosedLightPattern χ)
    (htop : SameTopology ψ χ)
    (hload : integratedMeaningLoad ψ ≠ integratedMeaningLoad χ) :
    ¬ (MassLawLoadRealized ψ ∧ MassLawLoadRealized χ) := by
  intro hboth
  have hrest_ne : restMass ψ ≠ restMass χ := by
    intro hrest
    rw [restMass_eq_integratedMeaningLoad_of_stable ψ hψstable,
        restMass_eq_integratedMeaningLoad_of_stable χ hχstable] at hrest
    exact hload hrest
  exact sameTopology_different_restMass_obstructs_both_realized htop hrest_ne
    ⟨restMass_eq_predictedMass_of_load_realized ψ hψstable hboth.1,
     restMass_eq_predictedMass_of_load_realized χ hχstable hboth.2⟩

theorem sameTopology_realized_patterns_have_same_restMass
    {ψ χ : LightPattern Λ}
    (htop : SameTopology ψ χ)
    (hψ : restMass ψ = predictedMass ψ)
    (hχ : restMass χ = predictedMass χ) :
    restMass ψ = restMass χ := by
  rw [hψ, hχ]
  exact predictedMass_eq_of_sameTopology htop

What this page does not claim

The theorem does not prove that any pattern satisfies the mass law. The theorem does not claim that different topologies must have different loads. The theorem does not identify which of two same-topology patterns is the realized one.

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