19. Uncertainty quantification and numerical adequacy🔗

The representation-parametric quantity of R10 carries a model's numbers at whatever carrier a task needs:

ℝ to prove,
Float to run,
FP32 to bound rounding.

This chapter puts that parametricity to work on two questions a metrology model must answer but the calculus so far does not:

given the uncertainty of the input quantities, what is the uncertainty of the output? and
does the floating-point representation of the model lose information that matters at the scale of those uncertainties?

Both are developed against one shared, additive descriptor placed on a quantity — never a change to the carrier tower. The design is recorded in full in the project's UNCERTAINTY.md; this chapter is its blueprint face. Stages 0–3 are built and CI-checked (each item below links to the formal node that realizes it):

the reference layer and worked examples,
the GUM and Willink combines,
the autograd sensitivity coefficients,
the derivative-free SSPRC pipeline,
the five ladder theorems:
- T1, cumulant additivity;
- T2, \mathrm{gum} = \mathrm{willink}|_{\kappa_4=0};
- T3, Willink as the projection of the linearized SSPRC;
- T4, affine reference equals the mean;
- T5, convolution adds cumulants, and
the numerical-adequacy layer:
- the executable analysis carrier;
- the per-site theorems:
  - A1 absorption,
  - A2 Sterbenz,
  - A3 verdict soundness over ℝ;
  - the universal capstone A3′ over an arbitrary model DAG and input box;
  - A2 lifted to the genuine binary32 format fexp32; and
- the executable↔spec bridge, certifying the runtime absorption verdict against the round₃₂ specification on TorchLean's computable IEEE32Exec model (George et al., 2026)Robert Joseph George, Jennifer Cruden, Will Adkisson, Xiangru Zhong, Huan Zhang, and Anima Anandkumar (2026). “TorchLean: Formalizing Neural Networks in Lean”. arXiv preprint arXiv:2602.22631 (cs.MS). .; and
- the Axis-U significance wiring, coupling the autograd c_i with the descriptor's u_i into the significance scale c_i u_i the adequacy carrier checks against (Stage 3.4); and
- its heterogeneous generalization, the kinded ×/÷ budget DAG, whose ProductKind/QuotientKind edges are threaded through a multi-node graph and whose threaded propagation collapses to the flat quadrature (residual 2).

Since Stage 3.5 the sensitivity coefficients are also proved correct — the reverse pass is the adjoint of the Fréchet derivative — and Stage 3.6 carries that endpoint from the compiled tape (direct simulation) to the tape the bridge actually builds (eager provenance). The kinded ×/÷ budget DAG (residual 2) is realized, its threaded propagation proved to collapse to the flat quadrature.