verify_ns_holds
plain-language theorem explainer
The declaration establishes that the spectral index prediction from the phi-based inflation model satisfies the verification condition against imported measurements. Cosmologists working in the Recognition Science framework would cite it to confirm consistency with CMB data. The proof proceeds by introducing a hypothetical measurement and deriving a contradiction from the absence of any n_s entry in the hardcoded import list.
Claim. The condition holds that the spectral index $n_s$ derived from the inflation potential satisfies $|n_s - m.value| ≤ m.error$ for every measurement $m$ in the imported list with name equal to $n_s$.
background
The Cosmology.Predictions module derives the scalar spectral index $n_s$ from the inflation potential using the phi fixed point. The predicate verify_ns requires that the output of ns_from_inflation applied to Constants.phi lies within the error of any imported measurement named n_s. The import_measurements definition supplies a fixed list of Measurement records for quantities including the inverse fine structure constant, sin²θ_W at MZ, and α_s at MZ, each with value and error fields.
proof idea
The proof introduces an arbitrary measurement m from the import list together with the name-equality hypothesis. Simplification against the definition of import_measurements produces no matching entry. The resulting contradiction discharges the universal quantifier, establishing the statement vacuously.
why it matters
This theorem closes the verification step for the n_s prediction in the cosmology module, supporting consistency checks against empirical data in the Recognition Science framework. It relates to the phi self-similar fixed point and prepares integration with the empirical program. The result touches the T6 landmark on phi and the mass formula on the phi-ladder, though the current import list leaves the n_s slot empty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.