tensor_to_scalar
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.