tensorToScalarRatio
plain-language theorem explainer
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).
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.