pith. sign in
module module high

IndisputableMonolith.Masses.NumericalPredictions

show as:
view Lean formalization →

Module supplies interval bounds and equalities for powers of φ, centered on φ^6 ∈ (17,18) as a proxy for generation mass ratios such as m_b/m_s. Researchers deriving particle spectra from the phi-ladder would cite these results. Content consists of definitions and bounds assembled from Fibonacci identities together with imported interval modules for φ and α^{-1}.

claim$φ^6 ∈ (17,18)$ with the identity $φ^6 = 8φ + 5$, serving as a numerical stand-in for generation mass ratios $m_b/m_s$ or $m_τ/m_μ$ after corrections.

background

The module sits inside the Masses domain of Recognition Science and imports the base time quantum τ₀ = 1 tick from Constants, interval bounds on α^{-1} from AlphaBounds, and algebraic bounds on φ = (1 + √5)/2 from PhiBounds. The latter module obtains its φ bounds from the quadratic inequalities 2.236² < 5 < 2.237². Local notation follows the phi-ladder convention in which mass ratios are expressed as yardstick × φ^(rung - 8 + gap(Z)).

proof idea

This is a definition module, no proofs. It aggregates equalities and interval statements for successive powers of φ by direct appeal to Fibonacci relations and the imported numeric bounds.

why it matters in Recognition Science

Supplies the concrete numerical layer that converts the abstract self-similar fixed point φ (T6) into testable mass ratios. The supplied doc-comment identifies the direct link to generation mass ratios m_b/m_s. No downstream declarations are recorded in the current graph.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)