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 binary64 execution with a logical model and a separate native boundary),
• FloatLib configured binary values, with the exponent and fraction widths selected in their type (import NN.Spec.Core.FloatInstances for their adapters),
• interval enclosures for verification,
• ℝ (proof-level mathematics).

The scalar parameter serves several purposes:

• 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 compact model, state the proof-level contract, then run verification bounds. Rewriting each model for each phase is error-prone.
• A scalar-polymorphic specification keeps the layer and model definitions shared while the scalar instance determines their numerical meaning.
• Cross-checking happens at the scalar semantics layer, not inside duplicated model definitions.
• Context α is larger than a minimal arithmetic interface, but avoids duplicating architectures across execution, proof, and verification code.

Related work:

• 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 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.decidableGT is included so executable code can decide comparisons (e.g. ReLU / argmax). The derived global DecidableRel instance has low priority so native decision procedures win.
• LawfulContext α (below) records when a Context agrees with a Mathlib ordered field on α.
• The ℝ context dictionary lives in NN.Spec.Core.Context.Real and the opt-in rational one in NN.Spec.Core.Context.Rational. FloatLib's shared elementary-function class already imports real analysis; selecting a context does not add an accuracy theorem for finite-precision arithmetic.
• 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 Context (α : Type) extends Inhabited α, One α, Zero α, Add α, Sub α, Mul α, Div α, Neg α, Pow α α, Max α, Min α, BEq α, LT α, LE α, MathFunctions α, NatCast α, RatCast α, TorchLean.Numeric.QuotientArithmetic α : 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 : α → α
• natCast : ℕ → α
• ratCast : ℚ → α
• supported : Bool
• depth : ℕ
• addWithFlags : α → α → α × UInt8
• subWithFlags : α → α → α × UInt8
• mulWithFlags : α → α → α × UInt8
• divWithFlags : α → α → α × UInt8
• encode : α → Option (QuotientCoefficients (depth α))
• decode : QuotientCoefficients (depth α) → Option α
• copyPrimal : α → α → α
• defaultEpsilon : α

  Backend-selected safeguard used by default in guarded formulas; not machine epsilon.

• decidableGT : DecidableRel fun (x1 x2 : α) => x1 > x2

  Decision procedure for the scalar type's strict order.

• stopGradient? : Option (α → α)

  Remove differentiation metadata from a scalar at a detach boundary.

  Ordinary numeric carriers leave this as none, so detaching a tensor can reuse its storage. A carrier such as Dual α supplies a map that keeps the primal value and clears its tangents. This is needed when a reverse pass runs over dual numbers: cutting the tape edge alone would leave the detached value's forward tangent available to later operations.

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

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

def Context.stopGradient {α : Type} [Context α] (x : α) : α

Clear a scalar's differentiation metadata, if its carrier has any.

@[instance_reducible, instance 100]

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

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

The instance has low priority so that a type's own decision procedure (Real.decidableLT, Float.decLt, ...) wins whenever one exists.

Lawful contexts

Context α carries no laws: it only bundles operations. LawfulContext α records, for a scalar type that also carries a Mathlib ordered field structure, that the Context dictionary computes exactly the same operations. Generic proofs about scalar-polymorphic specifications can then rewrite the dictionary operations into the ordinary ring operations and finish with Mathlib.

Only exact facts are recorded. Transcendental constants (lnTen, pi, ...) and the total power operation are backend specific and stay unconstrained.

class LawfulContext (α : Type) [Context α] [Field α] [LinearOrder α] [IsStrictOrderedRing α] : Prop

Compatibility of a Context dictionary with a linearly ordered field structure on the same type.

Each field equates a Context projection (written with the explicit instance path Context.to*) with the corresponding Mathlib operation.

• add_eq (x y : α) : x + y = x + y

  Dictionary addition is ring addition.

• mul_eq (x y : α) : x * y = x * y

  Dictionary multiplication is ring multiplication.

• sub_eq (x y : α) : x - y = x - y

  Dictionary subtraction is ring subtraction.

• div_eq (x y : α) : x / y = x / y

  Dictionary division is field division.

• neg_eq (x : α) : -x = -x

  Dictionary negation is ring negation.

• zero_eq : Zero.zero = Zero.zero

  The dictionary zero is the ring zero.

• one_eq : One.one = One.one

  The dictionary one is the ring one.

• lt_iff (x y : α) : x < y ↔ x < y

  The dictionary strict order is the field order.

• le_iff (x y : α) : x ≤ y ↔ x ≤ y

  The dictionary order is the field order.

• max_eq (x y : α) : x ⊔ y = max x y

  Dictionary max is the lattice maximum.

• min_eq (x y : α) : x ⊓ y = min x y

  Dictionary min is the lattice minimum.

• beq_iff (x y : α) : (x == y) = true ↔ x = y

  Boolean equality decides propositional equality.

• natCast_eq (n : ℕ) : ↑n = ↑n

  The natural-number cast is the semiring cast.

• ratCast_eq (value : ℚ) : ↑value = ↑value

  The rational-number cast is the field cast.

• abs_eq (x : α) : MathFunctions.abs x = |x|

  The dictionary absolute value is the lattice absolute value.

• defaultEpsilon_pos : 0 < Context.defaultEpsilon

  The backend tolerance is strictly positive.

@[instance_reducible, inline]

instance instContextFloat : Context Float

Full Context instance for Float (runtime backend).

@[instance_reducible, inline]

instance instContextFloat32 : Context Float32

Full Context instance for native binary32 execution.