energy_momentum_relation
plain-language theorem explainer
The energy-momentum relation follows as an algebraic identity once the Lorentzian metric is fixed by the J-cost forcing chain. Researchers working on emergent spacetime from recognition principles cite it to recover the standard relativistic dispersion in units with c = 1. The proof is a one-line linear arithmetic reduction of the supplied hypothesis.
Claim. Given $E^2 = p_1^2 + p_2^2 + p_3^2 + m^2$, it follows that $E^2 - (p_1^2 + p_2^2 + p_3^2) = m^2$ in units where $c = 1$.
background
The Spacetime Emergence module derives the full 4D Lorentzian structure from the J-cost functional and the T0–T8 forcing chain. Spatial directions receive positive metric signature from J''(1) = 1 while the temporal direction receives the negative sign from the 8-tick recognition operator, producing η = diag(−1, +1, +1, +1) and the light-cone structure. The upstream definition E counts edges of the D-cube and supports the spatial dimension count D = 3.
proof idea
The proof is a one-line wrapper that applies the linarith tactic to rearrange the hypothesis by subtracting the three momentum squares from both sides.
why it matters
This declaration closes the derivation from RCL through J-uniqueness, the eight-tick octave, and D = 3 to the relativistic energy-momentum relation. It sits at the end of the spacetime emergence chain and confirms that the forced metric yields E² = p² + m² with no free parameters. The module doc-comment states that every step is forced and zero parameters remain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.