r_band
plain-language theorem explainer
The theorem shows that the RS tensor-to-scalar ratio, given by 2 over 45 phi squared, lies strictly between 0.015 and 0.020. Cosmologists using Recognition Science cite the interval when testing A2 inflation predictions against CMB observations. The tactic proof splits the conjunction, substitutes the quadratic relation for phi, invokes the 1.61 to 1.62 bounds, and closes both sides with linear arithmetic after reciprocal inequalities.
Claim. $0.015 < 2/(45 phi^2) < 0.020$, where $phi$ satisfies $phi^2 = phi + 1$ and $1.61 < phi < 1.62$.
background
The module treats the tensor-to-scalar ratio in Recognition Science cosmology under A2 inflation depth. tensorToScalarRatio is the definition 2 divided by 45 times phi to the power 2. phi2_eq records the identity phi squared equals phi plus one that follows from the golden-ratio quadratic. Upstream lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo supply the numerical bounds 1.61 less than phi and phi less than 1.62. The module documentation states the RS prediction r equals 2 over 45 phi squared belongs to the open interval from 0.015 to 0.020.
proof idea
The tactic proof applies constructor to split the conjunction into two goals. Each goal unfolds tensorToScalarRatio, rewrites with phi2_eq, pulls in the corresponding phi bound lemma, establishes positivity of the denominator via nlinarith, derives the reciprocal comparison with div_le_div_of_nonneg_left, and finishes with linarith against an explicit numerical inequality produced by norm_num.
why it matters
The result supplies the interval component required by the TensorRatioCert structure and the tensorRatioCert definition that packages positivity together with the band. It realizes the explicit RS prediction recorded in the module documentation for the tensor-to-scalar ratio. The bound sits inside the Recognition Science derivation of cosmological parameters from the phi ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.