The unit registry table (esm-spec §4.8.1)
The flat table, exactly as written in §4.8.1: a symbol is in it, spelled exactly,
or it does not resolve. Each entry is built from the scale the spec STATES for it,
so the identities in Esm.Units.Identities
are checks of the table rather than
restatements — with three exceptions, where the spec states the scale AS a
product: hp (550 × 0.3048 × 0.45359237 × 9.80665), psi
(0.45359237 × 9.80665 / 0.0254²) and Torr (101325/760). Their identities
confirm only that those products agree with the ft, lb and atm entries;
the independent check on hp is its binary64 fold (hp_fold_left_to_right
).
Scales the spec does not state are the SI definitions the symbol names (km is
1000 m, bar is 10⁵ Pa, …), except for three choices recorded as questions in
the phase-1 report: cal (thermochemical 4.184 J — the spec names no
calorie), and the scales of the mixing ratios ppm/ppb/ppt (the spec calls
them dimensionless and gives no scale; ppt is read as 10⁻¹², parts per
trillion), each matching every binding.
def D (m kg s mol K A cd rad : ℚ) : Dim
A dimension from its eight exponents, in axis order.
def mk (d : Dim) (q : ℚ) : U
A registry entry: a dimension and an exact positive rational scale.
def mkPi (d : Dim) (q : ℚ) (k : ℚ) : U
A registry entry with a power of π in its scale.
def table : List (String × U)
The §4.8.1 table, group by group, in the spec’s order.
def sym (s : String) : U
The table entry for a key (dimensionless 1 for a non-key; used only on keys).
theorem lookup_isSome_iff (s : String) : (lookup s).isSome ↔ s ∈ keys
The table is flat: a symbol resolves iff it is a key exactly as spelled.