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)Marginal noteRobert 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); and
the conformity-assessment layer (ISO/IEC Guide 98-4): tolerance and acceptance limits as bound roles, the guard band derived from a stated risk or from the costs of being wrong, a deployed band read as coverage or systematic under one classification rule (with its NaN rule), and the ratchet theorem that lets an acceptance limit tighten itself.

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.