module module high

`IndisputableMonolith.Gravity.Inflation`

The Inflation module defines the α-attractor parameter α = φ² arising from J-cost self-similarity near x = 1. Researchers modeling RS inflation would cite its spectral index and tensor-to-scalar bounds. The module supplies supporting definitions and inequalities that feed the J-cost inflaton derivation without containing proofs.

claim$\alpha = \phi^2$ where $\phi$ satisfies $\phi^2 = \phi + 1$, setting the curvature scale of the inflaton potential inherited from $J(x) = \frac12(x + x^{-1}) - 1$.

background

This module operates in the Gravity domain and imports the Constants module whose sole content is the RS time quantum $\tau_0 = 1$ tick. The supplied doc-comment states that $\alpha = \phi^2$ follows from the self-similarity condition on the cost functional, so that the inflaton potential inherits the quadratic character of $J(x)$ near $x = 1$. Sibling declarations supply concrete bounds on the spectral index $n_s$ and tensor-to-scalar ratio $r$ at 55 e-folds together with positivity and range statements for the auxiliary quantity $X$.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the $\alpha$-attractor definitions required by the downstream JCostInflaton module, whose doc-comment states that it proves the Recognition Composition Law forces the inflaton potential to equal $J(x)$ and derives the slow-roll parameters $\varepsilon$ and $\eta$ from the curvature of $J$ in log coordinates. It therefore fills the curvature-scale step that links T5 J-uniqueness and T6 phi fixed-point to inflationary observables.

scope and limits

Does not derive the Recognition Composition Law.
Does not compute numerical predictions for CMB observables.
Does not address reheating or post-inflationary evolution.
Does not connect to the eight-tick octave or spatial dimension count.

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