fNL_observed
plain-language theorem explainer
The declaration supplies the Recognition Science assignment for the local non-Gaussianity parameter f_NL as the constant -2. Cosmologists comparing single-field inflation models to Planck data would cite this value when checking RS consistency with observed CMB statistics. The definition is a direct constant assignment that matches the reported central value from Planck 2018.
Claim. The local non-Gaussianity parameter $f_{NL}$ is assigned the numerical value $-2$.
background
The Cosmology.PrimordialSpectrum module derives the primordial power spectrum from J-cost quantum fluctuations during inflation, with the phi-ladder fixing the spectral tilt and amplitude. The module states that the CMB reveals nearly scale-invariant fluctuations seeded by these J-cost effects, with n_s approximately 0.965 and amplitude 2.1 times 10 to the minus 9. The upstream result supplies a MetaRealizationCert recording structural properties required by the orbit and step coherence axioms in the self-reference structure.
proof idea
The definition is a direct constant assignment of -2, chosen to align with the Planck central value for local f_NL.
why it matters
This definition supplies the RS value for f_NL inside the COS-009 derivation of the primordial spectrum from J-cost fluctuations. It supports the module's listed implications for CMB observables, including small non-Gaussianity consistent with single-field slow-roll. The assignment touches the framework's prediction that f_NL remains small when the phi-ladder governs the spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.