Encyclopedia Masses Masses Mass Genesis Stable Light Pattern Rest Mass Evolve Pattern Of Stable
ARTICLE 4 claims 3 theorems 1 model
Masses Mass Genesis Stable Light Pattern Rest Mass Evolve Pattern Of Stable
Rest mass in this framework is a conserved quantity: a stable pattern's mass does not change as it evolves through its eight-step cycle.
Rest mass as an invariant
Rest mass is a property that does not change when a system evolves, provided the system is stable. The Recognition Science framework expresses this through a machine-checked theorem about its model of light patterns. A light pattern is a discrete configuration of values on a finite grid, and its evolution is a step-by-step shift of those values. The theorem states that if a pattern is stable, meaning it is localized, carries nontrivial neutral load, and closes into an eight-step orbit, then its rest mass after any number of evolution steps equals its rest mass at the start.
The proof is direct. Stability gives the pattern a closed eight-step orbit, and the evolution operation preserves the pattern's support, topology labels, sector, rung, and integrated load. Rest mass for a stable pattern is defined as that integrated load, so preserving the load preserves the mass. The theorem appears in the framework's library as restMass_evolvePattern_of_stable, and it is a proved result, not a hypothesis.
This invariant matters because it gives the framework a conservation law: stable things keep their identity over time. It is a structural fact about the model, not a statement about any specific particle. The theorem does not claim that rest mass takes particular values, nor that it follows a golden-ratio ladder. Those are separate claims. It also does not claim that unstable patterns conserve mass; the invariant applies only to stable ones.
A reader should take away a precise picture: within this model, stability and rest mass are linked. If a pattern is stable, its mass is a fixed number through all evolution steps. The framework proves this as a closed result, and it is a building block for later work on mass generation.
MODEL evolvePattern_support · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.lean
@[simp] theorem evolvePattern_support
(ψ : LightPattern Λ) (k : ℕ) :
(evolvePattern k ψ).support = ψ.support := rfl
THEOREM restMass_evolvePattern_of_stable · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.lean
theorem restMass_evolvePattern_of_stable
(ψ : LightPattern Λ) (k : ℕ)
(hψ : StableClosedLightPattern ψ) :
restMass (evolvePattern k ψ) = restMass ψ := by
have h_ev := stable_evolvePattern_of_stable ψ k hψ
rw [restMass_eq_integratedMeaningLoad_of_stable (evolvePattern k ψ) h_ev,
restMass_eq_integratedMeaningLoad_of_stable ψ hψ,
integratedMeaningLoad_evolvePattern ψ k]
THEOREM stable_closed_orbit · evolvePattern_support · evolvePattern_topology · sectorOf_evolvePattern · rungOf_evolvePattern · integratedMeaningLoad_evolvePattern · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.lean
theorem stable_closed_orbit
(ψ : LightPattern Λ) (hψ : StableClosedLightPattern ψ) :
ClosedRHatOrbit ψ :=
hψ.2.2
@[simp] theorem evolvePattern_support
(ψ : LightPattern Λ) (k : ℕ) :
(evolvePattern k ψ).support = ψ.support := rfl
@[simp] theorem evolvePattern_topology
(ψ : LightPattern Λ) (k : ℕ) :
(evolvePattern k ψ).topology = ψ.topology := rfl
@[simp] theorem sectorOf_evolvePattern
(ψ : LightPattern Λ) (k : ℕ) :
sectorOf (evolvePattern k ψ) = sectorOf ψ := rfl
@[simp] theorem rungOf_evolvePattern
(ψ : LightPattern Λ) (k : ℕ) :
rungOf (evolvePattern k ψ) = rungOf ψ := rfl
theorem integratedMeaningLoad_evolvePattern
(ψ : LightPattern Λ) (k : ℕ) :
integratedMeaningLoad (evolvePattern k ψ) =
integratedMeaningLoad ψ :=
integratedMeaningLoad_evolve_invariant ψ k
THEOREM restMass_invariant · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.lean
theorem restMass_invariant (k : ℕ) :
restMass (evolvePattern k Ψ.pattern) = restMass Ψ.pattern :=
restMass_evolvePattern_of_stable Ψ.pattern k Ψ.stable
What this page does not claim
The theorem does not assign specific numerical values to rest mass. The theorem does not apply to unstable patterns, which may change mass. The theorem does not prove the phi-rung quantization or the mass-law identity.
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/StableLightPattern.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:
- What specific values of rest mass arise from the framework's phi-rung quantization?
- How does the framework derive the mass-law identity that connects rest mass to other quantities?
- Which physical particles does the framework identify with specific stable light patterns?
- How does the framework's notion of stability relate to stability in classical physics?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
MODEL evolvePattern_support · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.lean
@[simp] theorem evolvePattern_support (ψ : LightPattern Λ) (k : ℕ) : (evolvePattern k ψ).support = ψ.support := rflA light pattern is a discrete configuration of values on a finite grid, and its evolution is a step-by-step shift of those values. evolvePattern_support · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.leanTHEOREM restMass_evolvePattern_of_stable · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.lean
theorem restMass_evolvePattern_of_stable (ψ : LightPattern Λ) (k : ℕ) (hψ : StableClosedLightPattern ψ) : restMass (evolvePattern k ψ) = restMass ψ := by have h_ev := stable_evolvePattern_of_stable ψ k hψ rw [restMass_eq_integratedMeaningLoad_of_stable (evolvePattern k ψ) h_ev, restMass_eq_integratedMeaningLoad_of_stable ψ hψ, integratedMeaningLoad_evolvePattern ψ k]The theorem states that if a pattern is stable, meaning it is localized, carries nontrivial neutral load, and closes into an eight-step orbit, then its rest mass after any number of evolution steps equals its rest mass at the start. restMass_evolvePattern_of_stable · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.leanTHEOREM stable_closed_orbit · evolvePattern_support · evolvePattern_topology · sectorOf_evolvePattern · rungOf_evolvePattern · integratedMeaningLoad_evolvePattern · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.lean
theorem stable_closed_orbit (ψ : LightPattern Λ) (hψ : StableClosedLightPattern ψ) : ClosedRHatOrbit ψ := hψ.2.2@[simp] theorem evolvePattern_support (ψ : LightPattern Λ) (k : ℕ) : (evolvePattern k ψ).support = ψ.support := rfl@[simp] theorem evolvePattern_topology (ψ : LightPattern Λ) (k : ℕ) : (evolvePattern k ψ).topology = ψ.topology := rfl@[simp] theorem sectorOf_evolvePattern (ψ : LightPattern Λ) (k : ℕ) : sectorOf (evolvePattern k ψ) = sectorOf ψ := rfl@[simp] theorem rungOf_evolvePattern (ψ : LightPattern Λ) (k : ℕ) : rungOf (evolvePattern k ψ) = rungOf ψ := rfltheorem integratedMeaningLoad_evolvePattern (ψ : LightPattern Λ) (k : ℕ) : integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ := integratedMeaningLoad_evolve_invariant ψ kStability gives the pattern a closed eight-step orbit, and the evolution operation preserves the pattern's support, topology labels, sector, rung, and integrated load. stable_closed_orbit · evolvePattern_support · evolvePattern_topology · sectorOf_evolvePattern · rungOf_evolvePattern · integratedMeaningLoad_evolvePattern · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.leanTHEOREM restMass_invariant · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.lean
theorem restMass_invariant (k : ℕ) : restMass (evolvePattern k Ψ.pattern) = restMass Ψ.pattern := restMass_evolvePattern_of_stable Ψ.pattern k Ψ.stableRest mass for a stable pattern is defined as that integrated load, so preserving the load preserves the mass. restMass_invariant · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.lean