spatial_norm_sq
plain-language theorem explainer
The spatial norm squared isolates the Euclidean length of the three spatial components in a 4-vector displacement. Researchers deriving Lorentzian geometry from J-cost minimization cite it when decomposing intervals or establishing light-cone conditions. The definition is a direct sum of squares on the spatial indices of the Fin 4 vector.
Claim. For a displacement 4-vector $v = (v_0, v_1, v_2, v_3)$, the spatial norm squared is $v_1^2 + v_2^2 + v_3^2$.
background
The module derives the full 4D Lorentzian structure (signature (−,+,+,+), light cone, proper time) from the J-cost functional and the T0–T8 forcing chain. Displacement is the 4-vector of spacetime increments (Δt, Δx₁, Δx₂, Δx₃). The spatial part receives the positive metric sign because J''(1) = 1 makes quadratic displacement cost positive definite along each spatial axis, while the temporal direction is singled out by the 8-tick recognition operator that lowers cost.
proof idea
One-line definition that extracts the components indexed 1, 2, 3 of the Fin 4 vector and squares each term before summing.
why it matters
The definition supplies the positive spatial contribution required by interval_eq_spatial_minus_temporal and the light-cone theorems (lightlike_iff_speed_c, spacelike_iff_superluminal). It realizes the D = 3 spatial count forced at T8 and the positive curvature from J''(1) = 1. The same quantity appears inside proper_time_sq and feeds the RealityCertificate that packages the entire emergence chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.