alpha_inflaton
plain-language theorem explainer
The definition sets the α-attractor parameter to φ^{-2} in the reals, with φ the golden ratio. Cosmologists modeling small-field alpha-attractor inflation inside RS baryogenesis cite it for the inflaton potential V(χ) = V₀ tanh²(χ / √(6φ)). The assignment is a direct one-line definition with no lemmas or reductions.
Claim. The α-attractor parameter is defined by α = φ^{-2}, where φ is the golden ratio. This enters the inflaton potential as V(χ) = V₀ tanh²(χ / (√6 φ)) in the inverse parameterization convention.
background
The RS Baryogenesis module derives a parameter-free matter-antimatter asymmetry from nine ledger parities that select a unique CP-odd channel. It fixes CP-odd couplings λ_CP = φ^{-7} and κ_CP = φ^{-9}, the recognition mass M_rec = 2√(2π) M_Pl, and the baryon asymmetry η_B ≈ 5.1 × 10^{-10}. The module adopts the inverse convention for the α-attractor, setting α = φ^{-2} to realize small-field inflation with Planck suppression, while noting that the natural convention α = φ² yields equivalent spectra once the number of e-foldings is adjusted.
proof idea
The declaration is a direct definition that assigns the real power phi raised to negative two. No lemmas are invoked; the body is a one-line assignment.
why it matters
This supplies the α parameter consumed by alpha_inflaton_alt (which rewrites it as (φ-1)^2 via φ² = φ + 1 and extracts n_s ≈ 1 - 2/N) and by alpha_inflaton_pos (which proves positivity). It completes the inflaton parameterization step required by the RS Baryogenesis paper, linking to the phi fixed point (T6) and the eight-tick octave (T7) of the forcing chain. The inverse convention choice keeps spectral predictions intact while embedding Planck-scale suppression.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.