proper_time_sq_eq_neg_interval
plain-language theorem explainer
The theorem equates proper time squared for any four-vector displacement to the negative of its spacetime interval. Researchers deriving the Lorentzian metric from J-cost minimization cite this identity to fix the temporal sign. The proof is a one-line simplification that unfolds the proper time definition together with the spatial-minus-temporal interval relation.
Claim. For any displacement $v : Fin 4 → ℝ$, proper time squared satisfies $τ²(v) = −Δs²(v)$, where $Δs²$ denotes the spacetime interval.
background
The SpacetimeEmergence module derives 4D Lorentzian geometry from the J-cost functional via the T0–T8 forcing chain. Displacement is the type of 4-vectors (Fin 4 → ℝ). The interval function is the quadratic form with signature (−,+,+,+), and the lemma interval_eq_spatial_minus_temporal encodes its decomposition into spatial and temporal quadratic parts. This local setting follows the module statement that spacetime structure, including the metric signature, is forced by cost minimization rather than postulated as background.
proof idea
The proof is a one-line wrapper that applies simp to unfold the definition of proper_time_sq and substitutes the equality from interval_eq_spatial_minus_temporal.
why it matters
This identity is invoked directly by proper_time_sq_pos_of_timelike to establish positivity of proper time for timelike displacements. It fills a step in the derivation of the Lorentzian signature (−,+,+,+) forced by J''(1)=1 on spatial axes together with the 8-tick octave (T7) for the temporal direction and D=3 (T8). The result confirms that proper time is the positive quantity along causal paths in the emergent geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.