module module high

`IndisputableMonolith.Gravity.Inflation`

The Gravity.Inflation module defines the α-attractor parameter α = φ² arising from the self-similarity condition on the J-cost functional. It establishes the quadratic character of the inflaton potential near the fixed point using the φ² = φ + 1 relation. Cosmologists deriving RS inflation models cite these definitions when computing slow-roll parameters from the Recognition Composition Law. The module supplies auxiliary results on positivity, bounds, spectral indices, and tensor-to-scalar ratios without containing proofs.

claimThe α-attractor parameter satisfies α = φ², where φ is the golden ratio fixed by φ² = φ + 1. This sets the curvature scale for the inflaton potential inherited from J(x) near x = 1.

background

This module sits in the Gravity domain and imports the Constants module, which supplies the RS-native time quantum τ₀ = 1 tick. It introduces the α-attractor from the self-similarity condition of the cost functional: the inflaton potential inherits the quadratic character of J(x) near x = 1, with the φ² = φ + 1 identity fixing the curvature scale. The module defines supporting objects including alpha_attractor, alpha_attractor_pos, alpha_attractor_bounds, spectral_index, tensor_to_scalar, r_at_55_bounds, n_s_at_55, r_in_detectable_range, X_opt, X_opt_pos, and Omega_0.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the α-attractor definitions that feed the JCostInflaton module, which proves that the Recognition Composition Law forces the inflaton potential to be J(x) = ½(x + x⁻¹) − 1 and derives the slow-roll parameters ε and η from the curvature of J in log coordinates. It fills the step connecting the self-similarity condition to the quadratic curvature scale in the RS inflation framework.

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