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

tensor_to_scalar_upper_bound

show as:
view Lean formalization →

Recognition Science cosmology adopts 0.06 as the upper limit on the tensor-to-scalar ratio r. Researchers comparing RS-derived primordial spectra to CMB observations would cite this bound when testing J-cost fluctuation models. The definition is a direct assignment of the combined Planck and BICEP/Keck constraint.

claimThe tensor-to-scalar ratio satisfies $r < 0.06$, with the numerical value taken from Planck and BICEP/Keck observations of the cosmic microwave background.

background

The PrimordialSpectrum module derives the CMB power spectrum P(k) = A_s (k/k_*)^(n_s - 1) from Recognition Science principles. Primordial fluctuations arise from J-cost quantum fluctuations during inflation, with the phi-ladder fixing the spectral tilt n_s - 1. The module imports the scale function defined as phi^k and the power function that multiplies amplitude by the scaled wavenumber term. Upstream amplitude definitions from S-matrix and double-slit contexts supply the underlying transition probabilities used in fluctuation calculations.

proof idea

The definition is a direct assignment of the observational upper bound 0.06 for the tensor-to-scalar ratio.

why it matters in Recognition Science

This constant supplies the observational anchor for the COS-009 derivation of the primordial spectrum from J-cost fluctuations. It supports the target paper proposition on the CMB spectral index from the golden ratio and connects to the nearly scale-invariant spectrum with n_s ≈ 0.965. The bound is referenced against the amplitude and power functions in the same module but has no downstream uses yet.

scope and limits

formal statement (Lean)

  52noncomputable def tensor_to_scalar_upper_bound : ℝ := 0.06

proof body

Definition body.

  53
  54/-! ## The Power Spectrum -/
  55
  56/-- The primordial power spectrum P(k) = A_s (k/k_*)^(n_s - 1).
  57
  58    - k: wavenumber (inverse length scale)
  59    - k_*: pivot scale (0.05 Mpc⁻¹)
  60    - A_s: amplitude at pivot
  61    - n_s: spectral index -/

depends on (5)

Lean names referenced from this declaration's body.