Scalar

Spec-only scalar conventions.

These aliases fix their scalar to ℝ for mathematical reasoning. Typed tensors and model execution also support native Float/Float32 and FloatLib configured binary scalars through Context.

Because SpecScalar is ℝ, this module brings in Mathlib's real-analysis hierarchy. It does not provide the real Context instance; import NN.Spec.Core.Context.Real for that. Anything that only needs Float or a general [Context α] should import NN.Spec.Core.Context and stay light.

References / context:

• TorchLean paper (overall scalar-polymorphic architecture and trust boundary discussion): arXiv:2602.22631.
• IEEE 754-2019 is the reference point for the executable Float32 model (ExecFloat.Binary 8 23) used in the runtime/numerics layers (not this file).

@[reducible, inline]

abbrev Spec.SpecScalar : Type

Spec scalars live in ℝ.

@[reducible, inline]

abbrev Spec.SpecTensor (s : Shape) : Type

Spec tensors are Real-typed tensors.