Masses Mass Genesis Pattern Readout Equivalence Pattern Single Source Equivalenc

The single-source readout

Inertial mass resists acceleration; gravitational mass responds to gravity. Classical physics treats their equality as an experimental fact, the equivalence principle, measured to extraordinary precision. Recognition Science offers a structural reason: if both readouts are defined as measurements of the same underlying cost, equality is not an experiment but a logical consequence.

The framework's ledger, a discrete record of events, assigns a cost to each stable pattern. The declaration pattern_single_source_equivalence proves a conditional theorem: given a theory where both inertial and gravitational mass are defined as functions of that single cost source, and given a stable closed light pattern, the two readouts are equal. The proof is a short rewrite, two definitions that point at the same source, and the equality falls out. It does not define the readouts to be equal; it requires each to be proved to read the same source.

The theorem then extends. A second result, pattern_single_source_reads_restMass, shows that for a stable pattern, both readouts equal the derived rest mass. A third, pattern_single_source_identity_with_restMass, packages both equalities into one statement: inertial equals gravitational, and both equal rest mass. A fourth, pattern_single_source_identity_with_predictedMass, adds a condition: if rest mass equals the topology-derived predicted mass, then both readouts equal that predicted mass as well.

These are formal theorems in a machine-checked library of formal theorems, not empirical claims. The framework also provides a structure, StableLoadReadoutTheory, that records the proof obligations for a concrete readout to measure the integrated load. A definition converts such a theory into the single-source form, and the equality theorems apply. The abstract equivalence principle from the framework's gravity module is available here through a shifted cost construction, making the pattern-level statement consistent with the broader theory.

What the theorem does not claim is equally precise. It does not assert that any particular physical system satisfies the premise; that is a separate proof obligation. It does not derive the numerical values of particle masses. It does not say that inertial and gravitational mass are equal by definition; the structure explicitly allows them to be separately named, and the equality must be proved. The theorem is a bridge: if the single-source premise holds, the equality is forced.

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_reads_restMass
    (T : PatternSingleSourceMassTheory Λ)
    (ψ : LightPattern Λ)
    (hψ : StableClosedLightPattern ψ) :
    ReadsStablePatternLoad T.readout ψ := by
  constructor
  · rw [T.inertial_from_source ψ hψ,
        T.stable_source_is_restMass ψ hψ]
  · rw [T.gravitational_from_source ψ hψ,
        T.stable_source_is_restMass ψ 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⟩

What this page does not claim

The theorem does not prove that any particular physical system satisfies the single-source premise. The theorem does not derive numerical values for particle masses. The theorem does not define inertial and gravitational mass to be equal; it proves their equality from the premise.

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: