Foundational Numeric Interfaces #

This module re-exports FloatLib's elementary-function interface and supplies TorchLean's native binary32 instance and natural-number casts. It knows nothing about tensors, models, or runtimes.

MathFunctions names the transcendental operations used by numerical code. Integer and rational constants use the standard numerical interfaces. The broader neural-model interface, Context, lives in NN.Spec.Core.Context.

FloatLib owns the single MathFunctions class and its Float and ℝ instances. Its elementary capability module imports real analysis; this facade does not define a second class or duplicate those instances.

source

def TorchLean.normalizationEpsilon {α : Type} [RatCast α] :

Default normalization stabilizer, obtained by casting the exact rational 1e-5 once.

Native and configured binary contexts round the fraction without first casting its denominator. This preserves the representable binary16 tolerance even though 100000 itself overflows there. The result can still be zero in a format that cannot represent a nearby positive value; callers using such a format must choose an explicit positive tolerance.

Instances For

source

@[instance_reducible]

instance instMathFunctionsFloat32_nN :

MathFunctions Float32

Native binary32 implementations of the scalar transcendental interface.

source

@[instance_reducible]

instance instNatCastFloat_nN :

NatCast Float

Cast naturals into Lean's host Float.

source