Foundational Numeric Interfaces

This module re-exports FloatLib's elementary-function interface and supplies TorchLean's native binary32 instance, native scalar casts, compensated log1p/expm1 formulas, and input-based sigmoid/tanh slopes and weighted pullbacks. Nested floating-point differentiation uses reciprocal cosh identities to retain small derivative coefficients near zero. The pullbacks reuse finite coefficient arithmetic when an intermediate slope or product loses range. Weighted square-root quotients use the same finite coefficient machinery. If the half exponential itself loses range, a bounded enclosure search evaluates the complete expression before rounding. This module knows nothing about tensors, model composition, 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.

def TorchLean.Numeric.sigmoid {α : Type} [Zero α] [One α] [Add α] [Div α] [Neg α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [MathFunctions α] [ops : QuotientArithmetic α] (x : α) : α

Logistic sigmoid with a nonpositive exponential argument on either branch.

If a checked sum loses range, finite coefficient arithmetic reconstructs the numerator and denominator together. A valid configured format need not represent 2, although it represents the sigmoid's result at zero. Unsupported carriers retain the ordinary branch formula.

def TorchLean.Numeric.Internal.average {α : Type} [RatCast α] [Add α] [Mul α] [ops : QuotientArithmetic α] (x y : α) : α

Average two derivative coefficients without losing a representable result during halving.

Ordinary products and addition keep their order. If a checked operation loses range, replay the complete average over finite coefficients and round only its result. The rational constant does not require the scalar type to represent 2. Nonfinite inputs keep the ordinary result.

def TorchLean.Numeric.Internal.sqrtBackward {α : Type} [NatCast α] [One α] [Mul α] [Div α] [ops : QuotientArithmetic α] (root seed : α) (factorFirst : Bool := false) : α

Apply the square-root chain rule using the root already computed by the forward pass.

factorFirst preserves the reverse rule's local-factor schedule; dual numbers divide the seed directly. If checked arithmetic loses range, replay the complete weighted quotient over finite coefficients. The constant 2 is then exact even when its scalar cast overflows. This recovers the quotient for the supplied, rounded root, not the analytic derivative before root rounding. Nonfinite inputs retain the ordinary result.

def TorchLean.Numeric.Internal.angleTangent {α : Type} [Zero α] [Add α] [Sub α] [Mul α] [Div α] [BEq α] [Max α] [MathFunctions α] [ops : QuotientArithmetic α] (x y dx dy : α) : α

Angular directional derivative at (x, y) in direction (dx, dy).

Scaling the coordinates avoids squaring large inputs. If a checked intermediate loses range, or the scaled products cancel, evaluate the complete finite quotient from the original inputs before rounding. A scaled seed can overflow even when the combined derivative is representable. The origin keeps its selected zero tangent; nonfinite inputs retain the ordinary formula. This does not assert differentiability across the principal angle's branch cut.

def TorchLean.Numeric.Internal.powerBackward {α : Type} [Zero α] [One α] [Sub α] [Mul α] [Pow α α] [BEq α] [ops : QuotientArithmetic α] (isZero : α → Bool) (base exponent seed : α) : α

Apply a constant-exponent power rule without rounding an out-of-range local factor first.

The ordinary arithmetic order is unchanged unless a checked intermediate loses range. Recovery encloses the complete weighted expression from the original inputs, including nested derivative coefficients. Nonfinite inputs, unsupported carriers and inconclusive bounds retain the ordinary result. The supplied zero predicate must inspect every differentiation coefficient.

def TorchLean.Numeric.Internal.powerTangent {α : Type} [Zero α] [Add α] [Mul α] [Div α] [BEq α] [MathFunctions α] [ops : QuotientArithmetic α] (base exponent power baseDirection exponentDirection : α) : α

Joint power tangent, retaining the forward pass's primal and ordinary arithmetic order.

If an intermediate loses range or the two terms cancel after rounding, bounded coefficient enclosures reconstruct the entire positive-base expression from the original base, exponent, and directions. The supplied forward value is used only by the ordinary path. Unsupported domains, nonfinite encodings and inconclusive bounds retain that ordinary result.

def TorchLean.Numeric.Internal.applySlope {α : Type} [Zero α] [One α] [Add α] [Mul α] [Div α] [Neg α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [BEq α] [RatCast α] [MathFunctions α] [ops : QuotientArithmetic α] (x : α) (seed : Option α) (isTanh : Bool) : α

Evaluate a sigmoid or tanh slope, optionally applying an incoming gradient.

Reciprocal cosh identities avoid cancellation near zero in nested floating-point derivatives. Ordinary scalar evaluation retains the decaying-exponential schedule. The half exponential avoids rounding the local slope to zero before applying its incoming gradient. If that intermediate loses range, the original input and seed feed a complete coefficient enclosure instead. An absent seed returns the slope itself, without an extra multiplication. Exposed callers need this helper visible for specialization.

def TorchLean.Numeric.sigmoidDeriv {α : Type} [Zero α] [One α] [Add α] [Mul α] [Div α] [Neg α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [BEq α] [RatCast α] [MathFunctions α] [QuotientArithmetic α] (x : α) : α

Sigmoid slope retaining small activation and derivative tails.

Unlike sigmoid x * (1 - sigmoid x), this retains a representable tail after the activation has rounded to one. Nested finite-precision carriers instead use 1 / (2 * (1 + cosh x)) to avoid cancellation in its derivatives near zero. The same range repair serves the standalone slope and weighted pullback. Selecting the sign of the exponential argument preserves the complex algebraic formula; taking its modulus would not.

def TorchLean.Numeric.tanhDeriv {α : Type} [Zero α] [One α] [Add α] [Mul α] [Div α] [Neg α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [BEq α] [RatCast α] [MathFunctions α] [QuotientArithmetic α] (x : α) : α

Tanh slope evaluated as the square of a scaled reciprocal cosh.

The ordinary scalar formula doubles the decaying exponential before squaring, instead of subtracting a rounded square from one. Nested finite-precision carriers use (1 / cosh x)^2, whose derivatives retain small inputs through sinh. Detected range loss uses the weighted pullback's repair; this also covers formats whose range cannot hold an intermediate 2.

def TorchLean.Numeric.sigmoidBackward {α : Type} [Zero α] [One α] [Add α] [Mul α] [Div α] [Neg α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [BEq α] [RatCast α] [MathFunctions α] [QuotientArithmetic α] (x seed : α) : α

Apply the sigmoid derivative to an incoming gradient without first losing its small tail.

Normal checked products retain the selected slope and multiplication. Differentiated carriers use reciprocal cosh identities and check the input, hyperbolic factor and slope for range loss. A factor rounded to one also requires the complete enclosure: its derivative coefficients can already have lost a product of small directions. This includes zero inputs at higher orders. Detected range loss otherwise replays the weighted slope from a rounded half exponential. If the input, half argument or exponential loses information, a bounded search encloses the complete expression from the original input and accepts only agreeing finite rounded coefficients. The search may fail to settle, in which case the staged repair is retained. Nested carriers use every coefficient, not primal-only equality. Unsupported carriers and nonfinite inputs retain ordinary arithmetic. The half-exponential approximation remains a separate source of error when that path is used.

def TorchLean.Numeric.tanhBackward {α : Type} [Zero α] [One α] [Add α] [Mul α] [Div α] [Neg α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [BEq α] [RatCast α] [MathFunctions α] [QuotientArithmetic α] (x seed : α) : α

Apply the tanh derivative to an incoming gradient, repairing intermediate range loss.

The cold path evaluates 4 * q^4 * seed / (1 + q^4)^2 from the rounded half exponential q = exp (-|x| / 2). If q or one of its coefficients loses range, an enclosure evaluates 4 * exp (-2 * |x|) * seed / (1 + exp (-2 * |x|))^2 before output rounding. An inconclusive search retains the staged repair. Unsupported carriers and nonfinite inputs use ordinary arithmetic. Nested carriers share the reciprocal-cosh calculation and range checks with sigmoidBackward.

def TorchLean.Numeric.log1p {α : Type} [One α] [Add α] [Sub α] [Mul α] [Div α] [BEq α] [MathFunctions α] (x : α) : α

Compensate rounding in 1 + x before taking its logarithm.

This retains a small argument when the addition rounds to one. Accuracy still depends on the scalar logarithm; the formula is not a correct-rounding guarantee.

def TorchLean.Numeric.expm1 {α : Type} [Zero α] [One α] [Sub α] [Mul α] [Div α] [Neg α] [BEq α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] [MathFunctions α] (x : α) : α

Evaluate exp x - 1 without losing small arguments to subtraction.

The logarithmic correction is restricted to the unit neighborhood, avoiding complex logarithm branch ambiguity. The zero-exponential branch handles underflow.

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.

@[instance_reducible]

instance instMathFunctionsFloat32_nN : MathFunctions Float32

Native binary32 implementations of the scalar transcendental interface.

@[instance_reducible]

instance instNatCastFloat_nN : NatCast Float

Cast naturals into Lean's host Float.

@[instance_reducible]

instance instNatCastFloat32_nN : NatCast Float32

Round naturals directly to binary32, without an intermediate binary64 rounding.

Machine-sized inputs use Lean's native integer conversion; larger naturals use its binary32 model.

@[instance_reducible]

instance instRatCastFloat_nN : RatCast Float

Round a rational once to native binary64 through FloatLib's binary model.

@[instance_reducible]

instance instRatCastFloat32_nN : RatCast Float32

Round a rational directly to native binary32, without an intermediate binary64 rounding.