seesaw_scale_phi_connection
plain-language theorem explainer
The theorem shows that the phi-predicted Majorana scale lies within 10^15 of 2.3 times 10^16. Neutrino modelers using the seesaw mechanism inside Recognition Science would cite it to fix the Majorana scale via the phi ladder. The tactic proof unfolds the prediction, inserts the bounds 1.618 < phi < 1.6185 together with the Fibonacci expression for phi^13, then verifies the absolute-value claim by linear arithmetic after rewriting with abs_lt.
Claim. Let MR denote the phi-predicted Majorana scale. Then $|MR - 2.3 × 10^{16}| < 10^{15}$.
background
The module treats neutrino mass differences inside Recognition Science. Mass is the real numbers in RS-native units. The golden ratio satisfies 1.618 < phi < 1.6185, and the auxiliary identity phi^13 = 233 phi + 144 follows from the recurrence phi^n = phi^{n-1} + phi^{n-2}. These facts supply the numerical window needed to locate the seesaw scale on the phi ladder.
proof idea
Unfold phiPredictedMR. Import the phi bounds and the exact phi^13 expression. Derive 520 < phi^13 < 522 by norm_num and linarith. Rewrite the goal with abs_lt. For the lower side multiply the target inequality by the positive phi^13 and apply linarith; repeat for the upper side.
why it matters
The result is used by nu_sum_bound_consistent to confirm that the predicted neutrino masses sum below the Planck limit. It closes the link between the phi-ladder mass formula and the seesaw scale, using the J-uniqueness and phi fixed-point steps of the forcing chain. No new parameters are added beyond the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.