timelike_iff_subluminal_velocity
The equivalence between positive proper time squared and subluminal velocity squared holds for any spacetime displacement with nonzero temporal component. Researchers deriving Lorentzian geometry from J-cost minimization would cite this to confirm the interior of the light cone. The proof rewrites proper time via the velocity relation, establishes temporal positivity, and splits the biconditional with linear arithmetic.
claimFor a spacetime displacement $v$ with nonzero time component, $0 <$ proper time squared$(v) $ iff velocity squared$(v) < 1$.
background
The Spacetime Emergence module derives the full 4D Lorentzian structure (signature (−,+,+,+), light cone, proper time) as a theorem of J-cost minimization along the T0–T8 forcing chain. Displacement is the 4-vector type Fin 4 → ℝ. Proper time and velocity are defined relative to the emergent metric whose temporal coefficient is negative because the 8-tick recognition operator reduces cost along that axis. The lemma depends on the algebraic identity proper_time_from_velocity together with positivity facts for squares.
proof idea
The tactic proof first rewrites proper_time_sq using proper_time_from_velocity. It then obtains positivity of the temporal square by unfolding and applying sq_pos_of_ne_zero. Constructor splits the biconditional: the forward direction assumes velocity squared ≥ 1, derives a non-positive difference via linarith, and reaches contradiction with nlinarith; the reverse direction multiplies the two positive quantities and concludes with linarith.
why it matters in Recognition Science
This lemma verifies that timelike intervals lie strictly inside the light cone once the J-cost functional and the eight-tick octave (T7) plus D = 3 (T8) have fixed the metric signature. It immediately precedes the energy-momentum section in the same file and supports the claim that E² = p² + m² follows from cost minimization without background postulates. No downstream uses are recorded yet.
scope and limits
- Does not derive the explicit components of the metric tensor.
- Does not treat spacelike or null displacements.
- Does not connect to the phi-ladder mass formula.
- Does not remove the nonzero-time hypothesis.
formal statement (Lean)
278theorem timelike_iff_subluminal_velocity (v : Displacement)
279 (ht : v ⟨0, by omega⟩ ≠ 0) :
280 0 < proper_time_sq v ↔ velocity_sq v ht < 1 := by
proof body
Tactic-mode proof.
281 rw [proper_time_from_velocity v ht]
282 have h_t_pos : 0 < temporal_sq v := by
283 unfold temporal_sq; exact sq_pos_of_ne_zero ht
284 constructor
285 · intro h
286 by_contra hle; push_neg at hle
287 have : 1 - velocity_sq v ht ≤ 0 := by linarith
288 nlinarith
289 · intro hv; exact mul_pos h_t_pos (by linarith)
290
291/-! ## §8 Energy-Momentum Relation from J-Cost -/
292
293/-- The energy-momentum relation (algebraic identity from the metric). -/