19.5. The SSPRC method and the lower ladder rungs
The two linearized rungs replace the model by its gradient at the input means. The SSPRC method
(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). does no such thing: it keeps the
full model but evaluates it cheaply by sampling each input systematically and propagating each
one separately. Its four steps are systematic sampling (each input at the equidistant probabilities
P_j = (j-\tfrac12)/N_i through its inverse CDF), separated propagation (vary one input, hold the
rest at their means, form the deviations a_{i,j} = f(\dots,x_{i,j},\dots) - R from the reference
R = f(E(X))), reconstruction of each input's deviation distribution, and convolution of those
distributions into the measurand's. Because the sample counts add (N_s = \sum_i N_i) rather
than multiply, it reaches Monte Carlo fidelity at a fraction of the model evaluations — and, keeping
the full model, it recovers the non-linear mean the linearized rungs cannot.
The SSPRC pipeline: from the model, the input descriptors, and a per-input sample count, produce the
combined (E(Y), u(Y)) by systematic sampling, separated propagation, and convolution — a
derivative-free method whose evaluation budget is additive in the inputs.
Lean code for Definition19.5.1●1 definition
Associated Lean declarations
-
defdefined in PropertyKindCalculus/Uncertainty/Ssprc.leancomplete
def PropertyKindCalculus.Uncertainty.Ssprc.run (model : List Float → Float) (inputs : List (PropertyKindCalculus.Uncertainty.InputDist Float)) (ns : List ℕ) : Float × Float
def PropertyKindCalculus.Uncertainty.Ssprc.run (model : List Float → Float) (inputs : List (PropertyKindCalculus.Uncertainty.InputDist Float)) (ns : List ℕ) : Float × Float
**SSPRC combined uncertainty `(E(Y), u(Y))`** read directly from the per-input deviation distributions. `E(Y) = R + Σ E(Aᵢ)` and `Var(Y) = Σ Var(Aᵢ)` — means and variances add under convolution, so the (combinatorially large) convolution is not needed for the moments. The `Σ E(Aᵢ)` term is the non-linearity correction the linearized rungs cannot produce.
Realized (Stage 2, Ssprc.run) over the Float carrier. run reads E(Y) = R + \sum_i E(A_i) and
\mathrm{Var}(Y) = \sum_i \mathrm{Var}(A_i) off the per-input deviation distributions (means and
variances add under convolution, so the combinatorial convolution need not be materialized);
runConv performs the actual discrete convolution and agrees, cross-checking the engine. On the
Degenhardt fictive model with 100 systematic samples per input — 300 evaluations against the Monte
Carlo reference's 20 000 — it returns E(Y) = 11.5875 (recovering the non-linear +0.3375 offset
that GUM cannot see) and u(Y) \approx 1.69, closer to the Monte Carlo value than GUM's 1.662 (the
DegenhardtSsprc example).
Convolution adds cumulants (T5). For independent centered probability distributions the second and
fourth cumulants are additive under convolution: \kappa_r(d_1 \star d_2) = \kappa_r(d_1) +
\kappa_r(d_2) for r \in \{2,4\}. Equivalently the cumulant map is a homomorphism from the
convolution operation onto the Cumulants monoid. This is the mathematical bridge under T3.
Lean code for Theorem19.5.2●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Uncertainty/Convolution.leancomplete
theorem PropertyKindCalculus.Uncertainty.Dist.cumulantsOf_conv (d1 d2 : PropertyKindCalculus.Uncertainty.Dist) (h1 : d1.IsProb) (h2 : d2.IsProb) (c1 : d1.IsCentered) (c2 : d2.IsCentered) : (d1.conv d2).cumulantsOf = d1.cumulantsOf + d2.cumulantsOf
theorem PropertyKindCalculus.Uncertainty.Dist.cumulantsOf_conv (d1 d2 : PropertyKindCalculus.Uncertainty.Dist) (h1 : d1.IsProb) (h2 : d2.IsProb) (c1 : d1.IsCentered) (c2 : d2.IsCentered) : (d1.conv d2).cumulantsOf = d1.cumulantsOf + d2.cumulantsOf
**T5 (homomorphism form).** `cumulantsOf` carries convolution to the `Cumulants` monoid's addition: `cumulantsOf (d₁ ⋆ d₂) = cumulantsOf d₁ + cumulantsOf d₂`. Convolution ↦ cumulant addition — the bridge underpinning T3, stated once.
Realized over ℝ (Convolution.lean): convolution is defined as the distribution of the sum of
independent contributions — every pairwise sum weighted by the product — and the additivity is
proved from the factorization of the joint expectation (kappa2_conv, kappa4_conv; the
-3\,E[X^2]^2 correction is exactly what cancels the cross term 6\,E[X^2]E[Y^2] in the fourth
moment of the sum), not assumed. Sorry-free (#print axioms → propext, Classical.choice,
Quot.sound).
Willink is the (\kappa_2,\kappa_4)-projection of the linearized SSPRC (T3). If each input's
deviation distribution is a centered probability distribution realizing its declared moments, then
the cumulants of the convolved combined deviation are exactly the Willink combined cumulants
(\sum_i c_i^2 u_i^2,\ \sum_i c_i^4 w_i). So convolving the separately-propagated inputs and
truncating at the fourth cumulant reproduces \mathrm{willink} — the lower edge of the ladder,
whose upper edge is T2. Rests on
convolution adding cumulants.
Lean code for Theorem19.5.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Uncertainty/Convolution.leancomplete
theorem PropertyKindCalculus.Uncertainty.cumulantsOf_combinedDeviation (xs : List PropertyKindCalculus.Uncertainty.SensitizedInput) (hp : ∀ t ∈ xs, t.2.1.IsProb) (hc : ∀ t ∈ xs, t.2.1.IsCentered) (hk2 : ∀ t ∈ xs, t.2.1.kappa2 = t.2.2.variance) (hk4 : ∀ t ∈ xs, t.2.1.kappa4 = t.2.2.fourthCumulant) : (PropertyKindCalculus.Uncertainty.combinedDeviation xs).cumulantsOf = PropertyKindCalculus.Uncertainty.willinkCumulants (PropertyKindCalculus.Uncertainty.termsOf xs)
theorem PropertyKindCalculus.Uncertainty.cumulantsOf_combinedDeviation (xs : List PropertyKindCalculus.Uncertainty.SensitizedInput) (hp : ∀ t ∈ xs, t.2.1.IsProb) (hc : ∀ t ∈ xs, t.2.1.IsCentered) (hk2 : ∀ t ∈ xs, t.2.1.kappa2 = t.2.2.variance) (hk4 : ∀ t ∈ xs, t.2.1.kappa4 = t.2.2.fourthCumulant) : (PropertyKindCalculus.Uncertainty.combinedDeviation xs).cumulantsOf = PropertyKindCalculus.Uncertainty.willinkCumulants (PropertyKindCalculus.Uncertainty.termsOf xs)
**T3 — Willink is the `(κ₂,κ₄)`-projection of the linearized SSPRC.** If each input's deviation distribution `Zᵢ` is a centered probability distribution realizing its declared moments (`κ₂ Zᵢ = uᵢ²`, `κ₄ Zᵢ = wᵢ`), then the cumulants of the convolved combined deviation are *exactly* the Willink combined cumulants `(Σcᵢ²uᵢ², Σcᵢ⁴wᵢ)`. So convolving the separately-propagated inputs and truncating at the fourth cumulant reproduces `willink` — the lower rung of the ladder.
Realized over ℝ (cumulantsOf_combinedDeviation): induction over the input list, each step the
scaling law \kappa_r(c_i \cdot Z_i) = c_i^{\,r}\,\kappa_r(Z_i) followed by the convolution
homomorphism T5, landing on willinkCumulants term by term. Together with T2 this closes the ladder
\mathrm{GUM} \subset \mathrm{Willink} \subset \mathrm{SSPRC} as a chain of homomorphisms
(the SsprcNesting example applies it to concrete distributions, pinning (\kappa_2,\kappa_4) =
(41, -1186)). Sorry-free.
The SSPRC reference equals the mean for an affine model (T4). When every input's deviation
distribution is centered — the case of a linear/affine model — the combined deviation is centered, so
the reference value R = f(E(X)) equals E(Y). The non-linearity signature E(Y) - R is exactly
the non-vanishing of \sum_i c_i\,E(Z_i) when a deviation distribution is not centered — the gap
the Degenhardt fictive example exhibits (0.3375) and the linearized rungs structurally miss.
Lean code for Theorem19.5.4●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Uncertainty/Convolution.leancomplete
theorem PropertyKindCalculus.Uncertainty.combinedDeviation_isCentered (xs : List PropertyKindCalculus.Uncertainty.SensitizedInput) (hc : ∀ t ∈ xs, t.2.1.IsCentered) : (PropertyKindCalculus.Uncertainty.combinedDeviation xs).IsCentered
theorem PropertyKindCalculus.Uncertainty.combinedDeviation_isCentered (xs : List PropertyKindCalculus.Uncertainty.SensitizedInput) (hc : ∀ t ∈ xs, t.2.1.IsCentered) : (PropertyKindCalculus.Uncertainty.combinedDeviation xs).IsCentered
Realized over ℝ (combinedDeviation_isCentered, with mean_combinedDeviation giving the general
gap \sum_i c_i\,E(Z_i)): the mean of a convolution is the sum of the means (weighted by the unit
totals), so a fold of centered contributions is centered. Sorry-free.