pith. sign in
module module high

IndisputableMonolith.Masses.MassRatiosProved

show as:
view Lean formalization →

The MassRatiosProved module supplies explicit numerical bounds on mass ratios via powers of the golden ratio. It establishes 17 < φ^6 < 18 from the relation φ^3 = 2φ + 1 together with the interval 1.5 < φ < 1.62. Researchers modeling particle hierarchies on the phi-ladder cite these bounds to constrain rung gaps. The derivation is a direct algebraic expansion and interval check.

claim$17 < \phi^6 < 18$, where $\phi$ satisfies $\phi^3 = 2\phi + 1$ and lies in $(1.5, 1.62)$.

background

The module resides in the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants along with the result that φ is forced by self-similarity in a discrete ledger with J-cost from PhiForcing. The supplied doc-comment records the central calculation: from φ^3 = 2φ + 1 one obtains φ^6 = (2φ + 1)^2, which is then bounded by substituting the given interval for φ. These bounds are intended for application to mass ratios on the phi-ladder.

proof idea

The argument expands the identity φ^6 = (φ^3)^2 = (2φ + 1)^2 and evaluates the resulting quadratic over the open interval 1.5 < φ < 1.62 to produce the strict inequalities 17 < φ^6 < 18. No external lemmas are invoked beyond the algebraic relation already stated in the doc-comment.

why it matters in Recognition Science

The bounds support the sibling declarations phi_6_bounds_mass_ratio, mass_ratio_from_rung_difference, and mass_ordering_from_rungs, which in turn populate MassRatioCert and mass_ratio_cert_exists. The calculation supplies concrete numerical content for the phi-ladder mass formula inside the Recognition Science forcing chain (T5–T6).

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (5)