Decimal prefixes and the exact non-SI conversions
DisprovedSI.prefixes_and_exact_non_siDecimal prefixes compose by adding exponents, and exact powers of ten never vanish. The kilogram, which carries a prefix in its name, receives its decimal multiples and submultiples on the gram: prefixed 3 gram = kilogram. The non-SI units exactly accepted for use with the SI (Table 8) whose defining factors are exact numerical factors have the recorded conversions: the tonne is the megagram, the bar is prefixed 5 pascal, the hour is 60 minutes, the day is 24 hours, the litre is the cubic decimetre, the astronomical unit is 149 597 870 700 m, the nautical mile is 1852 m, and the knot is (1852/3600) m s⁻¹.
import Mathlib import Definitions.Def_SI_dim import Definitions.Def_SI_units import Definitions.Def_SI_qmodel
/-!
# Decimal prefixes and the exact non-SI conversions
Chapter 3 of the SI Brochure fixes the decimal prefixes and the rule
that compound prefixes are not permitted; Table 8 lists the non-SI
units exactly accepted for use with the SI. Those with definitions
given by an exact numerical factor are: the minute, hour and day of
time; the litre; the tonne; the bar; the astronomical unit; the
nautical mile and the knot; and the electronvolt (its exactness is
the subject of a separate milestone). The prefixes compose according
to the addition of exponents, and the kilogram, which carries a
prefix in its name, receives its further prefixes on the gram. This
milestone is proved on the way to the goal theorem `SI.si_complete`.
-/
namespace SI
/-- Decimal prefixes compose by adding exponents, exact powers of ten
never vanish, the kilogram is the kilo-gram, and the exact non-SI
units of Table 8 have the recorded exact conversions: the tonne is
the megagram, the bar is 10⁵ Pa, the hour is 60 minutes, the day is
24 hours, the litre is the cubic decimetre, the astronomical unit is
149 597 870 700 m, the nautical mile is 1852 m, and the knot is
(1852/3600) m s⁻¹. -/
theorem prefixes_and_exact_non_si :
(∀ k l : ℤ, ∀ u : SIUnit, prefixed k (prefixed l u) = prefixed (k + l) u) ∧
(∀ k : ℤ, pow10 k ≠ 0) ∧
prefixed 3 gram = kilogram ∧
tonne = prefixed 6 gram ∧
bar = prefixed 5 pascal ∧
hour = uscale 60 minute ∧
day = uscale 24 hour ∧
litre = umul (prefixed (-1) metre)
(umul (prefixed (-1) metre) (prefixed (-1) metre)) ∧
au = uscale 149597870700 metre ∧
nauticalMile = uscale 1852 metre ∧
knot = uscale (1852 / 3600) (udiv metre second) := by
sorry
end SI
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The formal statement records: the composition law of decimal prefixes (two successive prefixes equal the single prefix with the summed exponent, which is why the brochure can exclude compound prefixes); the nonvanishing of every exact power of ten; the identity kilogram = kilo times gram; and the eight exact conversions of Table 8 listed with exact numerical factors: tonne = mega-gram, bar = 10⁵ Pa, hour = 60 min, day = 24 h, litre = (dm)³, au = 149 597 870 700 m, nautical mile = 1852 m, and knot = (1852/3600) m/s. Deliberately absent, as disclosed: the angle units with π factors (degree and its subdivisions), the dalton (its value carries an experimental uncertainty), the logarithmic units (neper, bel, decibel), the remaining decimal multiples of Table 8 (are, hectare, barn, ångström, gal, var), and the electronvolt, which has its own milestone. All arithmetic is over the rationals.