Physlib

Physlib.Relativity.SpeedOfLight

The Speed of Light

i. Overview

In this module we define 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 arbitrary 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

B. Instances on the type

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.

D. Positivity properties

6 declarations

instance

Coercion from `SpeedOfLight` to R\mathbb{R}

This definition provides a coercion from the `SpeedOfLight` type to the real numbers R\mathbb{R}. It allows a value representing the speed of light to be automatically treated as its underlying numerical value in R\mathbb{R}.

instance

Speed of light c=1c = 1

This definition provides an instance of the speed of light with a numerical value of 11. It represents the unit speed of light in a system of units (such as natural units) where the speed of light in vacuum is normalized to c=1c = 1.

theorem

The numerical value of the unit speed of light is 11

The numerical value of the unit speed of light constant 11 in the `SpeedOfLight` type is equal to 11.

theorem

The speed of light is strictly positive (c>0c > 0)

Let cc be a speed of light in vacuum. Its representation as a real number is strictly positive, i.e., c>0c > 0.

theorem

The speed of light is non-negative (c≥0c \ge 0)

Let cc be a speed of light in a vacuum. Its representation as a real number is non-negative, i.e., c≥0c \ge 0.

theorem

The speed of light is non-zero (c≠0c \neq 0)

Let cc be a speed of light in a vacuum. Then, its representation as a real number is non-zero, i.e., c≠0c \neq 0.