Cosmology Tensor To Scalar Ratio From Rs R Pos

What r_pos proves

The tensor-to-scalar ratio r is a number cosmologists use to describe the faint swirl of gravitational waves that inflation, the rapid early expansion of the universe, would leave imprinted on the cosmic microwave background. A larger r means stronger primordial gravitational waves; a value near zero means they are too weak to see with current instruments. In the Recognition Science framework, r is not fitted to telescope data but derived from a chain of forced constants, and the declaration r_pos is a small but exact piece of that derivation: it proves that the framework's predicted value of r is greater than zero.

The prediction itself is a simple formula: r = 2/(45φ²), where φ is the golden ratio, about 1.618. Plugging in the numbers gives r ≈ 0.0183, which lies in the band (0.015, 0.020). The framework's library, a machine-checked collection of formal theorems, proves three things about this number. First, r_pos: the ratio is strictly positive. Second, r_lt_one: it is less than one. Third, r_band: it falls between 0.015 and 0.020. These are not numerical approximations; they are exact statements proved from the definition of r and the known properties of φ, with no unproved assumptions and no axioms beyond the standard logical ones.

What r_pos does not claim is just as important. It does not say that the predicted r matches any measured value. The framework's formula lands in a range that current experiments, such as the BICEP and Planck collaborations, have not yet ruled out, but the comparison to observation is an empirical check, not a theorem. The declaration also does not say that the derivation of r from the framework's first principles is complete; the chain that forces the constants is proved in the library, but the physical bridge from recognition events to inflation is still open. Finally, r_pos says nothing about whether the tensor-to-scalar ratio is the right observable to test the framework; it only certifies that the number the framework produces is a valid positive probability-like quantity.

For a reader, the practical upshot is this: within the framework, r is not a free parameter. It is a fixed number, forced by the same logic that produces the golden ratio and the number of spatial dimensions. The proof r_pos is the smallest guardrail on that number, ensuring it is physically sensible before anyone asks whether it matches the sky.

theorem r_pos : 0 < tensorToScalarRatio :=
  div_pos (by norm_num) (mul_pos (by norm_num) (pow_pos phi_pos 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]

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

What this page does not claim

The predicted r matches any measured value; that comparison is an empirical check, not a theorem. The physical bridge from recognition events to inflation is complete; that bridge remains open. The tensor-to-scalar ratio is the only observable that can test the framework.

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: