Masses Mass Genesis Pattern Readout Equivalence Stable Load Readout Theory Ident

The readout identity

In classical physics, inertial mass and gravitational mass are two different properties. Inertial mass is how strongly an object resists a change in motion; gravitational mass is how strongly it responds to a gravitational field. Newton's laws treat them as separate, and only experiment shows they match. The equivalence principle, a central idea of general relativity, elevates that match to a postulate.

In the Recognition Science framework, the two readouts are not defined to be equal. Instead, the framework models a ledger, a discrete record of events, as the single source of both. The declaration stableLoadReadoutTheory_identity is a theorem in the framework's machine-checked library of formal theorems. It proves that if both readouts are required to measure the same integrated load, the total cost recorded in that ledger, then for any stable pattern, the inertial and gravitational readouts are equal, and both equal the rest mass derived from that same source.

The proof works by construction. The framework defines a structure that carries the two readouts and the two proof obligations: inertial mass reads the integrated load, and gravitational mass reads the same integrated load. From those two obligations alone, the theorem derives the equality. It does not need to define the readouts as equal; it only needs the evidence that each one reads the same underlying cost source.

What the theorem does not claim is just as important. It does not prove that any actual physical system satisfies those readout obligations. It proves a conditional: if a system is modeled with both readouts tied to one ledger, then the readouts agree. The framework's library also contains a separate theorem showing that when the rest mass equals a topology-derived predicted mass, the readouts match that predicted value as well, but again only under the same stable-pattern condition.

The consequence is a sharpened statement of the equivalence principle within the framework. Instead of assuming inertial and gravitational mass are equal, the framework shows the equality follows from a single-source assumption. The reader can now see the exact evidence object required to close the loop, and what remains open is whether any real pattern satisfies that evidence.

theorem stableLoadReadoutTheory_identity
    (T : StableLoadReadoutTheory Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ) :
    T.readout.inertialMass ψ = T.readout.gravitationalMass ψ ∧
    T.readout.inertialMass ψ = restMass ψ ∧
    T.readout.gravitationalMass ψ = restMass ψ :=
  pattern_single_source_identity_with_restMass
    (stableLoadReadoutTheory_to_singleSource T) ψ hψ

theorem stableLoadReadoutTheory_identity
    (T : StableLoadReadoutTheory Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ) :
    T.readout.inertialMass ψ = T.readout.gravitationalMass ψ ∧
    T.readout.inertialMass ψ = restMass ψ ∧
    T.readout.gravitationalMass ψ = restMass ψ :=
  pattern_single_source_identity_with_restMass
    (stableLoadReadoutTheory_to_singleSource T) ψ hψ

theorem stableLoadReadoutTheory_identity
    (T : StableLoadReadoutTheory Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ) :
    T.readout.inertialMass ψ = T.readout.gravitationalMass ψ ∧
    T.readout.inertialMass ψ = restMass ψ ∧
    T.readout.gravitationalMass ψ = restMass ψ :=
  pattern_single_source_identity_with_restMass
    (stableLoadReadoutTheory_to_singleSource T) ψ hψ

What this page does not claim

The theorem does not establish that inertial and gravitational mass are equal in any actual physical system. The theorem does not define the two readouts to be equal; it derives equality from a shared source assumption. The theorem does not show that the predicted mass equals the rest mass; that is a separate theorem with its own condition.

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