proper_time_from_velocity
This result equates the squared proper time interval for a four-vector displacement to the squared temporal component times one minus velocity squared. Researchers deriving Lorentzian geometry from J-cost minimization would cite it when connecting velocity to causal intervals. The proof is a short algebraic manipulation that clears the division in velocity squared via field simplification and concludes with linear arithmetic.
claimFor a spacetime displacement four-vector $v = (Δt, Δx_1, Δx_2, Δx_3)$ with $Δt ≠ 0$, the squared proper time satisfies $τ² = (Δt)²(1 − v²)$, where $v² = |Δx|² / (Δt)²$.
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 without assuming background spacetime. Displacement is the four-vector map from Fin 4 to reals. Proper time squared is defined as the temporal square minus the spatial norm squared; velocity squared is the ratio of those quantities when the temporal component is nonzero.
proof idea
The proof first records that the temporal square is nonzero from the hypothesis that the time component is nonzero. It then rewrites the target identity as an equality between the temporal square times (1 minus spatial over temporal) and the difference of temporal and spatial squares. Field simplification clears the division, after which rewriting the definitions of proper time squared and velocity squared plus linear arithmetic yields the result.
why it matters in Recognition Science
The theorem supplies the velocity-to-interval relation used by the immediate downstream result that positive proper time squared holds exactly when velocity is subluminal. It completes one link in the chain from the Recognition Composition Law through J-uniqueness, the eight-tick octave, and D = 3 to the emergence of the Lorentz factor and causal structure. The parent equivalence theorem applies it directly to obtain the timelike–subluminal biconditional.
scope and limits
- Does not derive the full Lorentz transformations.
- Does not treat curved spacetime or gravity.
- Does not incorporate quantum corrections or mass-gap dynamics.
- Does not fix numerical values for constants such as α or G.
formal statement (Lean)
268theorem proper_time_from_velocity (v : Displacement)
269 (ht : v ⟨0, by omega⟩ ≠ 0) :
270 proper_time_sq v = temporal_sq v * (1 - velocity_sq v ht) := by
proof body
Tactic-mode proof.
271 have h_ne : temporal_sq v ≠ 0 := by unfold temporal_sq; exact pow_ne_zero 2 ht
272 suffices temporal_sq v * (1 - spatial_norm_sq v / temporal_sq v) =
273 temporal_sq v - spatial_norm_sq v by
274 simp only [proper_time_sq, velocity_sq]; linarith
275 field_simp [h_ne]
276
277/-- **Subluminal velocity for timelike**: τ² > 0 iff v² < 1. -/