Context α: scalar interface for models + proofs

TorchLean is designed to be scalar-polymorphic: the same model/layer definitions can be instantiated over many numeric backends:

• Float (fast execution; trusted runtime semantics),
• TorchLean.Floats.IEEE754.IEEE32Exec (executable bit-level IEEE-754 binary32),
• interval enclosures for verification (see NN/Floats/Interval/*),
• ℝ (proof-level mathematics).

Why we designed it this way:

• We did not want separate "Float model code", "proof model code", and "verification model code" that slowly diverge and become inconsistent.
• In practice, we iterate across phases: execute a small model, state the proof-level contract, then run verification bounds. Rewriting each model for each phase is error-prone.
• A single scalar-polymorphic spec gives one source of truth for layers/models, while letting us swap numeric meaning by changing the scalar instance.
• This keeps cross-checking honest: if behavior changes between backends, the difference is visible at the scalar semantics layer, not hidden inside duplicated model definitions.
• The tradeoff is a slightly larger scalar interface (Context α), but we accept that complexity to keep architecture-level duplication low and proofs/reuse high.

Some relevant literature we were following / taking inspiration from:

• Bezanson et al., "Julia: A Fresh Approach to Numerical Computing" (generic numeric code across many scalar types; performance via specialization): https://arxiv.org/abs/1411.1607
• Spitters and van der Weegen, "Type classes for mathematics in type theory" (typeclass-based algebraic interfaces for reusable formalization and instances): https://doi.org/10.1017/S0960129511000119
• Elliott, "The Simple Essence of Automatic Differentiation" (one abstract formulation specialized to multiple concrete semantics/representations): https://arxiv.org/abs/1804.00746
• Mirman et al., "The Fundamental Limits of Interval Arithmetic for Neural Networks" (why interval backends are useful and where they become conservative): https://arxiv.org/abs/2112.05235

Our Context α is the same engineering pattern in a Lean setting: one model/layer definition, many scalar interpretations, and explicit tradeoffs about semantics.

To make this practical, we collect the numeric operations required by neural networks into a single typeclass:

Context α

This is intentionally broader than a standard algebraic structure: it bundles arithmetic, ordering, and common transcendental functions (exp/tanh/log/sqrt) used by activations and losses.

Notes

• Many spec definitions assume [Context α] so they can be re‑used at multiple dtypes.
• For "paper theorems", the spec layer fixes Spec.SpecScalar := ℝ (see NN/Spec/Core/Scalar.lean).
• Context.decidable_gt is included so executable code can decide comparisons (e.g. ReLU / argmax).
• For executable examples, Context.gtBool converts x > y into a printable Bool.
• For interval arithmetic, we override some order/comparison behavior (see namespace Interval below).

class MathFunctions (α : Type) : Type

Scalar transcendental functions used in activations and losses.

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

class Numbers (α : Type) : Type

Common scalar constants used in model definitions.

• neg_point_five : α
• neg_one : α
• pointone : α
• pointfive : α
• one : α
• zero : α
• two : α
• three : α
• four : α
• five : α
• ten : α
• log10 : α
• log10000 : α
• epsilon : α
• neg_thousand : α

Friendly aliases: these keep the original names (MathFunctions, Numbers) and give more descriptive names for scalar-facing code.

@[reducible, inline]

abbrev ScalarMath (α : Type) : Type

Alias for MathFunctions.

@[reducible, inline]

abbrev ScalarConstants (α : Type) : Type

Alias for Numbers.

class Context (α : Type) extends Inhabited α, One α, Zero α, Add α, Sub α, Mul α, Div α, Neg α, Pow α α, Max α, Min α, BEq α, LT α, LE α, MathFunctions α, Numbers α, Coe ℕ α : Type

The full scalar interface required by spec‑level tensors and models.

• default : α
• one : α
• zero : α
• add : α → α → α
• sub : α → α → α
• mul : α → α → α
• div : α → α → α
• neg : α → α
• pow : α → α → α
• max : α → α → α
• min : α → α → α
• beq : α → α → Bool
• lt : α → α → Prop
• le : α → α → Prop
• exp : α → α
• tanh : α → α
• cosh : α → α
• sqrt : α → α
• abs : α → α
• log : α → α
• pi : α
• cos : α → α
• sin : α → α
• sinh : α → α
• neg_point_five : α
• neg_one : α
• pointone : α
• pointfive : α
• two : α
• three : α
• four : α
• five : α
• ten : α
• log10 : α
• log10000 : α
• epsilon : α
• neg_thousand : α
• coe : ℕ → α
• decidable_gt : DecidableRel fun (x1 x2 : α) => x1 > x2

def Context.gtBool {α : Type} [Context α] (x y : α) : Bool

Decide x > y as a Bool using the Context's decidable_gt.

@[implicit_reducible]

instance instDecidableRelGt_nN {α : Type} [Context α] : DecidableRel fun (x1 x2 : α) => x1 > x2

A Context includes a decidable > relation; expose it as a standard typeclass.

@[implicit_reducible]

instance instMathFunctionsFloat : MathFunctions Float

MathFunctions instance for Lean's Float (runtime-oriented backend).

@[implicit_reducible]

noncomputable instance instMathFunctionsReal : MathFunctions ℝ

MathFunctions instance for ℝ (proof backend, noncomputable).

@[implicit_reducible]

instance instNumbersFloat : Numbers Float

Numbers literals for Float (runtime-oriented backend).

@[implicit_reducible]

noncomputable instance instNumbersReal : Numbers ℝ

Numbers literals for ℝ (proof backend, noncomputable).

@[implicit_reducible]

instance instCoeNatFloat_nN : Coe ℕ Float

Coerce naturals into Float using Float.ofNat.

@[implicit_reducible]

instance instCoeNatReal_nN : Coe ℕ ℝ

Coerce naturals into ℝ via the standard Nat-to-real coercion.

@[implicit_reducible]

instance instCoeNatRat_nN : Coe ℕ ℚ

Coerce naturals into ℚ via the standard Nat-to-rational coercion.

A lightweight ℚ backend

Context includes transcendental functions and real-valued exponentiation (Pow α α) because many models (softmax, tanh, etc.) need them when instantiated over Float / ℝ / interval scalars.

For ℚ, most transcendental functions do not map rationals to rationals, so there is no canonical exact interpretation. TorchLean therefore does not install the rational Context globally. Purely algebraic tests can opt in explicitly with:

open scoped NN.Spec.RationalAlgebraic

Current policy:

• abs is exact.
• pow x y is supported only when y is an integer rational (y.den = 1); otherwise it returns 0.
• Other transcendental functions are defined as 0 only in this explicitly scoped algebraic backend. This makes accidental softmax/GELU/tanh-over-ℚ use a typeclass error by default.

@[implicit_reducible]

def NN.Spec.RationalAlgebraic.instPowRatRat : Pow ℚ ℚ

Pow ℚ ℚ instance used for the lightweight rational backend.

Policy: support x^y only when y is an integer rational (y.den = 1); otherwise return 0. The instance is scoped so it is unavailable unless the caller explicitly opens NN.Spec.RationalAlgebraic.

@[implicit_reducible]

def NN.Spec.RationalAlgebraic.instMathFunctionsRat : MathFunctions ℚ

MathFunctions ℚ dictionary for the lightweight rational backend.

Only abs is meaningful; other transcendental functions are defined as 0 in this scoped backend and should not be used for semantic claims. Keeping this scoped makes unsupported transcendental rational models fail at elaboration unless a file deliberately opts into the algebraic-test backend.

@[implicit_reducible]

def NN.Spec.RationalAlgebraic.instNumbersRat : Numbers ℚ

Numbers ℚ dictionary for the lightweight rational backend.

The transcendentals (log10, etc.) are defined as 0 in this scoped backend; the basic rational literals are exact.

@[implicit_reducible]

def NN.Spec.RationalAlgebraic.instContextRat : Context ℚ

Full opt-in Context dictionary for exact rational algebraic fragments.

@[implicit_reducible]

instance instContextFloat : Context Float

Full Context instance for Float (runtime backend).

@[implicit_reducible]

noncomputable instance instContextReal : Context ℝ

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