A Property Kind Calculus for Measurement Metrology

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/RInterval for numerical adequacy, CudaT/ Tensor for GPU execution, Float for 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_i for 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.