Units on Length

A unit of length corresponds to a choice of translationally-invariant metric on the space manifold (to be defined). Such a choice is (non-canonically) equivalent to a choice of positive real number. We define the type LengthUnit to be equivalent to the positive reals.

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

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

structure LengthUnit : Type

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

• val : ℝ

  The underlying scale of the unit.

• property : 0 < self.val

@[simp]

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

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

instance LengthUnit.instInhabited : Inhabited LengthUnit

Equations

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

Division of LengthUnit

noncomputable instance LengthUnit.instHDivNNReal : HDiv LengthUnit LengthUnit NNReal

Equations

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

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

@[simp]

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

@[simp]

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

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

The scaling of a length unit

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

The scaling of a length unit by a positive real.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

Specific choices of Length units

To define a specific length units, we must first axiomise the existence of a a given length unit, and then construct all other length units from it. We choose to axiomise the existence of the length unit of meters.

We need an axiom since this relates something to something in the physical world.

axiom LengthUnit.meters : LengthUnit

The axiom corresponding to the definition of a length unit of meters.

noncomputable def LengthUnit.femtometers : LengthUnit

The length unit of femtometers (10⁻¹⁵ of a meter).

Equations

• LengthUnit.femtometers = LengthUnit.scale ((1 / 10) ^ 15) LengthUnit.meters LengthUnit.femtometers._proof_2

noncomputable def LengthUnit.picometers : LengthUnit

The length unit of picometers (10⁻¹² of a meter).

Equations

• LengthUnit.picometers = LengthUnit.scale ((1 / 10) ^ 12) LengthUnit.meters LengthUnit.picometers._proof_1

noncomputable def LengthUnit.nanometers : LengthUnit

The length unit of nanometers (10⁻⁹ of a meter).

Equations

• LengthUnit.nanometers = LengthUnit.scale ((1 / 10) ^ 9) LengthUnit.meters LengthUnit.nanometers._proof_1

noncomputable def LengthUnit.micrometers : LengthUnit

The length unit of micrometers (10⁻⁶ of a meter).

Equations

• LengthUnit.micrometers = LengthUnit.scale ((1 / 10) ^ 6) LengthUnit.meters LengthUnit.micrometers._proof_1

noncomputable def LengthUnit.millimeters : LengthUnit

The length unit of millimeters (10⁻³ of a meter).

Equations

• LengthUnit.millimeters = LengthUnit.scale ((1 / 10) ^ 3) LengthUnit.meters LengthUnit.millimeters._proof_1

noncomputable def LengthUnit.centimeters : LengthUnit

The length unit of centimeters (10⁻² of a meter).

Equations

• LengthUnit.centimeters = LengthUnit.scale ((1 / 10) ^ 2) LengthUnit.meters LengthUnit.centimeters._proof_1

noncomputable def LengthUnit.inches : LengthUnit

The length unit of inch (0.0254 meters).

Equations

• LengthUnit.inches = LengthUnit.scale 254e-4 LengthUnit.meters LengthUnit.inches._proof_1

noncomputable def LengthUnit.links : LengthUnit

The length unit of link (0.201168 meters).

Equations

• LengthUnit.links = LengthUnit.scale 0.201168 LengthUnit.meters LengthUnit.links._proof_1

noncomputable def LengthUnit.feet : LengthUnit

The length unit of feet (0.3048 meters)

Equations

• LengthUnit.feet = LengthUnit.scale 0.3048 LengthUnit.meters LengthUnit.feet._proof_1

noncomputable def LengthUnit.yards : LengthUnit

The length unit of a yard (0.9144 meters)

Equations

• LengthUnit.yards = LengthUnit.scale 0.9144 LengthUnit.meters LengthUnit.yards._proof_1

noncomputable def LengthUnit.rods : LengthUnit

The length unit of a rod (5.0292 meters)

Equations

• LengthUnit.rods = LengthUnit.scale 5.0292 LengthUnit.meters LengthUnit.rods._proof_1

noncomputable def LengthUnit.chains : LengthUnit

The length unit of a chain (20.1168 meters)

Equations

• LengthUnit.chains = LengthUnit.scale 20.1168 LengthUnit.meters LengthUnit.chains._proof_1

noncomputable def LengthUnit.furlongs : LengthUnit

The length unit of a furlong (201.168 meters)

Equations

• LengthUnit.furlongs = LengthUnit.scale 201.168 LengthUnit.meters LengthUnit.furlongs._proof_1

noncomputable def LengthUnit.kilometers : LengthUnit

The length unit of kilometers (10³ meters).

Equations

• LengthUnit.kilometers = LengthUnit.scale (10 ^ 3) LengthUnit.meters LengthUnit.kilometers._proof_1

noncomputable def LengthUnit.miles : LengthUnit

The length unit of a mile (1609.344 meters).

Equations

• LengthUnit.miles = LengthUnit.scale 1609.344 LengthUnit.meters LengthUnit.miles._proof_1

noncomputable def LengthUnit.nauticalMiles : LengthUnit

The length unit of a nautical mile (1852 meters).

Equations

• LengthUnit.nauticalMiles = LengthUnit.scale 1852 LengthUnit.meters LengthUnit.nauticalMiles._proof_2

noncomputable def LengthUnit.astronomicalUnits : LengthUnit

The length unit of an astronomical unit (149,597,870,700 meters).

Equations

• LengthUnit.astronomicalUnits = LengthUnit.scale 149597870700 LengthUnit.meters LengthUnit.astronomicalUnits._proof_2

noncomputable def LengthUnit.lightYears : LengthUnit

The length unit of a light year (9,460,730,472,580,800 meters).

Equations

• LengthUnit.lightYears = LengthUnit.scale 9460730472580800 LengthUnit.meters LengthUnit.lightYears._proof_2

noncomputable def LengthUnit.parsecs : LengthUnit

The length unit of a parsec (648,000/π astronomicalUnits).

Equations

• LengthUnit.parsecs = LengthUnit.scale (648000 / Real.pi) LengthUnit.astronomicalUnits LengthUnit.parsecs._proof_2

Relations between length units

theorem LengthUnit.miles_div_yards : miles / yards = ⟨1760, ⋯⟩

There are exactly 1760 yards in a mile.

theorem LengthUnit.furlongs_div_yards : furlongs / yards = ⟨220, ⋯⟩

There are exactly 220 yards in a furlong.