19.1. Why formalize this? What the rigor buys🔗

Uncertainty analysis is routinely done in a spreadsheet or a NumPy script, so casting it in a proof assistant earns its keep only by buying something those tools cannot. It buys five things — each exercised by a checked example below, not asserted here.

The published numbers are re-derived under CI, not transcribed. Each worked example reproduces a headline figure of its source paper as a #guard, so the UncertaintyExamples library building is what certifies the figure. Degenhardt's fictive model (UncertaintyExamples.DegenhardtFictive, its GUM answer cross-checked against a Monte Carlo reference) and Willink's gauge block (UncertaintyExamples.WillinkGaugeBlock, by the cumulants method) reproduce their papers' u_c, excess \gamma_Y, and expanded-uncertainty half-widths to the printed digits.
The method hierarchy is a theorem, so the three methods cross-validate for free. GUM ⊂ Willink ⊂ SSPRC is a chain of proved homomorphisms (T2, T3, resting on T5), not a slogan. Wherever their hypotheses hold the three answers must agree; a discrepancy is a modelling error or a broken proof, caught mechanically rather than by eye (UncertaintyExamples.SsprcNesting pins the shared cumulants (41, -1186)).
The sensitivity coefficients are proved equal to the derivative, not merely computed. The c_i = \partial f/\partial X_i the two linearized rungs need come from one reverse pass over the write-once model (the sensitivity bridge); since Stage 3.5 that reverse pass is proved to be the adjoint of the Fréchet derivative, an endpoint that holds on the very tape the bridge builds. A c_i entering a budget is therefore correct by theorem, not by trust in an autograd library (UncertaintyExamples.DegenhardtSensitivity returns (5, 5, 2.25) and reproduces u_c = 1.662).
"No information loss" is decided, not hoped for — and at the scale that matters. The hazard this half of the chapter guards is silent: a small-but-significant input uncertainty rounded away in floating point, corrupting the result with no error raised. The adequacy carrier detects exactly that, and its verdict is sound and complete — the flag fires iff a contribution is genuinely lost — at the half-ulp scale the same descriptor defines. UncertaintyExamples.AdequacySwamping flags a contribution swamped under a 10^8 accumulator and certifies the small-accumulator variant clean, while UncertaintyExamples.AdequacyCoupling drives the significance coupling — the uncertainty budget and the adequacy check from one descriptor list — so a UQ-analysed model is simultaneously adequacy-checked at its own uncertainty scale.
One model serves proof, differentiation, execution, and certification with no re-implementation. All of the above are interpretations of a single write-once kernel at different carriers, so the proved model and the model that runs cannot drift apart — they are one source. The next section makes this composition precise; the working consequence is that an edit to the model is proved, differentiated, run, and adequacy-checked from the one definition.

None of this substitutes for measurement, or for judgement about which distribution an input follows. What it removes is a specific class of silent errors:

a mis-stated propagation law — the combine rules are derived, not asserted: GUM and Willink are proved projections of the finer method (T2, T3), so a wrong law surfaces as a broken proof or a numerical cross-validation mismatch rather than a plausible-looking answer;
a sensitivity taken on trust — the coefficients c_i are proved equal to the adjoint of the Fréchet derivative on the very tape the sensitivity bridge builds (eager provenance), not read off an unverified autograd library;
an uncertainty contribution quietly lost to rounding — the adequacy carrier detects absorption, and its verdict is sound and complete at the half-ulp scale the same descriptor defines, so a swamped contribution is reported, not dropped in silence.

The uncertainty formalism turns each into an obligation the build must discharge.