proper_time_sq
plain-language theorem explainer
The definition sets proper time squared equal to the difference between the squared temporal component and the squared spatial norm of a four-dimensional displacement vector. Researchers deriving emergent Lorentzian geometry from cost minimization cite this when relating proper time to the interval. It is introduced as a direct algebraic combination of the already-defined temporal and spatial quadratic forms.
Claim. For a spacetime displacement $v = (t, x_1, x_2, x_3)$, the squared proper time is defined by $τ^2(v) = t^2 - |x|^2$.
background
Spacetime displacements are four-vectors with one temporal entry and three spatial entries. The temporal square isolates the squared time component while the spatial norm square sums the three squared spatial components. The interval is formed with the Minkowski metric of signature (−,+,+,+), so that interval equals spatial norm squared minus temporal square.
proof idea
Direct definition that subtracts the spatial norm squared from the temporal square of the input displacement.
why it matters
This supplies the explicit expression for proper time squared used to prove equality with the negative interval and positivity on timelike vectors. It feeds the theorems establishing the Lorentz factor and light-cone structure. It realizes the translation from the forced metric diag(−1,+1,+1,+1) (arising from J''(1)=1 spatially and the eight-tick cost reduction temporally) into the standard proper-time formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.