Foundational Numeric Interfaces

This module contains the small scalar interfaces shared by TorchLean's floating-point library and its tensor specifications. It deliberately knows nothing about tensors, models, runtimes, or verification.

MathFunctions names the transcendental operations used by numerical code. Numbers collects the few non-integral constants needed by scalar-polymorphic model definitions. The broader neural-model interface, Context, lives in NN.Spec.Core.Context and extends these foundations.

class MathFunctions (α : Type) : Type

Scalar transcendental functions shared by numerical and model code.

• exp : α → α
• tanh : α → α
• cosh : α → α
• sqrt : α → α
• abs : α → α
• log : α → α
• pi : α
• cos : α → α
• sin : α → α
• sinh : α → α

class Numbers (α : Type) : Type

Common scalar constants used by scalar-polymorphic model definitions.

• neg_point_five : α

  Backend representation of -0.5.

• neg_one : α

  Backend representation of -1.

• pointone : α

  Backend representation of 0.1.

• pointfive : α

  Backend representation of 0.5.

• one : α
• zero : α
• two : α

  Backend representation of 2.

• three : α

  Backend representation of 3.

• four : α

  Backend representation of 4.

• five : α

  Backend representation of 5.

• ten : α

  Backend representation of 10.

• log10 : α

  Backend representation of the natural logarithm of 10.

• log10000 : α

  Backend representation of the natural logarithm of 10000.

• epsilon : α

  Backend-supplied tolerance for numerically guarded formulas.

@[implicit_reducible]

instance instMathFunctionsFloat : MathFunctions Float

Host implementations of the scalar transcendental interface.

@[implicit_reducible]

noncomputable instance instMathFunctionsReal : MathFunctions ℝ

Exact-real interpretations of the scalar transcendental interface.

@[implicit_reducible]

instance instNumbersFloat : Numbers Float

Constants for Lean's host Float.

@[implicit_reducible]

noncomputable instance instNumbersReal : Numbers ℝ

Constants for exact-real specifications.

@[implicit_reducible]

instance instCoeNatFloat_nN : Coe ℕ Float

Coerce naturals into Lean's host Float.

@[implicit_reducible]

instance instCoeNatReal_nN : Coe ℕ ℝ

Coerce naturals into ℝ.

@[implicit_reducible]

instance instCoeNatRat_nN : Coe ℕ ℚ

Coerce naturals into ℚ.