Units on Mass

A unit of mass corresponds to a choice of translationally-invariant metric on the mass manifold (to be defined diffeomorphic to ℝ≥0). Such a choice is (non-canonically) equivalent to a choice of positive real number. We define the type MassUnit to be equivalent to the positive reals.

On MassUnit there is an instance of division giving a real number, corresponding to the ratio of the two scales of mass unit.

To define specific mass units, we first state the existence of a a given mass unit, and then construct all other mass units from it. We choose to state the existence of the mass unit of kilograms, and construct all other mass units from that.

structure MassUnit : Type

The choices of translationally-invariant metrics on the mass-manifold. Such a choice corresponds to a choice of units for mass.

• val : ℝ

  The underlying scale of the unit.

• property : 0 < self.val

@[simp]

theorem MassUnit.val_neq_zero (x : MassUnit) : x.val ≠ 0

theorem MassUnit.val_pos (x : MassUnit) : 0 < x.val

instance MassUnit.instInhabited : Inhabited MassUnit

Equations

• MassUnit.instInhabited = { default := { val := 1, property := MassUnit.instInhabited._proof_1 } }

Division of MassUnit

noncomputable instance MassUnit.instHDivNNReal : HDiv MassUnit MassUnit NNReal

Equations

• MassUnit.instHDivNNReal = { hDiv := fun (x t : MassUnit) => ⟨x.val / t.val, ⋯⟩ }

theorem MassUnit.div_eq_val (x y : MassUnit) : x / y = ⟨x.val / y.val, ⋯⟩

@[simp]

theorem MassUnit.div_neq_zero (x y : MassUnit) : ¬x / y = 0

@[simp]

theorem MassUnit.div_pos (x y : MassUnit) : 0 < x / y

@[simp]

theorem MassUnit.div_self (x : MassUnit) : x / x = 1

theorem MassUnit.div_symm (x y : MassUnit) : x / y = (y / x)⁻¹

@[simp]

theorem MassUnit.div_mul_div_coe (x y z : MassUnit) : ↑(x / y) * ↑(y / z) = ↑(x / z)

The scaling of a mass unit

def MassUnit.scale (r : ℝ) (x : MassUnit) (hr : 0 < r := by norm_num) : MassUnit

The scaling of a mass unit by a positive real.

Equations

• MassUnit.scale r x hr = { val := r * x.val, property := ⋯ }

@[simp]

theorem MassUnit.scale_div_self (x : MassUnit) (r : ℝ) (hr : 0 < r) : scale r x hr / x = ⟨r, ⋯⟩

@[simp]

theorem MassUnit.self_div_scale (x : MassUnit) (r : ℝ) (hr : 0 < r) : x / scale r x hr = ⟨1 / r, ⋯⟩

@[simp]

theorem MassUnit.scale_one (x : MassUnit) : scale 1 x ⋯ = x

@[simp]

theorem MassUnit.scale_div_scale (x1 x2 : MassUnit) {r1 r2 : ℝ} (hr1 : 0 < r1) (hr2 : 0 < r2) : scale r1 x1 hr1 / scale r2 x2 hr2 = ⟨r1, ⋯⟩ / ⟨r2, ⋯⟩ * (x1 / x2)

@[simp]

theorem MassUnit.scale_scale (x : MassUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) : scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x ⋯

Specific choices of mass units

To define a specific mass units. We first define the notion of a kilogram to correspond to the mass unit with underlying value equal to 1. This is really down to a choice in the isomorphism between the set of metrics on the mass manifold and the positive reals. From this choice of kilograms, we can define other length units by scaling kilograms.

def MassUnit.kilograms : MassUnit

The definition of a mass unit of kilograms.

Equations

• MassUnit.kilograms = { val := 1, property := MassUnit.instInhabited._proof_1 }

noncomputable def MassUnit.micrograms : MassUnit

The mass unit of a microgram (10^(-9) of a kilogram).

Equations

• MassUnit.micrograms = MassUnit.scale ((1 / 10) ^ 9) MassUnit.kilograms MassUnit.micrograms._proof_2

noncomputable def MassUnit.milligrams : MassUnit

The mass unit of milligram (10^(-6) of a kilogram).

Equations

• MassUnit.milligrams = MassUnit.scale ((1 / 10) ^ 6) MassUnit.kilograms MassUnit.milligrams._proof_1

noncomputable def MassUnit.grams : MassUnit

The mass unit of grams (10^(-3) of a kilogram).

Equations

• MassUnit.grams = MassUnit.scale ((1 / 10) ^ 3) MassUnit.kilograms MassUnit.grams._proof_1

noncomputable def MassUnit.ounces : MassUnit

The mass unit of (avoirdupois) ounces (0.028 349 523 125 of a kilogram).

Equations

• MassUnit.ounces = MassUnit.scale 28349523125e-12 MassUnit.kilograms MassUnit.ounces._proof_1

noncomputable def MassUnit.pounds : MassUnit

The mass unit of (avoirdupois) pounds (0.453 592 37 of a kilogram).

Equations

• MassUnit.pounds = MassUnit.scale 0.45359237 MassUnit.kilograms MassUnit.pounds._proof_1

noncomputable def MassUnit.stones : MassUnit

The mass unit of stones (14 pounds).

Equations

• MassUnit.stones = MassUnit.scale 14 MassUnit.pounds MassUnit.stones._proof_2

noncomputable def MassUnit.quarters : MassUnit

The mass unit of a quarter (28 pounds).

Equations

• MassUnit.quarters = MassUnit.scale 28 MassUnit.pounds MassUnit.quarters._proof_2

noncomputable def MassUnit.hundredweights : MassUnit

The mass unit of hundredweights (112 pounds).

Equations

• MassUnit.hundredweights = MassUnit.scale 112 MassUnit.pounds MassUnit.hundredweights._proof_2

noncomputable def MassUnit.shortTons : MassUnit

The mass unit of short tons (2000 pounds).

Equations

• MassUnit.shortTons = MassUnit.scale 2000 MassUnit.pounds MassUnit.shortTons._proof_2

noncomputable def MassUnit.metricTons : MassUnit

The mass unit of metric tons (1000 kilograms).

Equations

• MassUnit.metricTons = MassUnit.scale 1000 MassUnit.kilograms MassUnit.metricTons._proof_2

noncomputable def MassUnit.longTons : MassUnit

The mass unit of long tons (2240 pounds). Also called shortweight tons.

Equations

• MassUnit.longTons = MassUnit.scale 2240 MassUnit.pounds MassUnit.longTons._proof_2

noncomputable def MassUnit.nominalSolarMasses : MassUnit

The mass unit of nominal solar masses (1.988416 × 10 ^ 30 kilograms). See: https://iopscience.iop.org/article/10.3847/0004-6256/152/2/41

Equations

• MassUnit.nominalSolarMasses = MassUnit.scale 1988416e24 MassUnit.kilograms MassUnit.nominalSolarMasses._proof_1

Relations between mass units

theorem MassUnit.pounds_div_ounces : pounds / ounces = 16

theorem MassUnit.shortTons_div_kilograms : shortTons / kilograms = 907.18474

theorem MassUnit.longTons_div_kilograms : longTons / kilograms = 1016.0469088