Encyclopedia Masses Masses Mass Genesis Theorem Statement Raw Stable Mass Genesis First Principles T

ARTICLE 3 claims 3 theorems

Masses Mass Genesis Theorem Statement Raw Stable Mass Genesis First Principles T

A machine-checked library states the exact conditions under which a stable light pattern would count as having mass, without yet proving any such pattern exists.

The mass target

In physics, mass is a property of matter that resists acceleration and generates gravitational attraction. The Recognition Science framework aims to derive this property from a more basic picture, in which reality keeps a discrete record of recognition events, and patterns of light-like states carry the physical content. The declaration rawStableMassGenesisFirstPrinciplesTarget_of_admissibleCoverage fixes the first-principles target for this derivation: it states, as a formal proposition, that for any admissible collection of light patterns, every stable closed light pattern has a well-defined inertial and gravitational mass equal to its rest mass. Rest mass here is defined as the integrated load of the pattern when it is stable, and zero otherwise.

The declaration does not close the bridge. It is a statement of what must be proved, not a proof that the bridge is crossed. The central claim remains a surface of certificates whose hard fields must be filled in bottom-up from the framework's cost function, stability conditions, topology, and the golden-ratio forcing that yields the eight-tick cycle. Reverse reconstruction from known masses is deliberately absent from the canonical statement; it may suggest later lemmas, but it cannot discharge any field below. The theorem statement is the landing surface, not the landing.

What the library does establish, with machine-checked proofs, is the scaffolding around the target. It proves that a predicted mass is always positive, that a null propagating mode has zero rest mass, and that a stable closed light pattern has rest mass equal to its integrated meaning load. These are the consistency conditions that any successful mass-genesis proof must satisfy. They do not yet show that any stable closed light pattern exists, nor that the framework's predicted masses match the measured particle spectrum. Those remain open targets, to be reached by proving the certificate fields from the framework's axioms.

THEOREM MassGenesisTheoremFor · IndisputableMonolith/Masses/MassGenesis/TheoremStatement.lean
/-- M1 target theorem surface for a substrate and its canonical mass readout. -/
def MassGenesisTheoremFor
    (readout : PatternMassReadout Λ) : Prop :=
  ∀ ψ : LightPattern Λ, ClosedPatternMassConclusion readout ψ
THEOREM restMass_eq_integratedMeaningLoad_of_stable · restMass_eq_zero_of_not_stable · IndisputableMonolith/Masses/MassGenesis/TheoremStatement.lean
restMass_eq_integratedMeaningLoad_of_stable · IndisputableMonolith/Masses/MassGenesis/TheoremStatement.lean:227
theorem restMass_eq_integratedMeaningLoad_of_stable
    (ψ : LightPattern Λ) (hψ : StableClosedLightPattern ψ) :
    restMass ψ = integratedMeaningLoad ψ := by
  classical
  simp [restMass, hψ]
theorem restMass_eq_zero_of_not_stable
    (ψ : LightPattern Λ) (hψ : ¬ StableClosedLightPattern ψ) :
    restMass ψ = 0 := by
  classical
  simp [restMass, hψ]
THEOREM predictedMass_pos · restMass_eq_zero_of_null · restMass_eq_integratedMeaningLoad_of_stable · IndisputableMonolith/Masses/MassGenesis/TheoremStatement.lean
theorem predictedMass_pos (ψ : LightPattern Λ) :
    0 < predictedMass ψ :=
  MassLaw.predict_mass_pos (sectorOf ψ) (rungOf ψ) (ZOf ψ)
theorem restMass_eq_zero_of_null
    (ψ : LightPattern Λ) (hψ : NullPropagatingMode ψ) :
    restMass ψ = 0 :=
  restMass_eq_zero_of_not_stable ψ (not_stable_of_null ψ hψ)
restMass_eq_integratedMeaningLoad_of_stable · IndisputableMonolith/Masses/MassGenesis/TheoremStatement.lean:227
theorem restMass_eq_integratedMeaningLoad_of_stable
    (ψ : LightPattern Λ) (hψ : StableClosedLightPattern ψ) :
    restMass ψ = integratedMeaningLoad ψ := by
  classical
  simp [restMass, hψ]

What this page does not claim

The mass-genesis bridge is closed and stable light patterns are proved to exist. The framework's predicted masses match any measured particle masses. Reverse reconstruction from known masses is part of the canonical statement.

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/TheoremStatement.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