Massless particles:
ProvedMassEnergyEquivalence.massless_energy_eq_pcLet , and let and be the energy and momentum magnitude of a particle satisfying the energy–momentum relation with rest mass . Then
For photons, which have zero rest mass, the energy–momentum relation thus reduces to : their energy is due only to their momentum.
Formalization Note A massless particle travels at speed , where the Lorentz factor is undefined, so it cannot be described by the velocity-based quantities , of the definition file (with those would both vanish). The statement is therefore phrased directly in terms of a pair satisfying the energy–momentum relation with .
import Mathlib import Definitions.Def_MassEnergyEquivalence_Defs open MassEnergyEquivalence Filter Asymptotics Topology
namespace MassEnergyEquivalence
theorem massless_energy_eq_pc (c E p : ℝ) (hc : 0 < c) (hE : 0 ≤ E) (hp : 0 ≤ p)
(h : E ^ 2 - (p * c) ^ 2 = ((0 : ℝ) * c ^ 2) ^ 2) :
E = p * c := by sorry
end MassEnergyEquivalenceRead-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.
For all real with , , , if
then . The statement involves no definitions from the mission's definition file; and are free real numbers subject only to the listed hypotheses.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.