Masses Mass Genesis Stable Light Pattern Nontrivial Neutral Load Evolve Pattern

The persistence of neutral patterns

In the Recognition Science framework, a light pattern is a discrete arrangement of values on a finite grid, and its evolution is a step-by-step rule that transforms one pattern into the next. The theorem nontrivialNeutralLoad_evolvePattern_iff states a precise equivalence: a pattern has a nontrivial neutral load after any number of evolution steps if and only if it had that property before the steps began. In plainer terms, if a pattern starts with a certain kind of internal balance, that balance is preserved exactly through every tick of the evolution.

The declaration is one link in a chain of results about stable patterns. A stable pattern is one that is localized, meaning it occupies only a finite region, and has a nontrivial neutral load, meaning its internal charges sum to zero without being trivially empty. The framework proves that such a pattern closes into an eight-tick orbit: after eight applications of the evolution rule, every window of the pattern returns exactly to its starting value. The theorem in question extends this to all intermediate steps, showing that the defining property of stability is not a fragile accident but an invariant of the whole cycle.

What the declaration does not claim is equally important. It does not prove that any particular pattern exists, only that if one exists, its property persists. It does not establish the quantization of particle masses into phi-rungs, nor the mass-law identity that connects rest mass to integrated load. Those remain separate targets, explicitly noted in the framework's own documentation as unproved. The theorem is a structural guarantee about the evolution of patterns already assumed to be stable, not a recipe for creating them.

The practical consequence is that the framework can treat a stable pattern as a persistent object: its support, topology labels, integrated load, and rest mass all remain unchanged under evolution. This invariance is what allows the framework to speak of a pattern as a thing with enduring identity, rather than a fleeting configuration. The theorem supplies the formal backbone for that persistence, and it does so without needing to know which specific patterns exist or what masses they carry.

theorem nontrivialNeutralLoad_evolvePattern_iff
    (ψ : LightPattern Λ) (k : ℕ) :
    NontrivialNeutralLoad (evolvePattern k ψ) ↔
      NontrivialNeutralLoad ψ := by
  constructor
  · intro h
    rcases h with ⟨x, hx, hpos⟩
    refine ⟨x, hx, ?_⟩
    have hload :=
      IndisputableMonolith.Gravity.LightMeaningProcessingBridge.cyclicShift_iter_preserves_meaningLoad
        (ψ.window x) k
    exact hload ▸ hpos
  · intro h
    rcases h with ⟨x, hx, hpos⟩
    refine ⟨x, hx, ?_⟩
    have hload :=
      IndisputableMonolith.Gravity.LightMeaningProcessingBridge.cyclicShift_iter_preserves_meaningLoad
        (ψ.window x) k
    exact hload.symm ▸ hpos

/-- 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)

@[simp] theorem evolvePattern_support
    (ψ : LightPattern Λ) (k : ℕ) :
    (evolvePattern k ψ).support = ψ.support := rfl

theorem integratedMeaningLoad_evolvePattern
    (ψ : LightPattern Λ) (k : ℕ) :
    integratedMeaningLoad (evolvePattern k ψ) =
      integratedMeaningLoad ψ :=
  integratedMeaningLoad_evolve_invariant ψ k

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 prove that any stable pattern exists, only that stability persists if present. The theorem does not establish the phi-rung quantization of particle masses. The theorem does not derive the mass-law identity connecting rest mass to integrated load.

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: