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.
• Context.isZero includes differentiation metadata, unlike the primal-only comparisons of dual numbers. Composite carriers lift this test through every component.
• Context.pointwise lists the pointwise operators of Spec.PointwiseOp whose meaning depends on the scalar type, such as torch.div and torch.erf. The default lists none, so a graph evaluator reports them as unsupported for that type.
• Interval backends supply their own order/comparison operations; Context does not require a linear order or agreement between these operations and real-number comparisons.

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 : α → α → α
• sqrtNat (value : ℕ) : α

  Construct a square-root constant from a natural count.

  The default takes the square root after casting. Binary backends retain that path when the cast does not overflow, but use FloatLib's exact rational-root algorithm otherwise. A dimension can exceed the scalar range even when its square root is representable.

• isZero (value : α) : Bool

  Test for zero including differentiation metadata.

  Ordinary scalars use Boolean equality. Dual and compound scalars must inspect every component: a zero primal with a nonzero tangent is not a constant zero in a differentiated expression.

• 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.

• sigmoid : α → α

  Branch-stable sigmoid. Differentiation carriers apply its complete weighted chain rule.

• log1p : α → α

  Compensated log(1 + x). Differentiation carriers supply its analytic chain rule.

• expm1 : α → α

  Compensated exp x - 1. Differentiation carriers supply its analytic chain rule.

• 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.

• pointwise : Spec.PointwiseTable α

  Pointwise operators whose meaning depends on the scalar type, with that meaning.

  Each entry returns the result or the reason why the scalar type has none. Exact carriers give the reason at poles and outside the real domain, where IEEE arithmetic returns an infinity or a NaN in every format. A real result too large for a binary format is still a result. An omitted operator is unsupported for the type: evaluators report it and never substitute an approximation.

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.

def Context.floatPointwise : Spec.PointwiseTable Float

Host binary64 meanings of the pointwise operators the native runtime provides directly.

Division and square root are the correctly rounded IEEE operations, and the truncating quotient rounds the IEEE quotient toward zero, as PyTorch does. pow is the C library's power function. Flooring division needs an exact remainder and erf needs an error function, neither of which the host interface provides, so both are unsupported here.

def Context.float32Pointwise : Spec.PointwiseTable Float32

Host binary32 meanings of the pointwise operators, as floatPointwise describes them.

@[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.