module module

`IndisputableMonolith.Gravity.JCostInflaton`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Gravity.Inflation module_import

declarations in this module (30)

def G L58
theorem G_is_Jcost_log L61
theorem G_at_zero L64
theorem G_nonneg L68
theorem G_pos_of_ne_zero L73
def slow_roll_epsilon L84
theorem epsilon_formula L88
def slow_roll_eta L95
theorem eta_eq_one L99
theorem slow_roll_epsilon_vanishes L105
theorem epsilon_le_half L110
theorem epsilon_nonneg L123
theorem G_second_deriv_at_zero L132
theorem alpha_from_curvature L139
theorem calibration_forces_alpha L148
theorem n_s_from_jcost L157
theorem r_from_jcost L162
theorem n_s_at_55_from_jcost L168
structure InflationFromJCostCert L178
theorem inflation_from_jcost_cert L199
def fib_10 L212
theorem fib_10_eq L214
def H_N_e_55 L230
theorem H_N_e_55_holds L232
theorem n_s_55_in_planck_band L237
theorem N_e_rung_arithmetic L242
theorem N_e_is_fibonacci L245
theorem n_s_44_vs_55 L248
theorem n_s_at_44 L253
theorem n_s_55_value L256