proper_time_sq
The definition computes proper time squared for a four-vector displacement as the temporal component squared minus the spatial norm squared. Physicists deriving Lorentzian geometry from J-cost minimization cite this when establishing causal structure and the light cone. It is a direct abbreviation that subtracts the two component functions already defined in the module.
claimFor a spacetime displacement vector $v = (v_0, v_1, v_2, v_3)$, proper time squared is defined by $τ²(v) := v_0² - (v_1² + v_2² + v_3²)$.
background
The Spacetime Emergence module derives 4D Lorentzian geometry from the J-cost functional and the T0–T8 forcing chain. Displacement is the type Fin 4 → ℝ, a 4-vector whose components are interpreted as (Δt, Δx₁, Δx₂, Δx₃). The interval is defined as the sum η_{ii} v_i² with signature (−,+,+,+), spatial_norm_sq extracts the sum of the last three squared components, and temporal_sq extracts the zeroth squared component. These follow from the Recognition Composition Law, J-uniqueness at T5, the eight-tick octave at T7, and D = 3 at T8.
proof idea
The definition is a direct abbreviation that subtracts spatial_norm_sq v from temporal_sq v.
why it matters in Recognition Science
This supplies the proper-time expression used by proper_time_sq_eq_neg_interval (which equates it to the negative interval) and proper_time_from_velocity (which factors out the Lorentz factor). It fills the concrete step from the module's central theorem to the emergence of proper time, the light cone, and the arrow of time. The parent chain is RCL → J''(1) = 1 → eight-tick temporal direction → Lorentzian signature η = diag(−1, +1, +1, +1).
scope and limits
- Does not derive the Lorentzian signature or the interval definition.
- Does not prove positivity of proper time for timelike vectors.
- Does not relate proper time to velocity or the Lorentz factor.
- Does not connect directly to the J-cost functional or the forcing chain T0–T8.
formal statement (Lean)
251def proper_time_sq (v : Displacement) : ℝ := temporal_sq v - spatial_norm_sq v
proof body
Definition body.
252
253/-- Proper time squared = −interval. -/