fNL_observed
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the value of f_NL from the phi-ladder or J-cost axioms.
- Does not include the uncertainty interval reported by Planck.
- Does not connect f_NL to higher-order terms in the Recognition Composition Law.
formal statement (Lean)
212noncomputable def fNL_observed : ℝ := -2
proof body
Definition body.
213
214/-! ## Implications -/
215
216/-- RS predictions for CMB observations:
217
218 1. **n_s - 1 ≈ -1/(8φ³)**: Testable with Planck precision
219 2. **r ≈ (φ-1)⁴ ≈ 0.02**: Testable by CMB-S4
220 3. **Running ≈ 0**: Consistent with observations
221 4. **f_NL ≈ 0**: Small non-Gaussianity -/