running_observed
plain-language theorem explainer
The declaration records the observed running of the spectral index as the constant -0.006. Cosmologists comparing Recognition Science predictions for the primordial spectrum to Planck CMB data would reference this value when testing whether the tilt exhibits phi-structure. It is supplied directly as a noncomputable real constant without derivation from the J-cost or phi-ladder inside the module.
Claim. The running of the spectral index is defined by $dn_s / d ln k := -0.006$.
background
The COS-009 module derives the primordial power spectrum from J-cost quantum fluctuations during inflation, with the phi-ladder fixing the spectral tilt n_s - 1. The running parameter measures scale dependence of that tilt. The upstream theorem from PrimitiveDistinction reduces seven axioms to four structural conditions plus three definitional facts that underwrite all subsequent constants.
proof idea
The definition is a direct constant assignment of the Planck 2018 central value.
why it matters
This constant anchors comparisons between Recognition Science predictions and CMB observations, supporting the module target of deriving the primordial spectrum from J-cost fluctuations and the paper proposition on the CMB spectral index from the golden ratio. It leaves open whether the running exhibits phi-structure when the tilt is quantized on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.