proper_time_sq_eq_neg_interval
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not determine the sign of interval v for any displacement class.
- Does not derive the explicit components of the metric tensor.
- Does not address curved or higher-dimensional spacetimes.
- Does not incorporate mass terms or field dynamics.
Lean usage
rw [proper_time_sq_eq_neg_interval]; linarithformal statement (Lean)
254theorem proper_time_sq_eq_neg_interval (v : Displacement) :
255 proper_time_sq v = -interval v := by
proof body
Term-mode proof.
256 simp [proper_time_sq, interval_eq_spatial_minus_temporal]
257
258/-- Proper time squared is positive for timelike displacements. -/