TensorRatioCert
plain-language theorem explainer
The certification structure for the tensor-to-scalar ratio packages positivity together with membership in the interval (0.015, 0.020). Cosmologists modeling A2 inflation inside Recognition Science would cite it to record that the derived r equals 2 over 45 phi squared lies inside the target window. The structure is assembled directly from the positivity theorem and the band theorem.
Claim. Let $r = 2/(45 phi^2)$ with $phi$ the golden ratio. The structure certifies $0 < r$ and $0.015 < r < 0.020$.
background
In the module Tensor-to-Scalar Ratio from RS the ratio is introduced as the noncomputable definition $r = 2/(45 phi^2)$. The positivity theorem shows $0 < r$ by norm_num and pow_pos on phi. The band theorem proves the two-sided inequality by unfolding the definition, invoking phi greater than 1.61, and applying nlinarith to the resulting linear bounds. The module header states the RS prediction r equals 2 over 45 phi squared lies in (0.015, 0.020) with zero sorries.
proof idea
This is a structure definition that bundles the two field theorems. The positivity result is referenced directly for the first field and the band result for the second field. No additional tactics or reductions occur inside the structure.
why it matters
The structure is instantiated inside the tensor ratio certificate definition that closes the module. It supplies the Lean witness for the RS cosmological prediction of the tensor-to-scalar ratio, linking the numerical window to the self-similar fixed point phi from the forcing chain. The module reports zero sorries and zero axioms, confirming the interval claim is fully formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.