alpha_attractor_bounds
plain-language theorem explainer
The declaration proves that the α-attractor parameter satisfies 2.5 < α < 2.7. Cosmologists deriving slow-roll predictions from the Recognition Science cost functional would cite this interval when fixing the curvature scale for the spectral index and tensor-to-scalar ratio. The proof is a direct one-line term application of the phi-squared bounds lemma via the definition α = φ².
Claim. $2.5 < α < 2.7$, where $α = φ^2$ is the α-attractor parameter obtained from the self-similarity condition of the cost functional $J(x)$ near $x=1$.
background
The Inflation from phi module defines the α-attractor parameter as α = φ², where φ is the golden ratio obeying φ² = φ + 1. This identification arises because the inflaton potential inherits the quadratic character of J(x) under the self-similarity constraint. The module states that this yields parameter-free predictions: n_s ≈ 1 - 2/N and r ≈ 12 φ² / N², together with the log-periodic frequency Ω₀ = 2π / ln(π/φ).
proof idea
The proof is a one-line term wrapper that applies the phi_squared_bounds lemma from Constants. That lemma rewrites phi^2 = phi + 1 and invokes the supplied bounds phi > 1.5 and phi < 1.62 to conclude the interval for phi^2, which transfers directly to alpha_attractor by definition.
why it matters
The bound supplies the concrete numerical range for α in the RS inflationary framework, where α = φ² replaces the generic attractor parameter. It anchors the spectral predictions listed in the module documentation and connects to the phi-ladder and self-similar fixed point of the forcing chain. No downstream theorems are recorded, but the result is required for any quantitative use of the module's n_s and r formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.