module module high

`IndisputableMonolith.Gravity.JCostInflaton`

Module JCostInflaton defines the inflaton potential as G(t) = J(e^t) = cosh(t) - 1 exactly in log time coordinates. RS inflation modelers cite it when building slow-roll dynamics from the J-cost. The equivalence is immediate from the J definition and the exponential-to-hyperbolic identity.

claim$G(t) = J(e^t) = \cosh(t) - 1$ where $J(x) = \frac12(x + x^{-1}) - 1$.

background

Recognition Science derives all physics from the J-cost equation and the T0-T8 forcing chain. This module specializes J to the inflaton potential inside the inflationary predictions of Gravity.Inflation, which states that the alpha-attractor parameter is phi squared, the spectral tilt and tensor-to-scalar ratio are parameter-free, and the log-periodic modulation has frequency Omega_0 = 2 pi / ln(1/X_opt).

Constants supplies the RS time quantum tau_0 = 1 tick that sets native units for the coordinate t. The module records the exact identity G(t) = cosh(t) - 1 rather than an approximation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the exact inflaton potential required by the RS inflationary predictions formalized in Gravity.Inflation. It fills the J-cost definition step for the universe-origin paper's inflation section, enabling subsequent slow-roll derivations in the same module.

scope and limits

Does not derive slow-roll epsilon or eta.
Does not connect to the phi-ladder mass formula.
Does not address the alpha inverse band or G constant.
Does not treat the eight-tick octave or spatial dimensions.

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