2.10. Uncertainty and numerical adequacy (R14, R15, R18)🔗

R14 — Output uncertainty is computed by a provably nested ladder of methods. A measured input quantity carries not just a magnitude but a dispersion; given the uncertainty of the inputs of a model Y = f(X_1,\dots,X_k), the calculus computes the uncertainty of Y. The dispersion is an additive descriptor placed alongside a quantity — moments and cumulants, an inverse-CDF sampler, and a support range — never a change to the carrier tower, the same discipline R11 used for vectors. Three methods estimate the output uncertainty at increasing fidelity and cost: GUM linearization (combine variances), Willink's cumulants method (combine the second and fourth cumulants, recovering the tail shape), and the derivative-free SSPRC sampling method (propagate each input separately and combine by convolution, capturing full non-linearity). The organizing claim is that these form a provably nested ladder \mathrm{GUM} \subset \mathrm{Willink} \subset \mathrm{SSPRC}: each coarser method is a projection of the finer one, all resting on the additivity of cumulants under independent summation. The linearized methods' sensitivity coefficients c_i = \partial f/\partial X_i are not hand-supplied — they come from instantiating the write-once model at an autograd carrier, R10's representation parametricity put to a new use. This requirement is realized through Stages 1–2: the reference Monte Carlo propagator, the GUM and Willink combines (reproducing both source papers' headline numbers as checked facts), the autograd coefficients, the derivative-free SSPRC pipeline (recovering the fictive model's full non-linear output uncertainty at ~67× fewer model evaluations than Monte Carlo), and all five ladder theorems — cumulant additivity (T1), \mathrm{gum} = \mathrm{willink}|_{\kappa_4 = 0} (T2), convolution adds cumulants (T5), Willink as the (\kappa_2,\kappa_4)-projection of the linearized SSPRC (T3), and the affine reference equalling the mean (T4) — are proved over ℝ. The development is the Uncertainty quantification and numerical adequacy chapter, and the full design is recorded in the project's UNCERTAINTY.md.

R15 — A floating-point representation is numerically adequate iff it loses no information at the scale of the input uncertainties. R10 gives a model exact reals to prove with and IEEE floats to run with; R15 asks the sharper question the pairing makes possible — does the floating-point representation silently drop an input uncertainty that matters? "Matters" is made precise by R14's descriptor: the scale is the input dispersion itself, which is exactly why the two areas share one descriptor rather than being two features. The textbook failure becomes checkable — an input whose contribution c_i\,u_i falls below half a unit in the last place of the accumulated sum is numerically invisible, a silent corruption of the uncertainty result; its dual is exact-by-Sterbenz cancellation that nonetheless amplifies relative uncertainty. Because the model is written once over [NumCarrier α], the check is obtained for free by instantiating it at an analysis carrier that tracks each value's magnitude and carried uncertainty and flags swamping and harmful cancellation — sound because the swamping threshold is exactly half a ulp, proved on the rounding grid over ℝ and grounded in TorchLean's binary32 FP32 unit-in-the-last-place lemmas and its proven interval arithmetic. This requirement is realized through Stage 3: the executable Adequacy carrier (a NumCarrier running the swamping and cancellation checks over Float, with a worked flagged/clean example pair), and the three theorems over ℝ — A1 absorption (a sub-½-ulp perturbation is invisible, its converse fixing the threshold), A2 Sterbenz (near-equal subtraction is exact, its dual amplifying relative uncertainty), and A3 verdict soundness (the flag holds iff the contribution is lost — sound and complete). Stage 3.1 then lifts A3 to the whole evaluation: A3′ (DagBound) abstracts a write-once model as a binary32 +/− DAG and proves that the FP32 measurand's variation over an input box reproduces the exact ℝ variation up to a DAG-additive rounding budget (composed from the per-operation FP32 half-ulp bounds), collapsing to equality when no site rounds anywhere — so rounding is the sole source of the gap. Stage 3.2 then discharges the FLT-level Sterbenz: a TorchLean PR (neural_generic_format_FLT_sterbenz) lifts A2 from the self-contained FLX model to the gradual-underflow format binary32 actually uses (fexp32), so \mathrm{round}_{32}(u - v) = u - v for near-equal representable operands is a theorem about the real rounding operator (round32_sterbenz_exact), and a near-equal binary32 subtraction is lossless. Stage 3.3 then closes the executable↔spec gap: since Lean's host Float is an opaque FFI type no theorem can constrain, a second TorchLean PR gives TorchLean's computable IEEE32Exec model an executable ULP query (ulpExp?, its answers proved equal to ulp₃₂, answering on exactly the finite fragment) and an absorption test (absorbs, the float32 sum unchanged) that is sound against the specification — when it fires, the exact real sum rounds back under round₃₂ (exec_verdict_sound). So the computed adequacy verdict is provably the specified one, the residual Float32 ↔ IEEE32Exec step being an upstream assumption typeclass rather than an axiom. Stage 3.4 then wires the Axis-U significance yardstick: analyze drives both areas from one InputDist descriptor — instantiating a single write-once kernel at the autograd carrier for the sensitivities cᵢ and at the adequacy carrier (seeded from the same descriptor) for the verdict — so a model is adequacy-checked at the scale cᵢ·uᵢ its own uncertainty descriptor defines (the soundness inherited from the A3 verdict). What remains is extending the DAG to ×/÷, scoped in the project's UNCERTAINTY.md.

R18 — The recorded variance certifies a coverage interval. Once an output's uncertainty is a distribution, VIM 2.36–2.38 ask for a coverage interval — a probability attached to an interval about the mean. The variance the R14 descriptor already carries must certify one, in two tiers graded by what is assumed about the distribution's shape: distribution-free, the interval of k standard uncertainties about the mean has coverage at least 1 - 1/k^2 — the complement of Chebyshev's inequality, honest but conservative (k = 2 gives \ge 75\%, not the Gaussian 95\%, which is a shape assumption); and, for a bounded family, exact — the centered interval of half-width h of a uniform on [m - \delta, m + \delta] has coverage exactly h/\delta. Neither tier needs a true value — the sense in which coverage is provable while accuracy, closeness to nature, is not. The development is the Coverage intervals section of the uncertainty chapter.