phi_neg2_lt
plain-language theorem explainer
The golden ratio satisfies φ^{-2} < 0.384. Galaxy-rotation and mixing-angle certificates cite this upper bound when checking that the a priori amplitude C = φ^{-2} sits inside SPARC and PMNS error bars. The proof rewrites φ^{-2} as 1/(φ+1), uses φ > 1.61 to get φ+1 > 2.61, and compares reciprocals by a short calc with norm_num.
Claim. If $\varphi$ is the golden ratio (unique positive root of $\varphi^2=\varphi+1$), then $\varphi^{-2}<0.384$.
background
This module is the ILG a priori prediction certificate. It answers the paper's charge that SPARC fits of $(A,\alpha,r_0)$ only matched golden-ratio candidates after the fact. Recognition Science claims both $\alpha$ and the amplitude $C$ are forced by self-similarity before any data comparison.
From the forcing chain: RCL uniqueness of the $J$-cost yields self-similarity, which forces the scale ratio $\varphi$ with $\varphi^2=\varphi+1$ (T6). The discrete memory kernel then carries amplitude $C=\varphi^{-2}$. The sibling identity $\varphi^{-2}=1/(\varphi+1)$ is the algebraic form used throughout this file.
Upstream, phi_gt_onePointSixOne supplies the tight lower bound $\varphi>1.61$ that controls the reciprocal comparison.
proof idea
Rewrite the goal via the sibling identity $\varphi^{-2}=1/(\varphi+1)$. Invoke the constant bound $\varphi>1.61$, then linarith to get $\varphi+1>2.61$. Record positivity of $\varphi$ and of $\varphi+1$. Apply one_div_lt_one_div_of_lt (denominators positive, larger denominator yields smaller reciprocal) to obtain $1/(\varphi+1)<1/2.61$. Finish the calc by norm_num showing $1/2.61<0.384$.
why it matters
Direct input to C_prediction_validated, which checks that $C_{\mathrm{pred}}=\varphi^{-2}$ matches SPARC $A_{\mathrm{obs}}=0.38\pm 0.04$ inside $1\sigma$, using the sandwich $0.381<\varphi^{-2}<0.384$. Also consumed by pmns_theta12_match (solar angle needs bounds on $\varphi^{-2}$ and $\alpha$) and by neutrino mass-fraction bounds.
Framework landmark: T6 forces $\varphi$; the module derivation chain ends at $C=\varphi^{-2}\approx 0.382$ as the a priori ILG amplitude. This lemma is the numeric upper half of the certificate that converts that chain from post-hoc observation into a pre-registered prediction (paper §III.A gap).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.