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
integratedMeaningLoad_evolvePattern · IndisputableMonolith/Masses/MassGenesis/StableLightPattern.lean:132
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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND