The real scalar dictionary

Spec.SpecScalar is ℝ, so every "paper theorem" ultimately runs through the instances here. They are kept out of NN.Spec.Core.Context because Context ℝ needs MathFunctions ℝ, and that drags in the whole real-analysis hierarchy; modules working at Float or at a general [Context α] should not pay for it.

@[instance_reducible]

noncomputable instance instContextReal : Context ℝ

Full Context instance for ℝ (proof backend, noncomputable).

instance instLawfulContextReal : LawfulContext ℝ

The real Context is built from Mathlib's field structure, so every law holds by rfl.