Masses Mass Genesis Null Vs Closed Closed Nontrivial Rest Mass Pos

Positive rest mass

In physics, rest mass is the mass an object has when it is not moving. The Recognition Science framework, which models reality as a ledger (a discrete record of events), asks what kinds of patterns in that ledger can have positive rest mass. The declaration closed_nontrivial_restMass_pos answers a specific part of that question with a proved theorem.

The theorem states: if a pattern of recognition events is localized (it does not stretch out to infinity), is nontrivial (it is not just an empty or uniform background), and is closed (it repeats itself after a fixed number of ticks, here eight), then its rest mass is strictly greater than zero. In plain language, a stable, self-contained blob of activity in the ledger has weight. The proof chains together two earlier results: such a pattern is stable, and a stable closed pattern has positive rest mass.

The same module records the opposite case. A null-propagating mode, a pattern that moves outward at zero cost, has rest mass exactly zero. In the finite cyclic model used here, no such null mode can exist because every finite pattern closes after eight ticks. The framework therefore carries the null side on a separate, infinite carrier, where a zero-cost propagating mode does exist and has zero rest mass.

What the declaration does not claim is broader. It does not say that all closed patterns have positive mass; the pattern must also be localized and nontrivial. It does not assign a numerical value to any particle's mass. It does not say that the infinite null carrier is physical light; that identification is a separate modeling choice. The theorem is a structural result about the ledger, not a measurement or a prediction of specific masses.

theorem closed_nontrivial_restMass_pos
    (ψ : LightPattern Λ)
    (hloc : LocalizedSupport ψ)
    (hnontrivial : NontrivialNeutralLoad ψ) :
    0 < restMass ψ :=
  restMass_pos_of_stable ψ
    (closed_nontrivial_is_stable ψ hloc hnontrivial)

/-- The M1 null-rest-mass theorem is valid for the current predicate, but the
predicate is empty in the finite cyclic model. -/
theorem nullPropagatingMode_restMass_zero
    (ψ : LightPattern Λ) (hnull : NullPropagatingMode ψ) :
    restMass ψ = 0 :=
  restMass_eq_zero_of_null ψ hnull

/-- In the concrete finite cyclic Rhat surface, no `LightPattern` can satisfy
the current null-propagating predicate, because every finite pattern has the
eight-tick closure witness. -/
theorem no_nullPropagatingMode_for_finite_cyclic_Rhat
    (ψ : LightPattern Λ) :
    ¬ NullPropagatingMode ψ := by
  intro hnull
  exact hnull.2.1 (closedRHatOrbit_period_eight ψ)

theorem open_null_light_exists :
    ∃ γ : OpenNullLightMode, openNullRestMass γ = 0 :=
  openNullLightMode_nonempty

What this page does not claim

The theorem does not assign numerical mass values to any specific particle. The theorem does not say all closed patterns have positive mass; localization and nontriviality are required. The infinite null carrier is not identified as physical light; that is a separate modeling choice.

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/NullVsClosed.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: