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 axiomise the existence of a a given mass unit, and then construct all other mass units from it. We choose to axiomise the existence of the mass unit of kilograms, and construct all other mass units from that.
Equations
- MassUnit.instInhabited = { default := { val := 1, property := MassUnit.instInhabited._proof_1 } }
Division of MassUnit #
The scaling of a mass unit #
Specific choices of mass units #
To define a specific mass units, we must first axiomise the existence of a a given mass unit, and then construct all other mass units from it. We choose to axiomise the existence of the mass unit of kilograms.
We need an axiom since this relates something to something in the physical world.
The axiom corresponding to the definition of a mass unit of kilograms.
The mass unit of a microgram (10^(-9) of a kilogram).
Equations
Instances For
The mass unit of milligram (10^(-6) of a kilogram).
Equations
Instances For
The mass unit of grams (10^(-3) of a kilogram).
Equations
- MassUnit.grams = MassUnit.scale ((1 / 10) ^ 3) MassUnit.kilograms MassUnit.grams._proof_1
Instances For
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
Instances For
The mass unit of (avoirdupois) pounds (0.453 592 37 of a kilogram).
Equations
Instances For
The mass unit of stones (14 pounds).
Instances For
The mass unit of a quarter (28 pounds).
Instances For
The mass unit of hundredweights (112 pounds).
Equations
Instances For
The mass unit of short tons (2000 pounds).
Instances For
The mass unit of metric tons (1000 kilograms).
Instances For
The mass unit of long tons (2240 pounds). Also called shortweight tons.
Instances For
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