Masses Verification

Masses verification

Masses verification is the recognition-science practice of testing the framework's particle mass ladder against the measured values compiled by the Particle Data Group (PDG). The ladder is a consequence of the forcing chain: particle masses are predicted to sit at powers of the golden ratio phi, times a sector-specific scale. The verification module in Lean 4 checks that these predicted values land near the experimental numbers, and it does so with proofs, not with curve fitting.

The module's central objects are the experimental masses themselves, which are imported constants, and the predicted masses, which are definitions built from phi. For the lepton sector, the prediction for a rung r is phi^(57+r) divided by 2^22 and by 10^6, in MeV. The module proves that the electron, muon, and tau predictions equal this formula at their respective rungs. It then proves relative error bounds: the muon prediction is within 4 percent of the measured muon mass, and the proton binding energy prediction is within 3.5 percent of the measured proton mass.

The verification also checks ratios. The measured muon-to-electron mass ratio is established to lie between 206.76 and 206.77, while the tau-to-electron ratio is established to lie between 3477 and 3478. These measured ratios sit on opposite sides of the nearest integer powers of phi, a fact the module records as an undershoot for the muon and an overshoot for the tau. For the quark sector, the module proves that the predicted charm-to-up ratio is exactly phi^11 and the predicted top-to-charm ratio is exactly phi^6. These ratio theorems are exact statements about the definitions; they do not depend on the experimental values.

The epistemological status of the module is explicit: the experimental masses are imported constants, not derived from recognition science. The comparison is therefore an empirical check of the ladder, not a derivation of the masses themselves. What the module establishes is that the phi-power ladder, with its fixed sector scales, produces numbers that sit within a few percent of the measured values, and that the exact power ratios among the quark predictions are theorems of the definitions.

THEOREM muon_relative_error · IndisputableMonolith/Masses/Verification.lean

THEOREM proton_relative_error · IndisputableMonolith/Masses/Verification.lean

THEOREM ratio_mu_e_exp_bounds · IndisputableMonolith/Masses/Verification.lean

THEOREM charm_up_ratio · IndisputableMonolith/Masses/Verification.lean

THEOREM top_charm_ratio · IndisputableMonolith/Masses/Verification.lean

What this page does not claim

This answer does not claim that the experimental masses are derived from recognition science; they are imported constants. This answer does not claim that the mass predictions are exact; the module proves only relative error bounds and exact ratios among definitions. This answer does not claim that the phi-power ladder is the only possible mass formula consistent with the data.

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