InflationCert
plain-language theorem explainer
InflationCert packages the core RS inflation predictions into one structure: the attractor parameter equals φ + 1, α remains positive, the spectral index at 55 e-folds sits inside (0.96, 0.97), the modulation frequency Ω₀ is positive, and the curvature bound equals 1 in native units. Cosmologists comparing RS-derived spectra to CMB data would cite this certificate. The structure is assembled directly from five sibling lemmas with no additional reasoning steps.
Claim. A structure asserting that the attractor parameter satisfies $α = φ + 1$, that $α > 0$, that the spectral index at 55 e-folds lies in $(0.96, 0.97)$, that the modulation frequency $Ω_0 > 0$, and that the curvature bound $1/ℓ_0^2 = 1$ holds in RS-native units.
background
In the Recognition Science treatment of inflation the cost functional J induces self-similar potentials whose curvature scale is fixed by the golden ratio φ. The α-attractor parameter is defined as φ², which equals φ + 1 by the minimal polynomial of φ. The spectral index follows the slow-roll expression 1 − 2/N while Ω₀ = 2π / ln(π/φ) encodes the log-periodic modulation that arises from the eight-tick octave. The fundamental length ℓ₀ is normalized to 1, so the curvature bound at the recognition event R0 becomes |R| ≤ 1.
proof idea
The declaration is a structure definition. Its five fields are populated by direct reference to the lemmas alpha_attractor_eq_phi_plus_one, alpha_attractor_pos, n_s_at_55, Omega_0_pos, and curvature_bounded_at_R0.
why it matters
InflationCert collects the RS-specific inflationary observables and is instantiated by the theorem inflation_cert. It realizes the predictions stated in the module documentation: α = φ², n_s ≈ 1 − 2/N, r ≈ 12φ²/N², and Ω₀ ≈ 9.47. The construction rests on the self-similarity of J and the eight-tick period that sets the modulation frequency. No open questions are flagged in the surrounding code.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.