Masses Mass Genesis Pattern Readout Equivalence

The single-source mass theorem

In physics, inertial mass measures how much an object resists acceleration, while gravitational mass measures how strongly it responds to a gravitational field. The equivalence principle, a central idea of general relativity, asserts these two quantities are equal. The framework's machine-checked library of formal theorems proves this equality as a consequence of a deeper structure: if both masses are read from the same underlying cost source, their values must coincide.

The classical statement is well established. Newton's second law ties inertial mass to force and acceleration; Newton's law of gravitation ties gravitational mass to the force between bodies. Experiments from Galileo's leaning tower to modern torsion balances have confirmed their proportionality to extraordinary precision. The framework's contribution is not a new measurement but a formal derivation: it shows the equality follows necessarily from the assumption that both readouts draw on a single source.

In Recognition Science, the framework models mass as a readout of a pattern's cost, where cost is the forced price of recognizing a stable pattern. The module introduces a structure, PatternSingleSourceMassTheory, which records the proof obligations: each readout must be shown to read the same stable-pattern cost source, and that source must be the derived rest mass. The central theorem, pattern_single_source_equivalence, then proves that for any stable closed light pattern, the inertial and gravitational readouts are equal.

The proof is short and direct. It rewrites each readout using its defining equation to the shared source, then observes the two expressions are identical. A second theorem, pattern_single_source_identity_with_restMass, strengthens this: both readouts also equal the rest mass itself. When a further condition holds, namely that rest mass equals the topology-derived predicted mass, both readouts equal that predicted value as well.

The module also connects this pattern-level result to the abstract equivalence principle already proved in the framework's gravity module. It constructs a shifted source mass theory that satisfies the abstract theorem's hypotheses, showing the pattern-level statement is a faithful instance of the more general principle. This bridges the gap between the abstract cost formalism and the concrete pattern readouts used in mass genesis.

What this establishes in plain language: the framework does not define the two masses to be equal. It proves that if both are read from the same cost source, equality is forced. This is a theorem, not a postulate. The structure merely records what must be shown; the proof supplies the result. The module provides the exact evidence object needed for the mass genesis story, showing the two readouts agree and both agree with the derived rest mass.

theorem pattern_single_source_equivalence
    (T : PatternSingleSourceMassTheory Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ) :
    T.readout.inertialMass ψ = T.readout.gravitationalMass ψ := by
  rw [T.inertial_from_source ψ hψ,
      T.gravitational_from_source ψ hψ]

theorem pattern_single_source_identity_with_restMass
    (T : PatternSingleSourceMassTheory Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ) :
    T.readout.inertialMass ψ = T.readout.gravitationalMass ψ ∧
    T.readout.inertialMass ψ = restMass ψ ∧
    T.readout.gravitationalMass ψ = restMass ψ := by
  have hreads := pattern_single_source_reads_restMass T ψ hψ
  exact ⟨pattern_single_source_equivalence T ψ hψ, hreads.1, hreads.2⟩

/-- If M7 is closed for the pattern, the two readouts also equal the
topology-derived MassLaw value. -/
theorem pattern_single_source_identity_with_predictedMass
    (T : PatternSingleSourceMassTheory Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ)
    (hM7 : restMass ψ = predictedMass ψ) :
    T.readout.inertialMass ψ = predictedMass ψ ∧
    T.readout.gravitationalMass ψ = predictedMass ψ := by
  have hreads := pattern_single_source_reads_restMass T ψ hψ
  exact ⟨hreads.1.trans hM7, hreads.2.trans hM7⟩

theorem abstract_equivalence_principle_available_for_pattern
    (T : PatternSingleSourceMassTheory Λ)
    (ψ : LightPattern Λ) :
    (shiftedSourceMassTheory T ψ).inertial_mass 1 =
      (shiftedSourceMassTheory T ψ).gravitational_mass 1 :=
  Gravity.EquivalencePrinciple.single_source_equivalence
    (shiftedSourceMassTheory T ψ) 1 zero_lt_one

What this page does not claim

This does not claim the framework defines the two masses to be equal; it proves equality follows from a shared source. This does not claim the equivalence principle is a new physical postulate; it is a derived theorem within the framework. This does not claim any specific numerical value for any particle mass; the module concerns structural identity, not numerical prediction.

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: