Units: dimensions and exact scales (esm-spec §4.8.1)
A dimension is a vector of rational exponents over exactly the eight axes
m kg s mol K A cd rad (§4.8.1 “The eight canonical dimension axes”).
A scale is exact. §4.8.1 recommends representing it as “a map from prime
factor (and the symbol π) to a rational exponent”; this module does exactly
that. A scale is written as a formal product ∏ bᵢ ^ eᵢ (a list of base/exponent
pairs, Scale
), and what it MEANS is its exponent map Scale.exp : Base → ℚ:
two scales are the same scale iff their exponent maps are equal. Multiplying
units appends the lists (adds exponent maps), a rational power multiplies every
exponent, so a composite unit’s scale stays exact (§4.8.1 “Scales are EXACT”).
Scale.real
is the real number a scale denotes. It is a homomorphism, depends
only on the exponent map, and is positive; these are the facts that make the
formal representation a faithful exact model of the spec’s real-valued scales.
inductive Axis
| m | kg | s | mol | K | A | cd | rad
deriving DecidableEq, Repr, Inhabited
The eight canonical dimension axes, and no others (§4.8.1).
theorem Axis.exactly_eight :
(∀ a : Axis, a ∈ Axis.all) ∧ Axis.all.length = 8 ∧ Axis.all.Nodup
Exactly eight axes, and no others.
abbrev Dim
A dimension: a rational exponent per axis. Unit multiplication is +, a
rational power q is q • ·.
inductive Base
| pi
| prime (p : Nat.Primes)
deriving DecidableEq
A base of the exact-scale representation: π or a prime.
abbrev Scale
An exact scale as a formal product ∏ b ^ e. Only its exponent map
(Scale.exp
) is meaningful; the list order and repetitions are not.
theorem Scale.exp_eq_zero_of_not_mem (s : Scale) (b : Base) (h : b ∉ s.map Prod.fst) :
Scale.exp s b = 0
A base outside a scale’s support has exponent 0.
theorem Scale.exp_eq_iff (s t : Scale) :
Scale.exp s = Scale.exp t ↔ ∀ b ∈ (s ++ t).map Prod.fst, Scale.exp s b = Scale.exp t b
Equality of exponent maps is decided on the finitely many bases that occur.
The real value of a scale
theorem Scale.real_eq_prod (s : Scale) (S : Finset Base) (hS : ∀ x ∈ s, x.1 ∈ S) :
Scale.real s = ∏ b ∈ S, b.real ^ ((Scale.exp s b : ℚ) : ℝ)
The real value as a product over any finite set of bases containing the support.
theorem Scale.real_congr (s t : Scale) (h : Scale.exp s = Scale.exp t) :
Scale.real s = Scale.real t
The real value depends only on the exponent map: the formal representation never distinguishes a scale from itself.
Units
structure U where
dim : Dim
scale : Scale
A resolved unit: a dimension and an exact scale.
def val (u : U) : Dim × (Base → ℚ)
What a unit means: its dimension and its scale’s exponent map.
def Agree (u v : U) : Prop
Two units agree iff they have the same dimension and the same exact scale (§4.8.3 “agreement”; decided exactly, §4.8.1).
def ofScale (s : Scale) : U
The unit that is the given exact positive rational, dimensionless.