Masses Basic

The mass ladder

Masses Basic is the Recognition Science module that sets up the comparison between particle masses and the framework's predicted mass ladder. It defines a surrogate ladder for the charged leptons: the electron, the muon, and the tau. Each mass is modeled as phi raised to an integer exponent, where phi is the golden ratio forced by the recognition cost function. The module does not prove the match; it records the statement and the assumption that would complete it.

The ladder uses two exponent differences. The muon-to-electron step is exponent 11, and the tau-to-muon step is exponent 6. These exponents are a paper placeholder, a definitional choice, not a derived result. The module then defines what it would mean for the ladder to match the Particle Data Group measurements: for every imported measurement, the measured value must lie within its stated error of phi raised to the assigned exponent.

The central lemma, mass_ladder_holds, states that the ladder matches the PDG values when an external assumption, mass_ladder_assumption, is supplied. The proof is exactly that assumption; the lemma is a restatement. The pending proof note says the real work relies on that assumption. So the module establishes the form of the claim, not its truth. The scaling law behind the phi-power ladder is established elsewhere in the framework; the agreement with measured masses remains an empirical check, not a theorem.

MODEL rung_exponent · IndisputableMonolith/Masses/Basic.lean

MODEL rung_exponent · IndisputableMonolith/Masses/Basic.lean

MODEL mass_ladder_matches_pdg · IndisputableMonolith/Masses/Basic.lean

THEOREM mass_ladder_holds · IndisputableMonolith/Masses/Basic.lean

What this page does not claim

Not claiming the mass ladder matches measured values without the pending assumption. Not claiming the rung exponents are derived from the forcing chain. Not claiming the module proves the scaling law itself.

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