velocity_sq
plain-language theorem explainer
This definition supplies the squared velocity parameter for any spacetime displacement vector as the ratio of its spatial norm squared to its temporal component squared, provided the time component is nonzero. Researchers deriving Lorentzian geometry from J-cost minimization along the T0-T8 chain would cite it when computing proper time intervals or classifying causal character. It is realized as the direct algebraic quotient of the two component-norm functions.
Claim. For a displacement vector $v = (Δt, Δx_1, Δx_2, Δx_3)$ with $Δt ≠ 0$, the squared velocity parameter is $v^2 = |Δx|^2 / (Δt)^2$.
background
The Spacetime Emergence module derives the full 4D Lorentzian structure (signature (−,+,+,+), light cone, proper time) as a theorem of J-cost minimization. A Displacement is the 4-vector (Δt, Δx₁, Δx₂, Δx₃). The spatial norm squared sums the squares of the three spatial components; the temporal component squared isolates the time part. Upstream, the PrimitiveDistinction theorem supplies the seven axioms that reduce to four structural conditions plus definitional facts, while the module itself records the chain RCL → J-uniqueness (T5) → J''(1)=1 (spatial curvature) + φ (T6) → 8-tick octave (T7) + D=3 (T8) → c=1.
proof idea
The definition is a one-line wrapper that divides spatial_norm_sq by temporal_sq.
why it matters
It is invoked directly by proper_time_from_velocity, which states dτ² = (Δt)²(1 − v²), and by timelike_iff_subluminal_velocity, which equates positive proper time with v² < 1. These results close the derivation of the causal light cone and arrow of time from the J-cost functional together with the eight-tick octave (T7) and D=3 spatial dimensions (T8). The parent theorems thereby confirm that the Lorentz factor and E² = p² + m² emerge without background postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.