Prove2Me

Parker Solar Probe: 3v24c2≈3.9×10−8\tfrac{3v^2}{4c^2} \approx 3.9\times10^{-8}

Proved
MassEnergyEquivalence.parker_probe_correction

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

mathematical-physicsspecial-relativity

For the Parker Solar Probe's 2018 speed v=68 600 m/sv = 68\,600\ \mathrm{m/s} and c=299 792 458 m/sc = 299\,792\,458\ \mathrm{m/s}, the relative difference between the second- and third-order low-speed approximations of the energy satisfies

∣3v24c2−3.9×10−8∣<5×10−10,\left|\frac{3v^2}{4c^2} - 3.9\times10^{-8}\right| < 5\times10^{-10},

i.e. 3v24c2≈3.9×10−8\frac{3v^2}{4c^2}\approx 3.9\times10^{-8} to the two significant digits quoted in the article — an energy correction of about four parts per hundred million.

Preamble
import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology
Formal statement
namespace MassEnergyEquivalence

theorem parker_probe_correction :
    |3 * (68600 : ℝ) ^ 2 / (4 * (299792458 : ℝ) ^ 2) - 3.9e-8| < 0.05e-8 := 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.), §Low-speed approximation (p. 6): "The difference between the approximations for the Parker Solar Probe in 2018 is 3v24c2≈3.9×10−8\tfrac{3v^2}{4c^2} \approx 3.9\times10^{-8}" with v=68,600v = 68{,}600 m/s; c=299 792 458c = 299\,792\,458 m/s from §Practical examples (p. 8).
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 about real numbers, with no variables or hypotheses:

∣3⋅6860024⋅2997924582−3.9×10−8∣<0.05×10−8.\left|\frac{3\cdot 68600^2}{4\cdot 299792458^2} - 3.9\times10^{-8}\right| < 0.05\times 10^{-8}.
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