proper_time_sq_pos_of_timelike
plain-language theorem explainer
Timelike displacements where the spacetime interval is negative have strictly positive proper time squared. Researchers deriving Lorentzian geometry from J-cost minimization cite this to confirm the timelike causal cone in the emergent 4D spacetime. The proof is a one-line wrapper that rewrites proper time squared as the negation of the interval and applies linear arithmetic.
Claim. Let $v$ be a 4-vector displacement. If the spacetime interval $ds^2 < 0$, then the proper time squared satisfies $0 < -ds^2$.
background
In the SpacetimeEmergence module a Displacement is the 4-vector $v : Fin 4 → ℝ$ representing ($Δt$, $Δx_1$, $Δx_2$, $Δx_3$). The interval is the quadratic form $∑ η_{ii} v_i^2$ with the metric $η$ of signature (−,+,+,+). Proper time squared is defined as the difference between the squared temporal component and the squared spatial norm, which equals the negative of the interval by the upstream theorem proper_time_sq_eq_neg_interval.
proof idea
The proof is a one-line wrapper. It rewrites proper_time_sq v by the equality proper_time_sq v = −interval v, then invokes linarith on the hypothesis interval v < 0 to obtain the strict inequality.
why it matters
This lemma verifies that timelike vectors carry positive proper time in the Lorentzian structure forced by the J-cost functional and the T0–T8 chain. It directly supports the central claim of the module that the metric η = diag(−1,+1,+1,+1) emerges from RCL, J-uniqueness, the 8-tick octave, and D = 3 spatial dimensions, thereby grounding the light cone and causal ordering without background postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.