Energy equivalent of one kilogram: $c^2 = 89\,875\,517\,873\,681\,764$ J/kg

Proved

MassEnergyEquivalence.rest_energy_one_kilogram

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsspecial-relativity

In SI units, with $c = 299\,792\,458\ \mathrm{m/s}$ , the rest energy of a mass of one kilogram is

E = (1\ \mathrm{kg})\,c^2 = 89\,875\,517\,873\,681\,764\ \mathrm J \;(\approx 9.0\times10^{16}\ \mathrm J \approx 89.9\ \mathrm{PJ}).

Preamble

import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology

Formal statement

namespace MassEnergyEquivalence

theorem rest_energy_one_kilogram :
    restEnergy 299792458 1 = 89875517873681764 := by sorry

end MassEnergyEquivalence

Source

Wikipedia, *Mass–energy equivalence*, https://en.wikipedia.org/wiki/Mass%E2%80%93energy_equivalence (PDF snapshot supplied by the proposer, 25 pp.), §Practical examples (pp. 7–8): "

E/m = c^2 = (299\,792\,458

m/s

)^2 = 89\,875\,517\,873\,681\,764

J/kg"; "the energy equivalent of one kilogram of mass is 89.9 petajoules".

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — this is NOT a blind read-back. It was written by the same agent (Aristotle, by Harmonic) that drafted this Lean statement, with full knowledge of the source material and of the intended meaning. It is not independent testimony and must not be mistaken for an independent audit; it was produced and uploaded at the proposer's explicit request. An independent, blind read-back is still recommended before the proposal is submitted.

A closed numerical claim: the defined rest energy $E_0(c,m)=m c^2$ evaluated at $c = 299792458$ and $m = 1$ equals the real number $89875517873681764$ . No variables, no hypotheses, no units are represented.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Energy equivalent of one kilogram: c2=89 875 517 873 681 764c^2 = 89\,875\,517\,873\,681\,764c2=89875517873681764 J/kg

Energy equivalent of one kilogram: $c^2 = 89\,875\,517\,873\,681\,764$ J/kg