Pith. sign in
module module moderate

IndisputableMonolith.Foundation.MaximalForcing.RSMassLadderUniverse

show as:
view Lean formalization →

Defines the Recognition Science mass ladder: masses sit at M0·φ^r for a yardstick M0 and integer rung r. It packages claims that the ladder ratio is forced to φ and that physical mass ratios are independent of the arbitrary yardstick. Downstream forcing-closure work cites the classifier and trichotomy that sort mass-universe claims. The argument is definitional scaffolding plus short algebraic lemmas from φ-forcing.

claimA ladder mass is $M_0\cdot\varphi^r$ for yardstick $M_0>0$ and rung $r\in\mathbb{Z}$. The mass-universe package asserts: (i) consecutive-rung ratios equal $\varphi$; (ii) ratios of ladder masses are independent of the choice of $M_0$; (iii) mass-scaling claims fall into a forced trichotomy under the Maximal Forcing classifier.

background

Recognition Science places particle masses on a discrete $\varphi$-ladder. The carrier is an overall yardstick $M_0$ (units and overall scale); the integer rung $r$ is the only dynamical index. In RS-native units the mass formula is of the shape yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$. The golden ratio $\varphi$ itself is not free: PhiForcing shows it is the unique self-similar fixed point of a discrete ledger with $J$-cost structure (forcing-chain landmark T6).

This module sits under Maximal Forcing. RealityClosure is the crown interface: it does not assert the final theorem, but states the certificate shape $\forall C\in\mathrm{ForcingClosure},P,U,,\mathrm{ClaimClassification},U,C$. Mass-ladder statements are one family of claims that certificate must classify.

Sibling definitions introduce ladderMass, ratio and yardstick claim predicates, a mass-universe bundle, and witnesses that yardstick choice drops out of ratios.

proof idea

Most of the module is definitional: ladder points, claim predicates (ladder-ratio vs yardstick), and the mass-universe record. The forced-ratio lemmas are short algebraic consequences of $\varphi$-forcing and the definition $M_0\cdot\varphi^r$. Yardstick independence is a cancellation: $(M_0\varphi^{r_1})/(M_0\varphi^{r_2})=\varphi^{r_1-r_2}$. The classifier and trichotomy route mass-universe claims into the RealityClosure certificate shape; the scaling theorem packages the yardstick-free forced ratio as the physical content.

why it matters in Recognition Science

Without a forced ladder and yardstick-free ratios, mass predictions in RS remain unit conventions rather than structural claims. This module supplies the mass-universe fragment of Maximal Forcing: it turns the primer mass formula into classified claims that RealityClosure can accept or reject. It depends on PhiForcing (T6: $\varphi$ forced by self-similarity) and feeds the crown closure certificate interface. No downstream Lean users are wired yet in the graph; the intended parent is the ForcingClosure claim-classification theorem. Landmarks touched: T6 $\varphi$, the $\varphi$-ladder mass formula, and the Maximal Forcing closure program.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)