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

IndisputableMonolith.Masses.NumericalPredictions

show as:
view Lean formalization →

The module assembles numerical bounds on successive powers of phi together with derived mass ratios for particle generations. A physicist checking Recognition Science mass predictions against measured quark and lepton values would cite these intervals. Each bound follows from direct application of algebraic identities to the interval results imported from PhiBounds and AlphaBounds.

claim$phi^6 in (17,18)$ for the generation mass ratio $m_b/m_s$ or $m_tau/m_mu$ (with corrections), obtained from the Fibonacci identity $phi^6 = 8 phi + 5$.

background

Recognition Science places particle masses on a phi-ladder whose rungs are integer powers of the golden ratio, scaled by a yardstick set by the fundamental time quantum. The module imports the definition tau_0 = 1 tick from Constants, interval bounds on alpha inverse from AlphaBounds, and rigorous bounds on phi = (1 + sqrt(5))/2 from PhiBounds. The latter module establishes its intervals via the quadratic comparison 2.236^2 < 5 < 2.237^2.

proof idea

This is a module of bound statements rather than a single proof. Each declaration applies the imported PhiBounds lemmas together with the Fibonacci identity phi^6 = 8 phi + 5 and interval arithmetic to produce the stated numerical ranges.

why it matters in Recognition Science

The module supplies the concrete numerical intervals required to compare the Recognition Science phi-ladder mass formula with experimental generation ratios. It therefore supports quantitative checks of the T5 J-uniqueness and T6 phi fixed-point steps in the forcing chain. No downstream declarations are listed as using it yet.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)