A Property Kind Calculus for Measurement Metrology

19.3. The input uncertainty descriptor🔗

Definition19.3.1
Group: The uncertainty layer rests on one additive descriptor placed alongside a quantity's magnitude. It has two faces, matching its two consumers: carrier-parametric moment data (what the linearized methods consume and what the ℝ -level theorems are proved about), and a sampler (the inverse-CDF, the single primitive shared by the Monte Carlo and systematic methods). The support range is carried too, because it is exactly the datum the numerical-adequacy check needs — the architectural hinge that makes the two halves of this chapter one design. (28)
Group member previews
Preview
Definition 19.3.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

The moment data of an input: its mean, variance (\kappa_2 = u^2), fourth cumulant (\kappa_4 = w), and third cumulant (\kappa_3, asymmetry). Carrier-parametric — a bare record over any R — so it exists at ℝ for proofs and Float for execution alike. The cumulant constants of the named distributions (normal, uniform, triangular, arc-sine) are the values tabulated by Willink  (Willink, 2005)Robin Willink (2005). “A procedure for the evaluation of measurement uncertainty based on moments”. Metrologia. 42(5)..

Lean code for Definition19.3.1●1 definition
  • structure(4 fields)defined in PropertyKindCalculus/Uncertainty/InputDist.lean
    complete
    structure PropertyKindCalculus.Uncertainty.MomentData (R : Type) : Type
    structure PropertyKindCalculus.Uncertainty.MomentData
  (R : Type) : Type
    **Carrier-parametric moment/cumulant data** for an input quantity. `variance` is `κ₂ = u²`;
`fourthCumulant` is `κ₄ = w` (Willink Table 1), zero for a normal; `thirdCumulant` is `κ₃`
(asymmetry, zero for the symmetric families). Consumed by the linearized methods and proved
about over `ℝ`.

    Fields

    mean : R
    Expected value `E(Xᵢ)`. 
    variance : R
    Variance `u²` (the second cumulant κ₂). 
    fourthCumulant : R
    Fourth cumulant `w` (κ₄); `0` for a normal distribution. 
    thirdCumulant : R
    Third cumulant `κ₃` (asymmetry); `0` for symmetric distributions. (No default: `R` is an
unconstrained carrier, so there is no generic `0` to default to — set it at each site.)
Proof for Definition 19.3.1
uses 0

Realized. A four-field structure MomentData R; the named distributions are values built by smart constructors (InputDist.normal, .uniform, .triangular, .arcsine), each filling in its Willink-Table-1 cumulants — the open-world, values-not-constructors convention the whole project follows.

Definition19.3.2
Group: The uncertainty layer rests on one additive descriptor placed alongside a quantity's magnitude. It has two faces, matching its two consumers: carrier-parametric moment data (what the linearized methods consume and what the ℝ -level theorems are proved about), and a sampler (the inverse-CDF, the single primitive shared by the Monte Carlo and systematic methods). The support range is carried too, because it is exactly the datum the numerical-adequacy check needs — the architectural hinge that makes the two halves of this chapter one design. (28)
Group member previews
Preview
Definition 19.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

The input uncertainty descriptor: the moment data, an optional rigorous support [\mathrm{lo}, \mathrm{hi}], and an inverse-CDF sampler. Feeding a random probability to the sampler gives Monte Carlo; feeding a systematic probability (j-\tfrac12)/N gives the systematic sampling of the efficient method — one primitive, two methods.

Lean code for Definition19.3.2●1 definition
  • structure(3 fields)defined in PropertyKindCalculus/Uncertainty/InputDist.lean
    complete
    structure PropertyKindCalculus.Uncertainty.InputDist (R : Type) : Type
    structure PropertyKindCalculus.Uncertainty.InputDist
  (R : Type) : Type
    **The input uncertainty descriptor.** Carrier-parametric `moments`, an optional rigorous
`support` (for the numerical-adequacy check), and an `invCDF` sampler shared by MCM and SSPRC.

    Fields

    moments : PropertyKindCalculus.Uncertainty.MomentData R
    The carrier-parametric moments/cumulants. 
    support : Option (R × R)
    Rigorous support `[lo, hi]`, when the distribution is bounded (feeds numerical adequacy). 
    invCDF : Float → Float
    Inverse CDF: maps a probability `p ∈ (0,1)` to a sample. Random `p` ⇒ MCM; systematic
`p = (j-0.5)/N` ⇒ SSPRC. Concrete `Float`: sampling yields concrete numbers.
Proof for Definition 19.3.2
uses 0

Realized. InputDist R bundles MomentData with a support and an invCDF. The paired UncertainQuantity k R places it alongside a kinded Quantity k R as additive metadata, exactly the pattern R11 used for vector carriers — the carrier tower is untouched.