mass_ratio_phi7
plain-language theorem explainer
The theorem establishes that the neutrino squared-mass ratio lies within 0.5 of phi to the seventh times 1.17. Model builders comparing observed Delta m squared splittings to the golden-ratio ladder in Recognition Science cite this numerical match. The tactic proof unfolds the ratio definition, inserts the phi interval bounds, computes the phi^7 scaling via phi_pow7, and closes with linear arithmetic.
Claim. $|r - phi^7 * 1.17| < 0.5$ where $r = Delta m_{31}^2 / Delta m_{21}^2$ is the ratio of the observed squared mass differences.
background
The module treats observed neutrino mass differences. massRatio is defined as the quotient of the larger to smaller squared splitting deltam31_sq over deltam21_sq, with experimental central values near 2.51e-3 and 7.42e-5. The golden ratio phi satisfies the interval 1.618 < phi < 1.6185 by the phi_gt_1618 and phi_lt_16185 theorems, which rest on sqrt5 bounds and are reused across Physics modules. These interval facts descend from the PrimitiveDistinction theorem that extracts four structural conditions plus three definitional facts from seven axioms.
proof idea
The proof unfolds massRatio, deltam31_sq and deltam21_sq to expose the numerical ratio. It equates phi to goldenRatio then applies phi_gt_1618 and phi_lt_16185. Norm_num lemmas fix the experimental ratio inside (33.8, 33.9). Separate calculations using phi_pow7 bound phi^7 * 1.17 from below by 33.9 and from above by 34.1. The final step invokes abs_lt and closes both sides with linarith.
why it matters
The result places the neutrino hierarchy on the phi-ladder consistent with the mass formula yardstick * phi^(rung - 8 + gap(Z)). It supplies a concrete numerical check inside the StandardModel neutrino section and aligns with the self-similar fixed point phi forced at T6. No downstream uses are recorded, leaving open the question of deriving the 1.17 prefactor from J-cost or defectDist.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.