r_pos
plain-language theorem explainer
The theorem establishes that the Recognition Science tensor-to-scalar ratio is strictly positive. Cosmologists using RS inflation models cite it to confirm r lies in the positive reals before verifying its numerical band. The proof is a one-line wrapper that invokes div_pos on the explicit algebraic definition of tensorToScalarRatio.
Claim. $0 < 2/(45 phi^2)$ where $phi$ denotes the self-similar fixed point.
background
The module states the RS prediction r = 2/(45 phi^2) lies in (0.015, 0.020). The upstream definition sets tensorToScalarRatio : ℝ := 2 / (45 * phi ^ 2). This supplies the algebraic expression whose positivity is asserted here, inside a cosmology section that reports zero axioms and zero sorrys.
proof idea
One-line wrapper that applies div_pos to the numerator 2 and the denominator 45 * phi^2. The subgoals are discharged by norm_num on the rational constants and by pow_pos phi_pos on the squared term.
why it matters
It populates the r_pos field of TensorRatioCert, which is required by ClosedObservableFramework and by toRealizedHierarchy. The result therefore anchors the RS cosmology prediction inside the closed-observable interface that descends from the forcing chain (T5 J-uniqueness through T8 D = 3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.