tensor_to_scalar
The tensor-to-scalar ratio is defined as the direct quotient of tensor power spectrum amplitude to scalar power spectrum amplitude when the scalar amplitude is positive. Cosmologists deriving RS inflationary predictions from J-cost fluctuations would cite this ratio when matching to CMB observables such as those from LiteBIRD or CMB-S4. The definition reduces to a single division of the two input spectra.
claimThe tensor-to-scalar ratio satisfies $r = P_T / P_S$ whenever the scalar power spectrum satisfies $P_S > 0$.
background
The Cosmology.PrimordialSpectrum module derives the primordial power spectrum from J-cost quantum fluctuations during inflation, producing a nearly scale-invariant spectrum with spectral index near 0.965 and amplitude $A_s ≈ 2.1 × 10^{-9}$. The tensor-to-scalar ratio enters as the observable linking tensor and scalar modes in this RS mechanism.
proof idea
One-line definition that returns the quotient of the tensor spectrum by the scalar spectrum.
why it matters in Recognition Science
This supplies the standard $r = A_T / A_s$ used by downstream results including r_at_55_bounds, r_in_detectable_range, and r_from_jcost in Gravity.Inflation. Those theorems bound $r ∈ (0.005, 0.02)$ for $N ∈ [50,60]$ under the RS-specific choice α = φ², placing the prediction inside the CMB-S4 detectable window and linking to the phi-ladder and eight-tick octave structure.
scope and limits
- Does not compute a numerical value of r from e-foldings.
- Does not embed the alpha-attractor formula or phi dependence.
- Does not constrain the spectral index or scalar amplitude.
- Does not enforce RS-specific relations between the input spectra.
formal statement (Lean)
152noncomputable def tensor_to_scalar (ps_s ps_t : ℝ) (hs : ps_s > 0) : ℝ :=
proof body
Definition body.
153 ps_t / ps_s
154
155/-- RS prediction for r:
156
157 r may be φ-related. Possible predictions:
158 - r = (φ - 1)⁴ = 0.021 (testable by CMB-S4!)
159 - r = 1/(8φ⁵) = 0.011
160 - r = 1/φ⁸ = 0.021
161
162 All these are in the observable range! -/