Masses Mass Genesis Conditional Certificate Rest Mass Eq Mass Law From Condition

The conditional mass law

In physics, rest mass is the mass an object has when it is not moving, and it is the same for all observers. The Recognition Science framework aims to derive this quantity from a more basic structure: a discrete record of events, called a ledger. The theorem rest_mass_eq_mass_law_from_conditional_assumptions is a precise, machine-checked statement about when this derivation works.

The theorem states that if a certain substrate, a collection of possible patterns, satisfies two specific conditions, then for any stable, closed light pattern, its rest mass equals its predicted mass. The two conditions are that the substrate has a stable topology that is load-rigid, and that every stable topology has a factorized representative. These are technical requirements about the structure of the ledger, not physical laws. The theorem is proved in the framework's machine-checked library of formal theorems, meaning the logical steps are verified by a computer.

The declaration is part of a larger effort to build a 'Mass Genesis' certificate, a complete proof that mass arises from the ledger. This particular theorem is a conditional assembly: it shows what would be true if those two assumptions were proved. It deliberately does not claim the global certificate is closed. The remaining proof burden is to derive the two assumptions from the more basic principles of the framework, which is still an open target.

In Recognition Science, the framework models mass as a property of a stable pattern in the ledger. The theorem also connects this rest mass to two other notions: inertial mass, which resists acceleration, and gravitational mass, which responds to gravity. A separate theorem in the same module shows that if a readout correctly measures the pattern's load, then all three masses are equal. This is a step toward showing that the framework's concept of mass is consistent with the classical equivalence principle.

What the theorem does not claim is that the two assumptions are true. It is a conditional statement, not an unconditional derivation of mass. The framework's larger goal remains open: proving that the two conditions hold for the actual substrate of the universe. Until then, this theorem provides a clear target and a precise statement of what remains to be shown.

theorem rest_mass_eq_mass_law_from_conditional_assumptions
    (A : ConditionalMassGenesisAssumptions Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_global_rigidity_and_representatives
    A.stable_topology_load_rigid
    A.factorized_representatives
    ψ hψ

theorem rest_mass_eq_mass_law_from_conditional_assumptions
    (A : ConditionalMassGenesisAssumptions Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_global_rigidity_and_representatives
    A.stable_topology_load_rigid
    A.factorized_representatives
    ψ hψ

structure ConditionalCertificateAssemblyCert where
  rest_mass_field :
    ∀ {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
      (_ : ConditionalMassGenesisAssumptions Λ)
      (ψ : LightPattern Λ),
      StableClosedLightPattern ψ →
      restMass ψ = predictedMass ψ
  theorem_for_readout :
    ∀ {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
      (_ : ConditionalMassGenesisAssumptions Λ)
      (readout : PatternMassReadout Λ),
      MassGenesisTheoremFor readout

theorem inertial_gravitational_identity_from_reads
    (readout : PatternMassReadout Λ) (ψ : LightPattern Λ)
    (_hψ : StableClosedLightPattern ψ)
    (hreads : ReadsStablePatternLoad readout ψ) :
    readout.inertialMass ψ = readout.gravitationalMass ψ ∧
    readout.inertialMass ψ = restMass ψ ∧
    readout.gravitationalMass ψ = restMass ψ := by
  exact ⟨hreads.1.trans hreads.2.symm, hreads.1, hreads.2⟩

What this page does not claim

The two structural assumptions are true. The global Mass Genesis certificate is closed. The framework has derived the value of any particle's rest mass from first principles.

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