structure
definition
def or abbrev
CosmologicalPredictionsCert
show as:
view Lean formalization →
formal statement (Lean)
136structure CosmologicalPredictionsCert where
137 spectral_index_gt : (0.5 : ℝ) < 1 - 2 / (phi ^ 3)
138 spectral_index_lt : 1 - 2 / (phi ^ 3) < 1
139 hubble_pos : Real.log phi / 8 > 0
140 phi_sq_lower : (2.59 : ℝ) < phi^2
141 phi_sq_upper : phi^2 < (2.62 : ℝ)
142 phi_fourth_lower : (6.7 : ℝ) < (phi : ℝ)^(4 : ℕ)
143 phi_fourth_upper : (phi : ℝ)^(4 : ℕ) < (6.9 : ℝ)
144 phi_fifth_lower : (10.7 : ℝ) < (phi : ℝ)^(5 : ℕ)
145 phi_fifth_upper : (phi : ℝ)^(5 : ℕ) < (11.3 : ℝ)
146