tensorRatioCert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the value of r from first principles.
- Does not prove the RS prediction itself.
- Does not address higher-order corrections to the ratio.
formal statement (Lean)
53noncomputable def tensorRatioCert : TensorRatioCert where
54 r_pos := r_pos
proof body
Definition body.
55 r_band := r_band
56
57end IndisputableMonolith.Cosmology.TensorToScalarRatioFromRS