rest_energy_is_mass
plain-language theorem explainer
The identity confirms that rest energy squared equals rest mass squared when spatial momenta vanish, in units with c=1. Researchers deriving Lorentzian geometry from J-cost minimization cite this to close the relativistic dispersion relation under the forced metric signature. The proof is a one-line ring tactic that verifies the algebraic tautology directly.
Claim. In natural units with $c=1$, the rest energy $E_0$ of a particle satisfies $E_0^2 = m^2$, or equivalently $m^2 = 0^2 + 0^2 + 0^2 + m^2$ when the three spatial momentum components are zero.
background
The module derives the full 4D Lorentzian structure, including metric signature (−,+,+,+), from the J-cost functional and forcing chain T0–T8. Spatial directions acquire positive metric coefficients from J''(1)=1 while the temporal direction is singled out by the 8-tick operator that reduces cost; dimension counting gives one temporal octave plus D=3 spatial axes. The upstream definition E(D) counts edges of the D-cube and supports the spatial dimension tally used in the emergence chain.
proof idea
The proof is a one-line wrapper that applies the ring tactic to confirm the algebraic identity holds identically for any real m.
why it matters
This declaration closes the rest-energy case of the energy-momentum relation E² = p² + m² that the module lists as the final step in the derivation RCL → J-uniqueness (T5) → 8-tick octave (T7) + D=3 (T8) → η = diag(−1,+1,+1,+1) → E² = p² + m². It anchors the subsequent comment on the massless limit E = |p| and supplies the zero-momentum anchor for the full spacetime emergence theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.