NASA Jet Propulsion Laboratory formalizes a metrology quantity calculus in Lean 4