Masses Mass Ratios Proved

Mass ratios from the phi ladder

The MassRatiosProved module establishes the mathematical backbone for particle mass ratios in Recognition Science. It proves that when two masses are assigned to rungs on a phi-ladder, their ratio is exactly phi raised to the difference in rung numbers. This is a established theorem in Lean, not a fitted empirical relation.

The key structural result is the rung difference theorem: if mass m1 is proportional to phi^r1 and mass m2 is proportional to phi^r2, then m2/m1 equals phi^(r2-r1). This follows from the algebraic properties of powers. The module also proves a monotonicity result: a higher rung always corresponds to a higher mass, since phi is greater than one.

A concrete numerical bound is established for phi^6: it lies strictly between 17 and 18. This is derived from the defining relation phi^3 = 2*phi + 1, together with the bound 1.5 < phi < 1.62. The module packages this as a certificate structure, and proves that such a certificate exists. This gives a rigorous interval for the mass ratio between rungs differing by six steps.

These theorems are internal to the framework's structure. They do not by themselves identify which physical particle sits on which rung; that identification is a separate empirical step. What is established is the scaling law that governs ratios once the rung assignment is given.

THEOREM mass_ratio_from_rung_difference · IndisputableMonolith/Masses/MassRatiosProved.lean

THEOREM mass_ordering_from_rungs · IndisputableMonolith/Masses/MassRatiosProved.lean

THEOREM phi_6_bounds_mass_ratio · IndisputableMonolith/Masses/MassRatiosProved.lean

THEOREM mass_ratio_cert_exists · IndisputableMonolith/Masses/MassRatiosProved.lean

What this page does not claim

No specific particle masses are identified in this module. No empirical comparison against measured particle masses is made here. No claim about the physical recognition-to-linking bridge is made.

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