planckMeasurements
plain-language theorem explainer
planckMeasurements records the 2018 Planck satellite constraints on the scalar spectral index, tensor-to-scalar ratio, and non-Gaussianity as a reference string. Cosmologists testing Recognition Science inflation models against data would cite these values to check slow-roll predictions. The definition is a direct string literal with no computation or lemmas applied.
Claim. The 2018 Planck measurements are given by $n_s = 0.9649 ± 0.0042$, $r < 0.06$ (95% CL), and $f_{NL} = 0.9 ± 5.1$.
background
The Cosmology.Inflation module derives inflation from J-cost slow roll, identifying the inflaton with the J-cost field whose minimum lies at argument 1. Near this point the cost behaves quadratically, producing a flat region that drives exponential expansion and resolves the horizon, flatness, and monopole problems. Upstream structures calibrate the underlying J function: PhiForcingDerived.of supplies the J-cost structure while DAlembert.LedgerFactorization.of handles the positive-real multiplicative group and its calibration.
proof idea
The definition is a direct string literal assignment of the quoted Planck values. No lemmas are invoked and no tactics are used; the body simply returns the fixed string.
why it matters
This definition supplies the observational benchmark for the COS-001 J-cost inflation mechanism, allowing direct comparison of derived slow-roll parameters to the reported n_s and r bounds. It supports the module's listed falsification criteria and anchors the framework's inflation claims to external data without downstream theorem dependencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.