TensorSpectrum
plain-language theorem explainer
TensorSpectrum supplies the two parameters needed to specify the primordial tensor power spectrum in Recognition Science cosmology. Researchers deriving CMB tensor modes from J-cost fluctuations during inflation would cite this record when assembling the full power spectrum alongside scalar contributions. The declaration is a bare structure definition with no computation or lemmas.
Claim. A tensor spectrum is given by an amplitude $A_T$ and tensor index $n_T$, entering the power spectrum $P_T(k) = A_T (k/k_*)^{n_T}$ and related to the tensor-to-scalar ratio by $r = A_T / A_s$.
background
The Cosmology.PrimordialSpectrum module derives the primordial power spectrum from J-cost quantum fluctuations, with the phi-ladder fixing the spectral tilt. The CMB exhibits a nearly scale-invariant spectrum $P(k) ∝ k^{n_s-1}$ with $n_s ≈ 0.965$ and amplitude $A_s ≈ 2.1 × 10^{-9}$. Upstream amplitude definitions from SMatrixUnitarity and DoubleSlit supply the underlying quantum transition amplitudes that seed these fluctuations.
proof idea
The declaration is a structure definition that introduces the record TensorSpectrum with fields amplitude and tensor_index. No lemmas or tactics are invoked; it functions as a data container for later spectrum constructions.
why it matters
This structure completes the tensor sector of the COS-009 derivation of the primordial spectrum from RS principles. It encodes the consistency relation $n_T = -r/8$ and the observational bound $r < 0.06$, positioning the framework to predict gravitational-wave modes alongside scalar fluctuations tied to the phi-ladder. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.