Cosmology Tensor To Scalar Ratio From Rs Tensor To Scalar Ratio

The predicted ratio

In cosmology, the tensor-to-scalar ratio r measures the relative strength of primordial gravitational waves (the tensor component) against density fluctuations (the scalar component) in the early universe. A lower value means the gravitational-wave signal is weaker relative to the density ripples. Observational campaigns have spent years trying to pin it down, because its size discriminates between competing models of cosmic inflation.

The Recognition Science framework's machine-checked library of formal theorems contains a definition, tensorToScalarRatio, that assigns this ratio the value r = 2/(45φ²), where φ is the golden ratio. The library proves this number is positive, less than one, and lies strictly between 0.015 and 0.020. The proof is a direct computation from the definition; it does not invoke any observational data. The framework derives this number from its internal forcing chain, which fixes the golden ratio as a fundamental scaling constant.

Current measurements place the ratio below about 0.036 (from the BICEP/Keck collaboration), with some analyses tightening that bound further. The RS value of roughly 0.018 falls comfortably inside the observed upper limit. The framework's library does not claim this is a prediction that has been confirmed; it claims the value follows from its axioms and is consistent with the current upper bound. The derivation is a theorem, but the comparison with experiment is an empirical check, not part of the proof.

What the declaration does not claim: it does not claim that the tensor-to-scalar ratio has been measured to be this value, nor that the framework's derivation replaces the need for observation. It does not claim that the golden ratio itself is derived from cosmology; rather, the golden ratio enters as a fixed constant from the framework's foundational chain. The library's certificate, TensorRatioCert, packages the positivity and band theorems into a single object, but it adds no new physics beyond those two proved facts.

noncomputable def tensorToScalarRatio : ℝ := 2 / (45 * phi ^ 2)

theorem r_band : (0.015 : ℝ) < tensorToScalarRatio ∧ tensorToScalarRatio < 0.020 := by
  constructor
  · unfold tensorToScalarRatio
    rw [phi2_eq]
    have h1 := phi_gt_onePointSixOne
    have hpos : (0:ℝ) < 45 * (phi + 1) := by nlinarith
    have hlt : 45 * (phi + 1) < 45 * 2.63 := by nlinarith [phi_lt_onePointSixTwo]
    have hup : 2 / (45 * 2.63) ≤ 2 / (45 * (phi + 1)) := by
      apply div_le_div_of_nonneg_left (by norm_num) hpos (by nlinarith)
    linarith [show (0.015:ℝ) < 2 / (45 * 2.63) from by norm_num]
  · unfold tensorToScalarRatio
    rw [phi2_eq]
    have h1 := phi_gt_onePointSixOne
    have hpos : (0:ℝ) < 45 * (phi + 1) := by nlinarith
    have hgt : 45 * (phi + 1) > 45 * 2.59 := by nlinarith
    have hlo : 2 / (45 * (phi + 1)) ≤ 2 / (45 * 2.59) := by
      apply div_le_div_of_nonneg_left (by norm_num) (by nlinarith) (by nlinarith)
    linarith [show (2 : ℝ) / (45 * 2.59) < 0.020 from by norm_num]

theorem r_pos : 0 < tensorToScalarRatio :=
  div_pos (by norm_num) (mul_pos (by norm_num) (pow_pos phi_pos 2))

theorem r_lt_one : tensorToScalarRatio < 1 := by
  unfold tensorToScalarRatio
  rw [phi2_eq]
  have h1 := phi_gt_onePointSixOne
  have hpos : (0:ℝ) < 45 * (phi + 1) := by nlinarith
  rw [div_lt_iff₀ hpos]
  nlinarith

What this page does not claim

The tensor-to-scalar ratio has been measured to be approximately 0.018. The derivation of r from the framework replaces the need for observational cosmology. The golden ratio is derived from cosmological measurements.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/TensorToScalarRatioFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: