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

The obstruction

In the Recognition Science account, mass is not a free parameter. A stable closed pattern of light, called a light pattern, carries a rest mass measured by its integrated neutral load, and a predicted mass computed from topology-derived labels. The framework's library proves a conditional bridge: if a stable pattern's load realizes the mass-law value, then its rest mass equals its predicted mass. The declaration sameTopology_different_restMass_obstructs_both_realized states the sharp obstruction: two patterns with the same topology but different rest masses cannot both satisfy that equality.

Why this matters: the topology alone fixes the predicted mass. The theorem predictedMass_eq_of_sameTopology proves that two patterns with the same topology have equal predicted masses. If both also had rest masses equal to that common predicted value, their rest masses would be equal. The obstruction theorem is the contrapositive: different rest masses rule out both being realized. It is a no-smuggling result, preventing an unproved assumption about load normalization from hiding inside the equality claim.

The theorem does not say that same-topology patterns must have equal rest masses. Arbitrary amplitudes are permitted, so rest masses can differ. It does not prove that any pattern satisfies the mass-law equality; that requires the missing realization predicate, MassLawLoadRealized, which remains an open condition. The obstruction only constrains the set of simultaneously realized patterns, not the values themselves.

theorem sameTopology_different_restMass_obstructs_both_realized
    {ψ χ : LightPattern Λ}
    (htop : SameTopology ψ χ)
    (hdiff : restMass ψ ≠ restMass χ) :
    ¬ (restMass ψ = predictedMass ψ ∧ restMass χ = predictedMass χ) := by
  intro hboth
  exact hdiff
    (sameTopology_realized_patterns_have_same_restMass htop hboth.1 hboth.2)

theorem predictedMass_eq_of_sameTopology
    {ψ χ : LightPattern Λ} (h : SameTopology ψ χ) :
    predictedMass ψ = predictedMass χ := by
  unfold predictedMass
  rw [sectorOf_eq_of_sameTopology h,
      rungOf_eq_of_sameTopology h,
      ZOf_eq_of_sameTopology h]

theorem restMass_eq_predictedMass_of_load_realized
    (ψ : LightPattern Λ)
    (hstable : StableClosedLightPattern ψ)
    (hrealized : MassLawLoadRealized ψ) :
    restMass ψ = predictedMass ψ := by
  rw [restMass_eq_integratedMeaningLoad_of_stable ψ hstable]
  exact hrealized

What this page does not claim

The theorem does not prove that any pattern satisfies restMass = predictedMass. The theorem does not imply that same-topology patterns must have equal rest masses. The theorem does not establish the missing realization predicate MassLawLoadRealized.

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: