The units of charge

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

We assume that the charge manifold is already defined with an orientation, with the electron being in the negative direction.

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

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

structure ChargeUnit : Type

The choices of translationally-invariant metrics on the charge-manifold. Such a choice corresponds to a choice of units for charge. This assumes that an orientation has already being picked on the charge manifold.

• val : ℝ

  The underlying scale of the unit.

• property : 0 < self.val

@[simp]

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

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

instance ChargeUnit.instInhabited : Inhabited ChargeUnit

Equations

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

Division of ChargeUnit

noncomputable instance ChargeUnit.instHDivNNReal : HDiv ChargeUnit ChargeUnit NNReal

Equations

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

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

@[simp]

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

@[simp]

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

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

The scaling of a charge unit

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

The scaling of a charge unit by a positive real.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Specific choices of charge units

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

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

axiom ChargeUnit.coulombs : ChargeUnit

The axiom corresponding to the definition of a charge unit of coulomb.

noncomputable def ChargeUnit.elementaryCharge : ChargeUnit

The charge unit of a elementryCharge (1.602176634×10−19 coulomb).

Equations

• ChargeUnit.elementaryCharge = ChargeUnit.scale 1602176634e-28 ChargeUnit.coulombs ChargeUnit.elementaryCharge._proof_1