Masses Mass Genesis Refined Stable Carrier Full Chain For Stable Load Readout

The mass readout chain

In classical physics, the equality of inertial mass and gravitational mass is the weak equivalence principle, a principle of general relativity tested to extraordinary precision. The Recognition Science framework approaches this from a different direction: it defines mass as a property of stable, closed patterns of light, and asks what theorems follow from that definition alone. The declaration full_chain_for_stableLoadReadout is the capstone of this effort, a machine-checked theorem in the framework's library of formal proofs that assembles the entire chain of mass properties for a specific, refined class of patterns.

The chain begins with a stable closed light pattern, a discrete record of light events that persists under the framework's evolution rule. The raw notion of stability is too broad: it permits amplitude variation at fixed topology, which the framework's obstruction module shows is incompatible with a unique mass assignment. The refined carrier, a TopologyNormalizedStablePattern, adds a factorized topology load-density as proof evidence, not as a reverse fit. The theorem then establishes, for any such pattern and any stable load readout theory, six properties simultaneously: the integrated meaning load is invariant under evolution, the rest mass is positive, the mass is quantized on the golden-ratio rung ladder, the rest mass equals the predicted mass from the mass law, and both the inertial and gravitational mass readouts equal the rest mass.

The force of the theorem is the conjunction. It does not merely assert one identity; it derives them all from the same structural assumptions, and it does so in a way that a proof assistant has checked step by step. The readout identity, in particular, is a formal statement of the weak equivalence principle for these patterns: the inertial mass and gravitational mass readouts agree, and both agree with the rest mass. This is not an empirical measurement or a numerical coincidence; it is a logical consequence of the definitions, holding for every pattern in the refined class.

What the theorem does not claim is equally important. It does not claim that every stable closed light pattern satisfies these properties; the obstruction theorem explicitly shows that a same-topology pair with different loads refutes the all-raw-stable construction target. It does not claim that the refined carrier has been physically constructed from the underlying dynamics; the docstring states plainly that deriving the density field from Q3/Rhat/CP6 dynamics remains an open construction problem. And it does not claim that the framework's mass values match measured particle masses; that comparison is an empirical check, not a theorem. The chain is a conditional guarantee: if a pattern carries the refined admissibility evidence, then the full mass readout chain holds.

theorem full_chain_for_stableLoadReadout
    (T : StableLoadReadoutTheory Λ)
    (Ψ : TopologyNormalizedStablePattern Λ) :
    (∀ k : ℕ,
      integratedMeaningLoad (evolvePattern k Ψ.pattern) =
        integratedMeaningLoad Ψ.pattern) ∧
    0 < restMass Ψ.pattern ∧
    PhiRungQuantized Ψ.pattern ∧
    restMass Ψ.pattern = predictedMass Ψ.pattern ∧
    T.readout.inertialMass Ψ.pattern = restMass Ψ.pattern ∧
    T.readout.gravitationalMass Ψ.pattern = restMass Ψ.pattern := by
  have hread := stableLoadReadoutTheory_reads_restMass T Ψ.pattern Ψ.stable
  exact
    ⟨fun k => load_invariant Ψ k,
     restMass_pos Ψ,
     phiRungQuantized Ψ,
     restMass_eq_predictedMass Ψ,
     hread.1,
     hread.2⟩

theorem readout_identity
    (T : StableLoadReadoutTheory Λ)
    (Ψ : TopologyNormalizedStablePattern Λ) :
    T.readout.inertialMass Ψ.pattern =
        T.readout.gravitationalMass Ψ.pattern ∧
      T.readout.inertialMass Ψ.pattern = restMass Ψ.pattern ∧
      T.readout.gravitationalMass Ψ.pattern = restMass Ψ.pattern :=
  stableLoadReadoutTheory_identity T Ψ.pattern Ψ.stable

/-- The old all-raw-stable construction target is impossible in the presence of
a same-topology stable pair with different load. -/
theorem not_allStableMassAdmissible_of_sameTopology_different_load
    {ψ χ : LightPattern Λ}
    (hψ : StableClosedLightPattern ψ)
    (hχ : StableClosedLightPattern χ)
    (htop : SameTopology ψ χ)
    (hload : integratedMeaningLoad ψ ≠ integratedMeaningLoad χ) :
    ((∀ η : LightPattern Λ,
        StableClosedLightPattern η →
          MassAdmissibleStablePattern η) → False) := by
  intro Hall
  have hψM : restMass ψ = predictedMass ψ :=
    restMass_eq_predictedMass_of_massAdmissible (Hall ψ hψ)
  have hχM : restMass χ = predictedMass χ :=
    restMass_eq_predictedMass_of_massAdmissible (Hall χ hχ)
  have hrest : restMass ψ = restMass χ :=
    sameTopology_realized_patterns_have_same_restMass htop hψM hχM
  rw [restMass_eq_integratedMeaningLoad_of_stable ψ hψ,
      restMass_eq_integratedMeaningLoad_of_stable χ hχ] at hrest
  exact hload hrest

What this page does not claim

The theorem does not claim that all stable closed light patterns satisfy the mass chain; the same-topology different-load obstruction refutes that. The theorem does not claim the refined carrier has been physically constructed from underlying dynamics; deriving the density field remains open. The theorem does not claim numerical agreement with measured particle masses; that comparison is an empirical check, not a theorem.

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