tensorRatioCert
plain-language theorem explainer
The definition packages the positivity and interval bounds on the tensor-to-scalar ratio r into a single certificate structure. Cosmologists referencing Recognition Science inflation predictions would cite it to invoke the derived bounds without repeating the calculations. It is assembled as a one-line record constructor that supplies the two component theorems r_pos and r_band.
Claim. Let $r$ denote the tensor-to-scalar ratio. The certificate asserts that $0 < r$ and $0.015 < r < 0.020$, where $r = 2/(45 phi^2)$.
background
In the module Tensor-to-Scalar Ratio from RS, the ratio is given by $r = 2/(45 phi^2)$. The structure TensorRatioCert collects two properties: positivity of $r$ and the numerical band $(0.015, 0.020)$. Upstream, the theorem r_pos establishes positivity by showing the denominator is positive, and r_band proves the interval bounds using the equation for phi squared and inequalities on phi.
proof idea
The definition is a one-line wrapper that constructs the TensorRatioCert record by assigning the theorem r_pos to the r_pos field and r_band to the r_band field.
why it matters
This definition packages the RS prediction for the tensor-to-scalar ratio $r = 2/(45 phi^2)$ into a reusable certificate. It supports cosmological applications of the Recognition Science framework by providing a verified interval for $r$ in the range $(0.015, 0.020)$. No downstream uses are recorded yet, but it closes the A2 inflation depth module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.