proper_time_from_velocity
plain-language theorem explainer
Proper time squared for a 4-displacement equals its temporal component squared multiplied by one minus the squared velocity. Researchers extracting the Lorentz factor from J-cost minimization cite this relation. The tactic proof first records that the temporal square is nonzero, then uses field simplification on the velocity ratio followed by linear arithmetic to recover the proper time definition.
Claim. For a displacement $v = (\Delta t, \Delta x_1, \Delta x_2, \Delta x_3)$ with $\Delta t \neq 0$, let $\tau^2 := (\Delta t)^2 - |\Delta \mathbf{x}|^2$ and $v^2 := |\Delta \mathbf{x}|^2 / (\Delta t)^2$. Then $\tau^2 = (\Delta t)^2 (1 - v^2)$.
background
The Spacetime Emergence module derives the full Lorentzian structure (signature (−,+,+,+), light cone, proper time) from the J-cost functional and the T0–T8 forcing chain. The Recognition Composition Law plus J-uniqueness (T5) forces positive spatial curvature and the eight-tick temporal direction (T7), while T8 supplies D = 3 spatial dimensions and c = 1.
Displacement is the type of 4-vectors (Fin 4 → ℝ). The auxiliary definitions are proper_time_sq v := temporal_sq v − spatial_norm_sq v, temporal_sq v := v(0)^2, spatial_norm_sq v the sum of the three spatial squares, and velocity_sq v ht := spatial_norm_sq v / temporal_sq v when the time component is nonzero.
This identity supplies the algebraic bridge between the interval and the velocity parameter inside the emergent flat spacetime.
proof idea
The proof first obtains temporal_sq v ≠ 0 from the hypothesis that the time component is nonzero. It then proves the auxiliary equality temporal_sq v ⋅ (1 − spatial_norm_sq v / temporal_sq v) = temporal_sq v − spatial_norm_sq v by field_simp on the nonzero denominator. Linear arithmetic identifies the left-hand side with proper_time_sq after substituting the definition of velocity_sq.
why it matters
The result feeds directly into the downstream theorem timelike_iff_subluminal_velocity, which states that τ² > 0 if and only if v² < 1. It forms one link in the chain from the Recognition Composition Law through J-uniqueness (T5), the phi fixed point (T6), the eight-tick octave (T7), and D = 3 (T8) to the emergence of the light cone, Lorentz factor, and E² = p² + m². The module shows that the entire causal structure is forced by cost minimization with zero free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.