The numeric carrier

The evaluator in LambdaS.Dynamics is generic in its numbers, and one definition serves both masters: the section below spells out the two instances.

Everything about units is carrier-independent, which is why the proofs never mention Num beyond threading it: unit soundness and erasure are statements about which branch an evaluator takes, not about arithmetic.

What the two instances demonstrate

ℝ and Float are the same definition read two ways. At ℝ the evaluator is the object the soundness and erasure theorems are about, and necessarily noncomputable since Real.exp is. At Float it is compiled to C. Nothing about units differs between them, which is the point: the dimensional content of the calculus is carrier-independent, and a carrier can be swapped (for complex amplitudes, intervals, dual numbers for differentiation) without touching the type system or a single theorem.

Positivity

npow and nlog are meaningful on positive arguments. Λs's pow is applied to positive magnitudes in practice, but the language does not enforce it, because enforcing it would exclude signed quantities from the calculus. For negative arguments, the two carriers use different conventions for non-integer powers. Real.rpow is the real part of the principal complex power, so (-8) ^ (1/3 : ℝ) denotes 1, not the real cube root. Float.pow returns NaN for a negative base and a non-integer floating-point exponent. This is a choice of totalization, not a claim that real odd roots do not exist. No theorem equates the compiled result with the real semantics. The invariance theory needs no positivity (relQ_rpow carries no sign hypothesis, because a positive scale factor distributes over rpow at every real base); Kennedy's Pi theorem still does.

The native kernel

LambdaS.Map proves the units of a linear map are rank-one (entry (j,i) carries δ_W(j)/δ_V(i)), so an m×n map needs m+n units rather than mn, and those live in the type. By the time a numeric kernel runs, the checker has discharged every dimensional obligation and the payload is a flat array of doubles: no tagging, no strides, no per-entry metadata.

That is the substantive claim, and these two declarations test it. Both are @[extern], so the compiled binary calls C (c/lambdas_blas.c); the Lean bodies are the fallbacks the interpreter uses and the definitions the theorems see. On Apple platforms the C calls Accelerate's cblas_ddot and cblas_dgemv; elsewhere it runs portable loops, so the build has no external dependency. blasBackend reports which was compiled in.

The trust boundary is the usual FFI one: the C is assumed to agree with the Lean body, and the compiled checks in LambdaS.QM exercise it on real data. The agreement has one precondition, that the flat array holds m × n doubles; the Lean body reads out of range through get! and the C checks the sizes and aborts. ddot truncates to the shorter vector in both.

@[extern lambdas_ddot]

def LambdaS.ddot (a x : FloatArray) : Float

Inner product of two flat vectors.

Equations

• One or more equations did not get rendered due to their size.

@[extern lambdas_dgemv]

def LambdaS.dgemv (m n : ℕ) (a x : FloatArray) : FloatArray

Matrix–vector product, a row-major m×n: one call per product, which is the shape cblas_dgemv wants.

Written as a map over Array.range rather than a push loop so that the size of the result is manifest: dgemv_size is what the soundness proof needs, and the C is trusted to agree with this body.

Equations

• LambdaS.dgemv m n a x = { data := Array.map (fun (i : ℕ) => List.foldl (fun (s : Float) (j : ℕ) => s + a.get! (i * n + j) * x.get! j) 0.0 (List.range n)) (Array.range m) }

@[simp]

theorem LambdaS.dgemv_size (m n : ℕ) (a x : FloatArray) : (dgemv m n a x).data.size = m

@[extern lambdas_blas_backend]

def LambdaS.blasBackend : Unit → String

Which numeric backend the binary was compiled against.

Equations

• LambdaS.blasBackend x✝ = "Lean fallback"

class LambdaS.Num (R : Type) : Type

The numeric operations an evaluator needs.

• ofRat : ℚ → R
• add : R → R → R
• mul : R → R → R
• div : R → R → R
• npow : ℚ → R → R

  A constant rational power. Primitive because it is not definable from the field operations; see LambdaS.NonDef.sqrt_not_definable.

• nlog : R → R
• nexp : R → R
• le : R → R → Bool

  Comparison. The one observation a conditional makes. Quantities are comparable only at a common unit (T-IfLe), which is what keeps this invariant: rescaling multiplies both sides by the same positive factor.

• dot : List R → List R → R

  Inner product. Defaulted to a fold; carriers with a native kernel override it.

• matVec : List (List R) → List R → List R

  Batched matrix–vector product, the operation eval performs when it applies a linear map. Defaulted to a row-at-a-time fold; carriers with a native kernel override it with a single call.

• matVec_length (M : List (List R)) (x : List R) : (matVec M x).length = M.length

  The result has one entry per row. A law rather than a theorem, because the overriding instance decides how the product is computed and the soundness proof needs the length regardless.

@[instance_reducible]

noncomputable instance LambdaS.instNumReal : Num ℝ

The carrier the theorems are about. Noncomputable, as Real.exp forces.

Equations

• One or more equations did not get rendered due to their size.

class LambdaS.OrderedNum (R : Type) extends LambdaS.Num R : Type

Carriers whose comparison survives a rescaling.

Separate from Num on purpose: the evaluator needs le to run, but only the abstraction theorems need it to be invariant, and Float cannot supply that. Multiplication rounds, so c * x and c * y can compare differently from x and y at subnormals and near overflow. Making this a field of Num would therefore have forced either a false law or a sorry.

The split is the honest one and it is the same split the development already draws elsewhere: theorems over ℝ, binary over Float, with the places they part ways pinned rather than papered over (QM.boundaryChecks). The abstraction theorems live in the denotational semantics over ℝ and never mention this class, so nothing here is newly unproved; Float has never satisfied an arithmetic identity and was never asked to.

What differs is the consequence of rounding. In add and mul it perturbs a number. In le it changes which branch runs, so a unit change can alter control flow rather than the last bits, and that is the failure a user would actually be ambushed by.

The guarantee worth telling a user is sharper than this law. Multiplication by a power of two is exact in IEEE 754, so a rescaling by 2^k preserves comparisons on the nose and this law does hold at Float in that case. It is also the case that matters: a compiler rescaling to keep magnitudes near 1 picks binary powers because they are free and exact. Rescale by 2^k and control flow is preserved; rescale by 3.28 and it need not be. Outside that case a branch can flip only when the two sides are within rounding of each other, which means the comparison was ill-conditioned regardless of units.

Positivity is not decoration. At c = 0 both products collapse to zero and the comparison is decided by reflexivity rather than by x and y, so the law is false without it. Rescalings are positive by construction, Scaling living in log space, so the hypothesis is discharged wherever this is used.

• ofRat : ℚ → R
• add : R → R → R
• mul : R → R → R
• div : R → R → R
• npow : ℚ → R → R
• nlog : R → R
• nexp : R → R
• le : R → R → Bool
• dot : List R → List R → R
• matVec : List (List R) → List R → List R
• matVec_length (M : List (List R)) (x : List R) : (matVec M x).length = M.length
• le_scale (c x y : R) : Num.le c (Num.ofRat 0) = false → Num.le (Num.mul c x) (Num.mul c y) = Num.le x y

@[instance_reducible]

noncomputable instance LambdaS.instOrderedNumReal : OrderedNum ℝ

ℝ is the carrier the abstraction theorems are stated over, so it is the one that has to satisfy the law.

Equations

• LambdaS.instOrderedNumReal = { toNum := LambdaS.instNumReal, le_scale := LambdaS.instOrderedNumReal._proof_1 }

@[instance_reducible]

instance LambdaS.instNumFloat : Num Float

Real double precision.

npow is bare Float.pow: even on positive bases its result is a floating-point approximation, not an equality with Real.rpow. On a negative base with a non-integer exponent it returns NaN, while Real.rpow uses the real part of the principal complex power. Mathlib also has 0 ^ q = 0 for nonzero q and x / 0 = 0, unlike floating-point infinities and NaNs. QM.boundaryChecks tests selected conventions in the binary.

Equations

• One or more equations did not get rendered due to their size.