pith. machine review for the scientific record. sign in
structure definition def or abbrev high

TensorSpectrum

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 147structure TensorSpectrum where
 148  amplitude : ℝ
 149  tensor_index : ℝ
 150
 151/-- The tensor-to-scalar ratio r = A_T / A_s. -/

depends on (2)

Lean names referenced from this declaration's body.