module module

`IndisputableMonolith.Gravity.Inflation`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

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

IndisputableMonolith.Gravity.JCostInflaton module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (17)

def alpha_attractor L35
theorem alpha_attractor_eq_phi_plus_one L37
theorem alpha_attractor_pos L39
theorem alpha_attractor_bounds L41
def spectral_index L47
def tensor_to_scalar L52
theorem r_at_55_bounds L55
theorem n_s_at_55 L62
theorem r_in_detectable_range L67
def X_opt L78
theorem X_opt_pos L80
def Omega_0 L88
theorem Omega_0_pos L91
def k_rec_com L103
theorem curvature_bounded_at_R0 L107
structure InflationCert L112
theorem inflation_cert L119