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

tensorToScalarRatio

show as:
view Lean formalization →

The definition supplies the RS-derived tensor-to-scalar ratio as the exact real number 2/(45 φ²). Cosmologists working inside Recognition Science cite it when bounding inflationary observables against CMB data. The declaration is a direct arithmetic expression that downstream bounds then verify lies in (0.015, 0.020).

claimThe tensor-to-scalar ratio is defined by $r = 2/(45 φ^2)$.

background

The module TensorToScalarRatioFromRS encodes the A2 inflation depth prediction inside Recognition Science cosmology. It imports the constant phi from IndisputableMonolith.Constants, where phi denotes the golden ratio fixed point forced by the self-similar structure of the J-cost function. The module states that RS predicts r = 2/(45φ²) ∈ (0.015, 0.020) with zero sorry or axiom.

proof idea

The declaration is a direct definition that evaluates the arithmetic expression 2 divided by 45 times phi squared. No lemmas or tactics are invoked; the expression serves as the base value for the positivity, upper-bound, and band theorems that follow.

why it matters in Recognition Science

This definition supplies the central value used by r_pos, r_lt_one, r_band, and the TensorRatioCert structure to certify that the ratio is positive and lies inside the narrow observational window. It realizes the RS cosmology prediction that links the phi-ladder (T6) to the eight-tick octave and spatial dimension D=3. The exact form allows the subsequent theorems to close the certification without additional hypotheses.

scope and limits

formal statement (Lean)

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

proof body

Definition body.

  16

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.