Algebra of units (esm-spec §4.8.1 "Scales are EXACT")

Lean module Esm.Units.Laws, formal/Esm/Units/Laws.lean at 184aa13d35e5
Imports Esm.Units.Registry

Units under multiplication form an abelian group up to agreement (equal dimension and equal exact scale), rational powers obey the exponent laws, and the real value of a scale is a positive homomorphism that agreement respects.

theorem abelian_group proved source

theorem abelian_group :
    (∀ u v w : U, ((u.mul v).mul w).Agree (u.mul (v.mul w))) ∧
    (∀ u v : U, (u.mul v).Agree (v.mul u)) ∧
    (∀ u : U, (one.mul u).Agree u) ∧
    (∀ u : U, (u.mul u.inv).Agree one) ∧
    (∀ u u' v v' : U, u.Agree u' → v.Agree v' → (u.mul v).Agree (u'.mul v'))

Units form an abelian group under multiplication, up to agreement; and agreement is a congruence for multiplication and rational powers.

theorem rpow_laws proved source

theorem rpow_laws :
    (∀ (u : U) (a b : ℚ), ((u.rpow a).rpow b).Agree (u.rpow (b * a))) ∧
    (∀ (u : U) (a b : ℚ), (u.rpow (a + b)).Agree ((u.rpow a).mul (u.rpow b))) ∧
    (∀ (u v : U) (q : ℚ), ((u.mul v).rpow q).Agree ((u.rpow q).mul (v.rpow q))) ∧
    (∀ u : U, (u.rpow 1).Agree u) ∧
    (∀ u : U, (u.rpow 0).Agree one) ∧
    (∀ (u u' : U) (q : ℚ), u.Agree u' → (u.rpow q).Agree (u'.rpow q))

Rational powers: the exponent laws hold exactly.

theorem real_hom proved source

theorem real_hom :
    (∀ s : Scale, 0 < Scale.real s) ∧
    (∀ s t : Scale, Scale.real (s ++ t) = Scale.real s * Scale.real t) ∧
    (∀ (s : Scale) (q : ℚ), Scale.real (Scale.rpow s q) = Scale.real s ^ (q : ℝ)) ∧
    (∀ u v : U, u.Agree v → Scale.real u.scale = Scale.real v.scale)

The real value of a scale: positive, multiplicative, carries rational powers to real powers, and agrees on agreeing units — so the exact representation never separates two scales with the same exponent map, and composing scales is exact.

This module also proves 4 lemmas without doc comments; they are in the source.