pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Masses.Manifest

show as:
view Lean formalization →

The Masses.Manifest module assembles explicit mass placements for particles on the Recognition Science phi-ladder. Each mass is expressed as yardstick times phi to the power of rung minus eight plus gap for the relevant Z. The module functions as a reference collection feeding spectrum calculations and constant derivations without performing any proofs.

claimMasses are given by $m = y_0 · ϕ^{r-8+g(Z)}$ on the phi-ladder, where $y_0$ is the yardstick, $r$ the rung index, $g(Z)$ the gap function of atomic number, and $ϕ$ the self-similar fixed point from T6.

background

Recognition Science places all masses on the phi-ladder after the forcing chain reaches T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave, and T8 D=3. The Recognition Composition Law supplies the algebraic structure for products and ratios of J-costs. The module imports Mathlib to support these real-number expressions and introduces the concrete rung and gap assignments for the mass manifest.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete mass values required by downstream theorems on particle spectra and the derivation of G = phi^5 / pi together with the alpha inverse band inside (137.030, 137.039). It closes the gap between the abstract forcing chain T0-T8 and observable mass ratios.

scope and limits

declarations in this module (2)