Masses Mass Law Predict Mass Pos

A guarantee of positivity

In physics, a mass is a positive quantity. No known particle has a negative mass, and any formula that could produce one would be suspect. The Recognition Science framework's ledger, a discrete record of recognition events, models stable particles as occupying rungs on a ladder indexed by the golden ratio φ. The framework's library, a machine-checked collection of formal theorems, proves that its master mass formula always yields a positive result for any valid configuration of sector, rung, and charge shift.

The master mass formula is m = yardstick(Sector) × φ^(r − 8 + gap(Z)). Here yardstick(Sector) is a sector-specific prefactor, r is an integer rung position, 8 is the fundamental cycle period, and gap(Z) is a correction term depending on a charge-based shift index Z. The theorem predict_mass_pos states that for any sector s, any integer rung r, and any integer charge shift Z_val, the predicted mass is strictly greater than zero. The proof is not a numerical check; it is a formal derivation in the machine-checked library, meaning the result holds for all inputs, not just a sampled set.

The positivity theorem is a consistency result, not a prediction of a specific mass value. It does not say which rung a particular particle occupies, nor what the yardstick for a sector is. Those are separate modeling choices. What the theorem guarantees is that the formula's structure cannot produce a negative or zero mass, a necessary condition for any credible mass formula. This is the kind of foundational sanity check that underpins the framework's larger claims about deriving particle masses from first principles.

In Recognition Science, the theorem is one link in a chain that forces the golden ratio, an eight-tick cycle, and three spatial dimensions. The mass law itself is a model, a definitional choice about how mass relates to recognition states, not a derived theorem. The positivity proof, however, is a theorem about that model: it shows the model is internally consistent in a basic but essential way. This distinction matters. A model can be wrong about the world while still being internally consistent, and the library does not claim otherwise.

What the theorem does not claim is equally important. It does not assert that the predicted masses match measured particle masses. That comparison is an empirical check, not a formal result. It does not claim that every rung integer corresponds to a real particle; the formula defines a mass for any integer, but which rungs are physically realized is a separate question. And it does not claim that the yardstick values are known; they are parameters of the model, not outputs of the theorem.

/-- Mass is positive for any valid configuration. -/
theorem predict_mass_pos (s : Sector) (r : ℤ) (Z_val : ℤ) :
    predict_mass s r Z_val > 0 := by
  unfold predict_mass
  apply mul_pos
  · -- yardstick is positive
    unfold yardstick Anchor.E_coh
    apply mul_pos
    · apply mul_pos
      · exact zpow_pos (by norm_num) (B_pow s)
      · exact zpow_pos phi_pos (-5 : ℤ)
    · exact zpow_pos phi_pos (r0 s)
  · -- phi^... is positive
    exact Real.rpow_pos_of_pos phi_pos _

/-- **THE MASTER MASS LAW**
    Predicts the mass of a species in a given sector. -/
noncomputable def predict_mass (sector : Sector) (rung : ℤ) (Z_val : ℤ) : ℝ :=
  yardstick sector * (phi ^ ((rung : ℝ) - 8 + gap_correction Z_val))

/-- Mass is positive for any valid configuration. -/
theorem predict_mass_pos (s : Sector) (r : ℤ) (Z_val : ℤ) :
    predict_mass s r Z_val > 0 := by
  unfold predict_mass
  apply mul_pos
  · -- yardstick is positive
    unfold yardstick Anchor.E_coh
    apply mul_pos
    · apply mul_pos
      · exact zpow_pos (by norm_num) (B_pow s)
      · exact zpow_pos phi_pos (-5 : ℤ)
    · exact zpow_pos phi_pos (r0 s)
  · -- phi^... is positive
    exact Real.rpow_pos_of_pos phi_pos _

What this page does not claim

The predicted masses match measured particle masses. Every rung integer corresponds to a real particle. The yardstick values are known or derived.

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