TensorSpectrum
plain-language theorem explainer
TensorSpectrum defines the two-parameter record for the primordial tensor power spectrum in Recognition Science cosmology. Researchers deriving gravitational-wave predictions from J-cost fluctuations during inflation would reference this structure when matching to CMB bounds. It is a direct record declaration with fields amplitude and tensor_index, carrying no computational content or proof obligations.
Claim. The tensor spectrum is the pair consisting of amplitude $A_T$ and tensor index $n_T$, so that the power spectrum takes the form $P_T(k) = A_T (k/k_*)^{n_T}$ with the single-field consistency relation $n_T = -r/8$.
background
The module COS-009 derives the primordial power spectrum from RS principles. Primordial fluctuations arise from J-cost quantum fluctuations during inflation, with the phi-ladder fixing the spectral tilt. The CMB exhibits a nearly scale-invariant spectrum with $n_s approx 0.965$ and amplitude $A_s approx 2.1 times 10^{-9}$. Tensor modes are the gravitational-wave counterpart, bounded by $r < 0.06$ from Planck plus BICEP/Keck data. Upstream amplitude definitions supply the complex transition amplitudes used in the broader QFT and quantum-mechanical scaffolding of the module.
proof idea
The declaration is a bare structure definition that introduces the record type with two real fields. No tactics or lemmas are applied; the construction is immediate from the Lean structure syntax.
why it matters
This structure supplies the tensor-sector counterpart to the scalar spectrum inside the COS-009 derivation of the primordial spectrum from J-cost fluctuations. It directly supports the paper proposition on the CMB spectral index from the golden ratio by providing the tensor amplitude and index needed for the consistency relation and future CMB-S4 forecasts. Within the Recognition framework it sits downstream of the phi-ladder and T6 fixed-point results that determine the tilt.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.