alpha_attractor_eq_phi_plus_one
plain-language theorem explainer
The declaration equates the α-attractor parameter to φ + 1. Cosmologists deriving RS inflationary spectra would cite it to substitute the golden-ratio value for the generic curvature scale in α-attractor models. The proof is a direct one-line application of the phi square identity lemma.
Claim. The α-attractor parameter satisfies $α = φ + 1$, where $φ$ is the golden ratio obeying $φ^2 = φ + 1$.
background
In the Inflation module the α-attractor parameter is defined as the curvature scale $α = φ^2$ inherited from self-similarity of the J-cost functional near the vacuum. The golden ratio $φ$ satisfies the minimal polynomial $x^2 - x - 1 = 0$. The upstream phi_sq_eq lemma records the algebraic identity $φ^2 = φ + 1$ obtained by unfolding the definition $φ = (1 + √5)/2$ and simplifying.
proof idea
The proof is a one-line wrapper that applies the phi_sq_eq lemma (from Constants or PhiLadderLattice) to replace the definition of alpha_attractor.
why it matters
This supplies the explicit value required by the parent inflation_cert theorem and by alpha_from_curvature, which together certify that every inflationary ingredient is forced by J-cost uniqueness. It realizes the self-similar fixed point (T6) for the inflaton and replaces the free α of generic α-attractors with the RS-native φ². The result touches the open question of obtaining the observed spectral index without adjustable parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.