module module high

`IndisputableMonolith.Gravity.JCostInflaton`

The module defines the inflaton potential G(t) as the J-cost evaluated in logarithmic time coordinates. Researchers modeling RS inflation would cite it for the exact closed form of the potential. It is a definition module with no proofs.

claimThe inflaton potential satisfies $G(t) = J(e^t) = 2^{-1}(e^t + e^{-t}) - 1 = 2^{-1}(e^t + e^{-t}) - 1$, where the J-cost is the function $J(x) = 2^{-1}(x + x^{-1}) - 1$.

background

This module belongs to the Gravity domain and imports the RS time quantum from Constants together with the inflationary framework from Gravity.Inflation. The upstream Inflation module formalizes RS inflationary predictions with the alpha-attractor parameter equal to phi squared and parameter-free spectral tilt. The J-cost itself originates from the Recognition Composition Law and satisfies J(x) = cosh(log x) - 1 exactly.

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 in Gravity.Inflation, including the alpha-attractor parameter phi squared and the log-periodic modulation frequency. It closes the link between the J-cost definition and the slow-roll parameters used in the eight-tick octave structure.

scope and limits

Does not derive the J-cost from the forcing chain T0-T8.
Does not compute numerical values for the spectral index or tensor-to-scalar ratio.
Does not address the Berry creation threshold or Z_cf values.
Does not extend the potential beyond the log-coordinate substitution.

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