19.2. Two orthogonal axes, and why their properties compose
A science model is written once as a carrier-polymorphic kernel over [NumCarrier α] (the WO1
discipline of the previous chapter). On top of that single source sit two orthogonal
parametrization axes:
-
the numeric carrier
R(Axis N) — how the numbers are represented:ℝfor proof, an autograd tape for sensitivity,FP32/RIntervalfor numerical adequacy,CudaT/ Tensor for GPU execution,Floatfor a fast CPU reference; -
the uncertainty descriptor (Axis U) — what is known about an input's dispersion: a per-quantity distribution carrying its moments, an inverse cumulative distribution function, and a support range.
The value of parametrizing both is that the guarantees compose — the same model yields a proof, a sensitivity, a numerical-adequacy certificate, and a GPU run as different interpretations, not as four re-implementations:
-
Proof carrier (
ℝ). The three uncertainty methods below are one provably nested ladder; numerical adequacy is a theorem, not a heuristic. -
the autograd tape (sensitivity). Exact sensitivity coefficients
c_i = \partial f/\partial X_ifor the linearized methods, and local surrogates for the sampling method. -
the uncertainty descriptor (noise). Measurement uncertainty becomes a first-class, composable property of a quantity, in the spirit of the VIM.
-
FP32/RInterval(no information loss). A certificate that the model does not silently drop a small-but-significant input uncertainty — at the scale that the same descriptor defines. -
Float/CudaT(fast execution). The identical model runs, batched, on CPU and GPU.