Masses Mass Genesis Stable Light Pattern Stable Iff Localized Nontrivial

The stability condition

In the Recognition Science framework, a light pattern (a discrete record of events on a cyclic grid) evolves by a fixed rule called Rhat, which shifts the pattern through eight positions before returning to the start. The framework's library, a machine-checked collection of formal theorems, proves a clean characterization: a light pattern is stable exactly when it has two properties. First, it is localized, meaning its activity is confined to a finite region rather than spread everywhere. Second, it is nontrivial in a specific sense, carrying a neutral load that is not zero.

The theorem stable_iff_localized_nontrivial states this equivalence formally: a pattern is a stable closed light pattern if and only if it has localized support and a nontrivial neutral load. The forward direction, that every stable pattern must be localized and nontrivial, follows from the definition of stability itself. The reverse direction, that any pattern with these two properties is stable, is the substantive result. It relies on a separate proved fact that every light pattern closes after exactly eight applications of the cyclic-shift evolution, a periodicity that gives the closed orbit.

This matters because it reduces a complex dynamical condition to two checkable properties. The library also shows that evolution preserves these properties: a stable pattern stays stable under the shift, and its rest mass, the framework's analogue of mass, remains constant. The theorem gives a concrete handle on which patterns persist and which do not, a first structural step in the framework's account of how stable particles emerge from underlying light patterns.

The theorem does not claim that these stable patterns have specific masses. The library explicitly states it does not prove phi-rung quantization or the mass-law identity, which would assign numerical masses to patterns. It also does not claim that the eight-tick periodicity holds for any evolution other than the concrete cyclic-shift Rhat used here. The result is about the structure of stability, not about the values that stable patterns carry.

/-- For the concrete eight-tick Rhat, stability reduces to locality plus
nontrivial neutral load. Later Rhat refinements can replace the closure
lemma without changing the downstream API. -/
theorem stable_iff_localized_nontrivial (ψ : LightPattern Λ) :
    StableClosedLightPattern ψ ↔
      LocalizedSupport ψ ∧ NontrivialNeutralLoad ψ := by
  constructor
  · intro hψ
    exact ⟨hψ.1, hψ.2.1⟩
  · intro hψ
    exact stable_of_localized_nontrivial ψ hψ.1 hψ.2

/-- Every light pattern closes after the concrete eight-tick cyclic-shift
Rhat evolution. This is the structural orbit-closure input for M2. -/
theorem closedRHatOrbit_period_eight (ψ : LightPattern Λ) :
    ClosedRHatOrbit ψ := by
  refine ⟨8, by norm_num, dvd_refl 8, ?_⟩
  intro x _hx
  exact cyclicShift_period_8 (ψ.window x)

theorem stable_evolvePattern_of_stable
    (ψ : LightPattern Λ) (k : ℕ)
    (hψ : StableClosedLightPattern ψ) :
    StableClosedLightPattern (evolvePattern k ψ) := by
  exact stable_of_localized_nontrivial (evolvePattern k ψ)
    (by simpa [LocalizedSupport, evolvePattern] using hψ.1)
    ((nontrivialNeutralLoad_evolvePattern_iff ψ k).2 hψ.2.1)

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]

What this page does not claim

The theorem does not assign numerical masses to stable patterns, nor does it prove phi-rung quantization or the mass-law identity. The eight-tick closure is proved only for the concrete cyclic-shift Rhat, not for any other evolution rule. The stability result does not establish that all light patterns are stable, only those with the two stated properties.

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: