The identities §4.8.1 states, checked against the table

theorem mi_eq_5280_ft : (sym "mi").Agree ((num 5280).mul (sym "ft"))

mi is exactly 5280 × ft (§4.8.1 customary table).

theorem mi_factorization :
    (sym "mi").scale.exp = Scale.exp
      [(.prime ⟨2, Nat.prime_two⟩, 4), (.prime ⟨3, Nat.prime_three⟩, 2),
       (.prime ⟨5, Nat.prime_five⟩, -3), (.prime ⟨11, by norm_num⟩, 1),
       (.prime ⟨127, by norm_num⟩, 1)]

mi is 201168/125 m = 2⁴ · 3² · 5⁻³ · 11 · 127 m, the factorization the spec writes out.

theorem lb_eq_short_ton_div_2000 : (sym "lb").Agree ((sym "short_ton").div (num 2000))

lb is exactly short_ton / 2000.

theorem short_ton_eq_ug : (sym "short_ton").Agree ((num 907184740000).mul (sym "ug"))

short_ton is exactly 907184740000 ug — InMAP’s conversion constant.

theorem torr_eq_atm_div_760 :
    (sym "Torr").Agree ((sym "atm").div (num 760)) ∧
    (sym "Torr").Agree (mk pressure (20265 / 152))

Torr is exactly atm / 760, i.e. 20265/152 Pa.

theorem torr_ne_mmHg : ¬ (sym "Torr").Agree (sym "mmHg")

Torr is NOT mmHg: same dimension, different exact scale.

theorem inHg_eq_25_4_mmHg : (sym "inHg").Agree ((num 25.4).mul (sym "mmHg"))

inHg is exactly 25.4 × mmHg.

theorem psi_eq_lbf_per_in2 :
    (sym "psi").Agree
      ((((num 9.80665).mul (sym "lb")).mul ((sym "m").mul ((sym "s").rpow (-2)))).div
        (((num 0.0254).mul (sym "m")).rpow 2))

psi is lbf/in²: lb × 9.80665 m/s² over (0.0254 m)².

theorem hp_eq_550_ft_lbf_per_s :
    (sym "hp").Agree
      (((((num 550).mul (sym "ft")).mul (sym "lb")).mul (num 9.80665)).mul
        ((sym "m").mul ((sym "s").rpow (-3))))

hp is 550 ft·lbf/s = 550 × ft × lb × 9.80665 W, exactly.

theorem yr_julian :
    sym "yr" = sym "year" ∧
    (sym "yr").Agree (mk time 31557600) ∧
    (sym "yr").Agree ((num 365.25).mul (sym "day"))

yr = year = the Julian year, 31557600 s = 365.25 day.

theorem deg_eq_pi_div_180 :
    (sym "deg").dim = angle ∧ Scale.real (sym "deg").scale = Real.pi / 180

deg is π/180 rad: dimension rad¹, real scale π / 180.

theorem sr_eq_rad_sq : (sym "sr").Agree ((sym "rad").rpow 2)

sr = rad².

theorem dimensionless_entries :
    ∀ k ∈ ["ppm", "ppb", "ppt", "ppmv", "ppbv", "pptv", "%", "percent", "psu",
      "molec", "molecule", "individuals", "vehicles", "units", "count",
      "", "1", "dimensionless"], (sym k).dim = 0

The mixing ratios, fractions and counts are dimensionless.

theorem percent_and_counts :
    (sym "%").Agree (num 0.01) ∧ (sym "percent").Agree (num 0.01) ∧
    ∀ k ∈ ["molec", "molecule", "individuals", "vehicles", "units", "count", "psu"],
      (sym k).Agree U.one

% (and percent) is dimensionless at scale exactly 0.01; the counts are dimensionless at scale 1 (not mol, not cd).

theorem C_is_coulomb : (sym "C").Agree ((sym "A").mul (sym "s")) ∧ (sym "C").dim .K = 0

C is the coulomb, A·s — no temperature component.

theorem dobson :
    (sym "DU").Agree (mk ((-2 : ℚ) • len) 2.6867e20) ∧ sym "Dobson" = sym "DU" ∧
    Scale.real (sym "DU").scale = 2.6867e20

DU and Dobson have dimension m⁻² and scale exactly 2.6867e20.

theorem customary_scales :
    Scale.real (sym "ft").scale = 0.3048 ∧ Scale.real (sym "mi").scale = 1609.344 ∧
    Scale.real (sym "lb").scale = 0.45359237 ∧
    Scale.real (sym "hp").scale = 550 * 0.3048 * 0.45359237 * 9.80665 ∧
    Scale.real (sym "gal").scale = 0.003785411784 ∧
    Scale.real (sym "inHg").scale = 3386.388640341 ∧
    Scale.real (sym "Torr").scale = 101325 / 760 ∧
    Scale.real (sym "psi").scale = 0.45359237 * 9.80665 / 0.0254 ^ 2 ∧
    Scale.real (sym "degF").scale = 5 / 9 ∧
    Scale.real (sym "BTU").scale = 1055.05585262

The pinned customary scales (§4.8.1 “A binding MUST use the values above”): each entry’s real scale is the stated exact value.

theorem mi_per_h : ((sym "mi").div (sym "h")).Agree (mk (len - time) 0.44704)

mi/h is exactly 0.44704 m/s, the constant MOVES’s SQL writes.

theorem gal_eq_231_in3 :
    (sym "gal").Agree ((num 231).mul (((num 0.0254).mul (sym "m")).rpow 3))

gal is 231 in³ with the international inch 0.0254 m.

theorem hp_fold_left_to_right :
    fmul (fmul (fmul (rn (550 : ℚ)) (rn 0.3048)) (rn 0.45359237)) (rn 9.80665)
      = rn (745.6998715822702 : ℚ) ∧
    rn (745.6998715822702 : ℚ) = rn (550 * 0.3048 * 0.45359237 * 9.80665 : ℚ)

The left-to-right binary64 fold ((550 × ft) × lb) × 9.80665, from the doubles nearest each literal, lands on the double nearest 745.6998715822702, which is also the double nearest the exact product.

theorem hp_fold_order_matters :
    fmul (fmul (fmul (rn (550 : ℚ)) (rn 0.3048)) (rn 9.80665)) (rn 0.45359237)
      ≠ fmul (fmul (fmul (rn (550 : ℚ)) (rn 0.3048)) (rn 0.45359237)) (rn 9.80665) ∧
    rn (550 * 0.3048 * 0.45359237 * 9.80665 : ℚ) ≠ 550 * 0.3048 * 0.45359237 * 9.80665

The fold order matters: ((550 × ft) × 9.80665) × lb lands on a different double, and the exact product is not a double.