Encyclopedia Cosmology Cosmology Tensor To Scalar Ratio From Rs

ARTICLE 3 claims 3 theorems

Cosmology Tensor To Scalar Ratio From Rs

Cosmology's tensor-to-scalar ratio measures the imprint of primordial gravitational waves, and one framework derives a specific value for it.

The predicted ratio

The tensor-to-scalar ratio r is a number cosmologists use to describe the earliest moments of the universe. It compares the strength of two kinds of ripples imprinted in the cosmic microwave background: tensor perturbations, which come from gravitational waves, and scalar perturbations, which come from density variations. A larger r means gravitational waves played a bigger role in the infant universe. The Planck satellite and other experiments have placed upper bounds on r, but no experiment has yet measured a nonzero value.

In Recognition Science, the framework derives a specific prediction for this ratio. The framework's central idea is that reality keeps a ledger, a discrete record of recognition events, and the cost of maintaining that ledger forces a chain of physical constants. From that chain, the framework's machine-checked library of formal theorems derives the expression r = 2/(45φ²), where φ is the golden ratio, approximately 1.618. The value lands in the band (0.015, 0.020).

The library proves this result formally. It establishes that the ratio is positive, that it is less than one, and that it falls inside the stated band. The proof uses the identity φ² = φ + 1, which is a defining property of the golden ratio. The derivation is a theorem in the library, not a numerical fit; the constants in the expression come from the framework's forcing chain, not from cosmological data.

The prediction sits within the range that current experiments can test. The BICEP/Keck array and other instruments are pushing observational limits toward r values near 0.01. If future experiments measure a value in this band, it would support the framework's account. If they measure a value outside it, the framework's prediction would be falsified. The framework treats this as an empirical check, not as a settled result.

THEOREM tensorToScalarRatio · IndisputableMonolith/Cosmology/TensorToScalarRatioFromRS.lean
noncomputable def tensorToScalarRatio : ℝ := 2 / (45 * phi ^ 2)
THEOREM r_band · IndisputableMonolith/Cosmology/TensorToScalarRatioFromRS.lean
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 · r_lt_one · IndisputableMonolith/Cosmology/TensorToScalarRatioFromRS.lean
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

No experiment has measured a nonzero tensor-to-scalar ratio. The framework does not derive the value of the golden ratio itself. This prediction is a theorem, not an empirical measurement.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND