The Speed of Light

i. Overview

In this module we deine a type for the speed of light in a vacuum, along with some basic properties. An element of this type is a positive real number, and should be thought of as the speed of light in some chosen but arbitary system of units.

ii. Key results

• SpeedOfLight : The type of speeds of light in a vacuum.

iii. Table of contents

• A. The Speed of Light type
• B. Instances on the type
• C. The instance of one
• D. Positivity properties

iv. References

A. The Speed of Light type

structure SpeedOfLight : Type

The speed of light in a vacuum. An element of this type should be thought of as the speed of light in some chosen but arbitary system of units.

• val : ℝ

  The underlying value of the speed of light.

• pos : 0 < self.val

B. Instances on the type

instance SpeedOfLight.instCoeReal : Coe SpeedOfLight ℝ

Equations

• SpeedOfLight.instCoeReal = { coe := SpeedOfLight.val }

C. The instance of one

We define the instance of one for SpeedOfLight to be the speed of light equal to 1. This is useful when we are working in units where the speed of light is equal to one.

instance SpeedOfLight.instOne : One SpeedOfLight

Equations

• SpeedOfLight.instOne = { one := { val := 1, pos := SpeedOfLight.instOne._proof_1 } }

@[simp]

theorem SpeedOfLight.val_one : val 1 = 1

D. Positivity properties

@[simp]

theorem SpeedOfLight.val_pos (c : SpeedOfLight) : 0 < c.val

@[simp]

theorem SpeedOfLight.val_nonneg (c : SpeedOfLight) : 0 ≤ c.val

@[simp]

theorem SpeedOfLight.val_ne_zero (c : SpeedOfLight) : c.val ≠ 0