A Property Kind Calculus for Measurement Metrology

19.8. Worked examples (checked facts)🔗

Thirteen examples reproduce a headline number (or a theorem) as a #guard, so the UncertaintyExamples library building under CI is what makes the claims true rather than asserted — the project's reflection-tests discipline applied to metrology. The first two are the Stage-0 reference numbers; the next two are the Stage-1 autograd and ladder facts; the next two are the Stage-2 SSPRC pipeline and its ladder theorems; the last seven are the Stage-3 adequacy carrier, its per-site theorems, the Stage-3.1 DAG capstone A3′, the Stage-3.2 binary32 Sterbenz, the Stage-3.3 executable↔spec bridge, the Stage-3.4 Axis-U significance coupling, and the Stage-3.6 direct-simulation closure.

  • PropertyKindCalculus.UncertaintyExamples.DegenhardtFictive — the non-linear fictive model Y = (X_1 + X_2^2)\,X_3 of Degenhardt  (Degenhardt et al., 2025)Johannes Degenhardt, Rainer Tutsch, Xiukun Hu, and Gaoliang Dai (2025). “A practically oriented, efficient alternative to the Monte Carlo method for measurement uncertainty estimation”. Metrologia. 62(2). §3.1, with a normal, a uniform, and a triangular input. The Monte Carlo reference gives E(Y) \approx 11.60, u(Y) \approx 1.70 (matching the paper's 11.5875, 1.691); the reference value R = f(E(X)) = 11.25, and the gap E(Y) - R = 0.34 is the non-linearity signature of the X_2^2 term — exactly what the linearized rungs cannot see. The GUM cross-check gives u_c \approx 1.662, visibly under the Monte Carlo value: the linearization drops the curvature, which is the whole motivation for the higher rungs.

  • PropertyKindCalculus.UncertaintyExamples.WillinkGaugeBlock — the gauge-block calibration of Willink  (Willink, 2005)Robin Willink (2005). “A procedure for the evaluation of measurement uncertainty based on moments”. Metrologia. 42(5). Table 4 (the GUM example H.1), evaluated by the cumulants method: combining the six error variables' variances and fourth cumulants gives u_Y = 33.4\,\mathrm{nm}, excess \gamma_Y = 0.124, and a 99% expanded-uncertainty half-width h_{0.99} = 87.6\,\mathrm{nm} — 5% narrower than the GUM procedure's 93 nm at the same coverage, because the (mostly negative) fourth cumulants pull the tails of the output toward normal. That narrowing is the difference between the GUM rung and the Willink rung, reproduced as a checked number.

  • PropertyKindCalculus.UncertaintyExamples.DegenhardtSensitivity — the Stage-1 autograd bridge on the same fictive kernel: interpreting it at the reverse-mode tape carrier returns the sensitivity coefficients (c_1, c_2, c_3) = (5, 5, 2.25) to machine precision (matching the hand-computed \partial Y/\partial X_i at the means), and feeding them through gumStdUnc reproduces u_c = 1.662 exactly — the write-once model differentiated with no rewrite.

  • PropertyKindCalculus.UncertaintyExamples.LadderNesting — T1/T2 applied to a concrete all-Gaussian term list over ℝ (gum = willink|κ₄=0 as a closed proof term, #print axioms confirming no sorryAx), together with the executable Float shadow of the collapse: for normal-only inputs the Willink 95% half-width is exactly 1.96\,u_c.

  • PropertyKindCalculus.UncertaintyExamples.DegenhardtSsprc — the Stage-2 SSPRC pipeline on the same fictive model  (Degenhardt et al., 2025)Johannes Degenhardt, Rainer Tutsch, Xiukun Hu, and Gaoliang Dai (2025). “A practically oriented, efficient alternative to the Monte Carlo method for measurement uncertainty estimation”. Metrologia. 62(2).: 100 systematic samples per input (300 model evaluations against the Monte Carlo reference's 20 000, a factor \approx 67) recover E(Y) = 11.5875 — including the non-linear +0.3375 offset the linearized rungs cannot produce — and u(Y) \approx 1.69, closer to the Monte Carlo value than GUM's 1.662; the actual convolution (runConv) reproduces the moment read-off to machine precision.

  • PropertyKindCalculus.UncertaintyExamples.SsprcNesting — the T3/T4/T5 ladder theorems applied to two concrete centered distributions over ℝ: convolution adds their cumulants (T5), the convolved combined deviation has exactly the Willink cumulants (41, -1186) (T3), and an all-centered (affine) input list yields a centered combined deviation, so E(Y) = R (T4) — with #print axioms confirming no sorryAx.

  • PropertyKindCalculus.UncertaintyExamples.AdequacySwamping — the executable Adequacy carrier on two write-once kernels: bias + x with a small input uncertainty is flagged swamped under a large accumulator (10^8, where \tfrac12\,\mathrm{ulp}_{32} = 4 > 1) and certifies clean under a small one (100); a − b of near-equal uncertain operands is flagged catastrophic cancellation (relative uncertainty ≥ 100%) and certifies clean when the operands are well separated — the same kernel, checked for free at each configuration.

  • PropertyKindCalculus.UncertaintyExamples.AdequacyLadder — the adequacy theorems A1 (absorption, \mathrm{round}_8(80+1) = 80), A2 (Sterbenz, 3 - 2 of two FLX 24 numbers is FLX 24), and A3 (the verdict biconditional) applied to concrete values over ℝ, with #print axioms confirming no sorryAx.

  • PropertyKindCalculus.UncertaintyExamples.AdequacyDag — the Stage-3.1 capstone A3′ instantiated on concrete model DAGs (a three-input accumulator, an add/sub variant, a deeper five-input tree): the FP32 measurand's variation over an input box equals the ℝ one up to the DAG-additive rounding budget, and exactly when no site rounds (flag-free) — again with #print axioms confirming no sorryAx.

  • PropertyKindCalculus.UncertaintyExamples.AdequacySterbenz32 — the Stage-3.2 A2 lift to the genuine binary32 format: \mathrm{round}_{32}(u - v) = u - v and (a - b).\mathrm{val} = a.\mathrm{val} - b.\mathrm{val} for near-equal representable binary32 values (so the sub32_within_half_ulp bound collapses to zero), tied back to the self-contained FLX 24 fact — with #print axioms confirming no sorryAx.

  • PropertyKindCalculus.UncertaintyExamples.AdequacyExecBridge — the Stage-3.3 executable↔spec bridge: the ULP query ulpExp? and absorption test absorbs run on concrete float32 bit patterns (#guard: at 2^{25} the ULP is 4, so a perturbation of 1 is absorbed and 4 is not; at 10^8 the ULP is 8, so 1 is absorbed and 8 is not), while exec_verdict proves that whenever the kernel reports absorption the exact real sum rounds back under \mathrm{round}_{32} — the computed verdict equal to the specified one, with #print axioms confirming no sorryAx.

  • PropertyKindCalculus.UncertaintyExamples.AdequacyCoupling — the Stage-3.4 kind-typed coupling: one analyzeQ on the Degenhardt descriptors yields kinded contributions (c_i u_i) = (1.0, 1.30, 0.28) at \mathrm{measurandY} whose quadrature reproduces the GUM combined uncertainty u_c = 1.662359 exactly, and certifies the model adequate at that scale; #check_failure probes make the metrological conflations (sensitivity↔uncertainty, heterogeneous quadrature, CouplingResultQ field swap) type errors; and a 10^8-accumulator swamps a contribution (one absorption), with contribution_absorbed_at_scale applying the A3 verdict at that scale, #print axioms confirming no sorryAx.

  • PropertyKindCalculus.UncertaintyExamples.AutogradDirectSim — the Stage-3.6 closure instantiated concretely: the vectorization homomorphisms at a 3-vector shape; the compiled product graph x_0 \cdot x_1 with direct_PR_soundness_compiled (the runtime dense reverse pass succeeds and its input-prefix realises the adjoint of the Fréchet derivative) and its inhabited forward simulation; an eager two-leaf/mul runtime tape whose shape-total-closure hypothesis is discharged constructor by constructor; and, via the eager-provenance addendum, EagerBuilds witnessing that runtime tape with direct_PR_soundness_eager giving the endpoint on it — no compilation involved — with #print axioms pinning the classical trio only.