TensorRatioCert
TensorRatioCert bundles the positivity and narrow-band membership of the RS-derived tensor-to-scalar ratio r = 2/(45 phi^2). Cosmologists comparing RS inflation predictions to CMB bounds would cite this certificate to confirm r lies inside (0.015, 0.020). The definition assembles the upstream positivity theorem and band theorem into a single record without further reasoning.
claimLet $r = 2/(45 phi^2)$. The structure certifies that $0 < r$ and $0.015 < r < 0.020$.
background
The module states the RS prediction r = 2/(45 phi^2) in (0.015, 0.020). The ratio is defined directly as 2 divided by 45 times phi squared, with phi the self-similar fixed point from the forcing chain. Upstream r_pos proves positivity by showing the numerator 2 is positive and the denominator 45 phi^2 is positive. Upstream r_band proves the interval membership by unfolding the definition, invoking phi2_eq, and applying phi greater than 1.618 together with nlinarith on the resulting linear inequality.
proof idea
The declaration is a structure definition that packages the two upstream theorems. It serves as a one-line wrapper assembling r_pos for the positivity field and r_band for the band field.
why it matters in Recognition Science
The structure feeds the downstream tensorRatioCert definition that instantiates the record. It encodes the explicit RS cosmology prediction for the tensor-to-scalar ratio, consistent with the phi-ladder and eight-tick octave landmarks. No open questions or scaffolding are attached.
scope and limits
- Does not derive the functional form of r from the Recognition Composition Law.
- Does not incorporate higher-order corrections or running of the ratio.
- Does not compare the interval to specific observational datasets or error bars.
formal statement (Lean)
49structure TensorRatioCert where
50 r_pos : 0 < tensorToScalarRatio
51 r_band : (0.015 : ℝ) < tensorToScalarRatio ∧ tensorToScalarRatio < 0.020
52