Numerical arrays in transverse-momentum-dependent parton distribution (TMD) extractions can share units and dimensions while representing different observations. Caching a fitted dependency can change the function being optimized while leaving reference-point predictions unchanged.

typed-TMD combines Python runtime contracts, which record observation semantics, scientific context and statistical problem, with a finite-expression language that makes parameter dependencies and variation masks explicit. A checker for dependency-safe caching is proved sound in Lean 4.21.0: accepted plans preserve the full parameterized function on the declared variation domain for any fixed pure interpretation. A category of parameter interfaces with admitted substitutions shows how cached constructions compose. The framework is applied to an external arTeMiDe/SV19 Drell–Yan fit and to a two-parameter diagnostic regression.

Lean checks dependency soundness, cache constancy, the concrete validator, substitution and interpretation laws, and fixed-slice transport. The Drell–Yan one-parameter fits and the reparameterization regression validate the runtime contracts, with four five-start external fits taking about 217 s.