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:
- What observational upper bound on r do current experiments set?
- How does the framework derive the factor 2/45 in the expression?
- What would a measured value outside the band imply for the framework?
- How does this prediction compare with other inflationary models?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM tensorToScalarRatio · IndisputableMonolith/Cosmology/TensorToScalarRatioFromRS.lean
noncomputable def tensorToScalarRatio : ℝ := 2 / (45 * phi ^ 2)The framework's machine-checked library of formal theorems derives the expression r = 2/(45φ²), where φ is the golden ratio. tensorToScalarRatio · IndisputableMonolith/Cosmology/TensorToScalarRatioFromRS.leanTHEOREM 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]The value lands in the band (0.015, 0.020). r_band · IndisputableMonolith/Cosmology/TensorToScalarRatioFromRS.leanTHEOREM 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] nlinarithThe library proves that the ratio is positive and less than one. r_pos · r_lt_one · IndisputableMonolith/Cosmology/TensorToScalarRatioFromRS.lean