Masses Mass Genesis Conditional Certificate Conditional Mass Genesis Assumptions

Conditional mass genesis

In physics, rest mass is the mass an object has when it is not moving, and gravitational mass is the property that determines how strongly it feels gravity. The equality of these two masses, known as the equivalence principle, is a central idea in general relativity. The Recognition Science framework attempts to derive this equality from a more fundamental model of reality as a discrete record of events, called a ledger. Its machine-checked library of formal theorems contains a declaration that shows exactly how much of this derivation is complete and how much remains open.

The declaration is called ConditionalMassGenesisAssumptions, and it is a formal structure that packages two assumptions. The first, stable_topology_load_rigid, asserts that the topology of a stable pattern is rigidly determined by its load. The second, factorized_representatives, asserts that every stable topology has a factorized representative. These are technical conditions about the internal structure of light patterns in the framework, where a light pattern is a discrete configuration of events in the ledger.

What the declaration establishes is a conditional theorem: if these two assumptions hold for a given substrate, then the framework proves that for every stable closed light pattern, the rest mass equals the predicted mass, and both equal the inertial and gravitational masses read out by any admissible measurement. This is a genuine theorem in the library, with no gaps in its logical derivation. It also proves that the readout's inertial mass equals its gravitational mass, and that both equal the rest mass, for any pattern that satisfies the stability condition.

However, the declaration deliberately does not claim that these two assumptions are true. The library's own documentation states that the global certificate is not closed, and that the remaining proof burden is the bottom-up derivation of the two assumptions. In other words, the framework has built a bridge that would complete the mass genesis story, but the bridge's foundations on one side are still under construction. The conditional theorem is a precise statement of what would follow if those foundations were laid, not a claim that they have been.

This matters because it shows the difference between a proved implication and a proved fact. The framework's library has proved that the equivalence principle follows from its structural assumptions, but it has not proved those assumptions themselves. A reader should understand that the declaration is a powerful conditional result, not a completed derivation of mass from the ledger. The open work is clearly identified: proving the two assumptions on a specific substrate would close the remaining gap and turn the conditional theorem into an unconditional one.

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ψ

/-- Fixed-substrate conditional Mass Genesis theorem. Once M7's two remaining
assumptions are proved on `Λ`, every admissible readout satisfies the original
M1 theorem surface. -/
theorem massGenesisTheoremFor_of_conditional_assumptions
    (A : ConditionalMassGenesisAssumptions Λ)
    (readout : PatternMassReadout Λ) :
    MassGenesisTheoremFor readout := by
  intro ψ
  exact closedPatternMassConclusion_of_conditional_assumptions A 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⟩

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

What this page does not claim

The declaration does not prove that the two assumptions hold for any actual substrate. The declaration does not claim that the global MassGenesisCertificate is closed. The declaration does not assert that the equivalence principle has been derived from the ledger without any remaining assumptions.

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: