module module high

`IndisputableMonolith.Gravity.JCostInflaton`

Module defines the inflaton potential as the J-cost evaluated in logarithmic time coordinates, producing the exact closed form G(t) = cosh(t) - 1. Cosmologists working within Recognition Science cite it when grounding slow-roll parameters and spectral predictions in the forcing chain. The module consists of a central definition of G together with lemmas establishing non-negativity, positivity away from zero, and the slow-roll quantities epsilon and eta.

claim$G(t) := J(e^t) = cosh(t) - 1$, where $J(x) = (x + x^{-1})/2 - 1$.

background

The J-cost function is fixed by T5 uniqueness in the UnifiedForcingChain and obeys the Recognition Composition Law. Constants supplies the RS-native time unit τ₀ = 1 tick. The upstream Inflation module states that the α-attractor parameter equals φ², that the spectral tilt and tensor-to-scalar ratio are parameter-free, and that the log-periodic modulation frequency is Ω₀ = 2π / ln(1/X_opt).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the explicit inflaton potential used to derive the α-attractor and spectral results in the Inflation module. It realizes the exact J-to-cosh relation from the forcing chain T5-T8, enabling the parameter-free predictions listed in the Universe-Origin Paper.

scope and limits

Does not derive the full power spectrum or CMB observables.
Does not incorporate quantum corrections or multi-field extensions.
Does not compute numerical values for the slow-roll parameters from first principles.
Does not address the Berry creation threshold or Z_cf in the inflationary context.

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