r_lt_one
plain-language theorem explainer
The theorem establishes that the Recognition Science tensor-to-scalar ratio is strictly less than one. Inflation modelers would cite this bound to confirm consistency with the basic slow-roll requirement. The proof unfolds the definition, substitutes the quadratic relation for phi, invokes the numerical lower bound on phi, and closes the inequality with linear arithmetic.
Claim. $2/(45 phi^2) < 1$, where $phi$ is the golden ratio obeying $phi^2 = phi + 1$.
background
The module computes the tensor-to-scalar ratio for A2 inflation depth in Recognition Science. The definition sets tensorToScalarRatio to 2 divided by 45 times phi squared. The theorem phi2_eq records the quadratic relation phi squared equals phi plus one, which follows from the self-similar fixed point of phi. The upstream lemma phi_gt_onePointSixOne supplies the concrete lower bound phi greater than 1.61, proved by comparing squares to 5. The module states the RS prediction r equals 2 over 45 phi squared lies in (0.015, 0.020).
proof idea
The proof unfolds the definition of tensorToScalarRatio, rewrites via phi2_eq to replace phi squared by phi plus one, imports the bound phi greater than 1.61, proves positivity of 45 times (phi plus one) by nlinarith, rewrites the target inequality using the division rule for positive denominators, and finishes with nlinarith.
why it matters
This result supplies a basic consistency check that the RS-derived ratio satisfies r less than 1, a prerequisite for viable inflation. It belongs to the cosmology module that predicts the narrow interval (0.015, 0.020) from the phi-ladder and eight-tick octave. No downstream theorems are recorded, yet the bound closes an elementary gate in the tensor-to-scalar derivation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.