verify_ns
plain-language theorem explainer
verify_ns defines the predicate requiring that any imported measurement labeled n_s lies within error of the value computed by ns_from_inflation at Constants.phi. A cosmologist checking Recognition Science inflation predictions against CMB data would cite this predicate. The definition is a direct universal quantification over the static measurement list, which evaluates vacuously in the current data.
Claim. The proposition that for every measurement record $m$ in the imported list, if $m$ is named $n_s$ then $|n_s(φ) - m.value| ≤ m.error$, where $n_s(φ) = 1 - 2/(60(φ-1))$ and $φ$ is the self-similar constant drawn from the CPM constants bundle.
background
The Cosmology.Predictions module derives the scalar spectral index from an inflation potential. The upstream definition ns_from_inflation supplies the approximate formula $1 - 2/(60(φ-1))$ obtained from the potential shape. Constants is the structure from LawOfExistence that bundles the real parameters required by the model, accessed here through the .phi field. import_measurements returns a fixed list of Measurement records, each carrying a name, value and error; the supplied list contains entries for the inverse fine-structure constant, sin²θ_W and α_s but no n_s entry. The local setting is therefore a self-contained check of the inflation-derived n_s against the available data.
proof idea
The declaration is a direct definition of the Prop as the stated universal quantification. It applies ns_from_inflation to Constants.phi inside the absolute-value comparison and restricts the check to records whose name equals n_s. No lemmas are invoked and no tactics appear; the body is the predicate itself.
why it matters
verify_ns is the target of the theorem verify_ns_holds, which establishes that the predicate holds (vacuously, because the measurement list contains no n_s entry). It supplies the verification step that closes the inflation-prediction chain in the cosmology module. In the Recognition Science framework the predicate connects the phi self-similar fixed point (T6) used to shape the inflation potential to an observable quantity, completing one link from the core functional equation to CMB data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.