TensorSpectrum
plain-language theorem explainer
TensorSpectrum is the structure holding the two real parameters that specify the tensor power spectrum in the Recognition Science derivation of primordial fluctuations. Researchers modeling CMB tensor modes or testing single-field inflation consistency relations would cite this definition when linking J-cost fluctuations to gravitational-wave predictions. The declaration is a bare structure definition that introduces amplitude and tensor_index fields with no further computation.
Claim. A tensor spectrum is a pair consisting of an amplitude $A_T$ and a tensor index $n_T$, so that the tensor power spectrum takes the form $P_T(k) = A_T (k/k_*)^{n_T}$.
background
The module COS-009 derives the primordial power spectrum from Recognition Science principles, with fluctuations arising from J-cost quantum fluctuations during inflation and the phi-ladder fixing the spectral tilt. The local setting states that the CMB spectrum is nearly scale-invariant with $n_s approx 0.965$ and amplitude $A_s approx 2.1 times 10^{-9}$, and that tensor modes are an additional prediction of inflation. 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 structure definition that directly introduces the two fields amplitude and tensor_index; no lemmas or tactics are applied.
why it matters
The structure supplies the tensor-sector counterpart to the scalar spectrum inside the COS-009 derivation of the primordial spectrum from J-cost fluctuations. It formalizes the standard inflation predictions (tensor power spectrum, consistency relation $n_T = -r/8$, and current bound $r < 0.06$) inside the Recognition Science framework that also invokes T5 J-uniqueness and T6 phi fixed-point. No downstream theorems yet consume the definition, leaving open the explicit connection to the phi-ladder tilt formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.