spatial_norm_sq
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not include the temporal component of the displacement.
- Does not encode the metric signature or compute the full interval.
- Does not invoke phi, the recognition operator, or any cost functional.
- Does not prove positivity, inequalities, or causal classification.
formal statement (Lean)
188def spatial_norm_sq (v : Displacement) : ℝ :=
proof body
Definition body.
189 v (1 : Fin 4) ^ 2 + v (2 : Fin 4) ^ 2 + v (3 : Fin 4) ^ 2
190
191/-- The temporal component squared. -/