Masses Mass Genesis Null Vs Closed Null Propagating Mode Rest Mass Zero

Mass and the null mode

In physics, rest mass is the mass an object has when it is not moving. The Recognition Science framework models physical structure as patterns in a discrete ledger, a record of recognition events, and assigns each pattern a rest mass. Its library, a machine-checked collection of formal theorems, establishes a conditional statement: if a pattern is a null-propagating mode, a pattern that propagates at zero recognition cost, then its rest mass is zero. The theorem is named nullPropagatingMode_restMass_zero and it is a formal derivation, not a physical measurement.

The statement is conditional because the framework's concrete finite model, where patterns repeat every eight ticks, contains no such null-propagating modes at all. The library establishes this emptiness separately: every finite pattern closes into a stable loop after eight ticks, so none can satisfy the null-propagating predicate. This means the zero-rest-mass theorem holds vacuously in the finite model; it applies to a class of patterns that the model does not actually contain. The framework therefore introduces a separate open carrier, an infinite ray, to represent light-like propagation, and establishes that modes on that carrier also have zero rest mass.

The framework contrasts null modes with closed matter patterns. A closed pattern with localized support and nontrivial neutral load, meaning a pattern that is confined and carries internal structure, is stable and has positive rest mass. The library establishes this and also establishes that a stable closed pattern cannot be a null-propagating mode. The two classes are disjoint by construction: what propagates freely has no rest mass, and what has rest mass is stable and closed.

The theorem does not claim that light exists in the finite model, nor that the open carrier represents photons in the standard sense. It does not derive the numerical value of any particle mass. It establishes a structural relation within the framework: the predicate for null propagation is incompatible with positive rest mass, and the finite model realizes this by having no null modes at all. The physical bridge from these formal patterns to observed particles remains an open target, not an established result.

/-- 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 closed_nontrivial_restMass_pos
    (ψ : LightPattern Λ)
    (hloc : LocalizedSupport ψ)
    (hnontrivial : NontrivialNeutralLoad ψ) :
    0 < restMass ψ :=
  restMass_pos_of_stable ψ
    (closed_nontrivial_is_stable ψ hloc hnontrivial)

theorem stablePattern_not_nullPropagatingMode
    (ψ : LightPattern Λ) (_hstable : StableClosedLightPattern ψ) :
    ¬ NullPropagatingMode ψ :=
  no_nullPropagatingMode_for_finite_cyclic_Rhat ψ

What this page does not claim

The theorem does not establish that light exists in the finite model; it establishes the null predicate is empty there. The framework does not derive the numerical value of any particle's rest mass from this theorem. The open carrier is a formal device, not a claim about photons in standard physics.

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: