interval
plain-language theorem explainer
The interval definition supplies the Minkowski quadratic form on 4-vectors in the emergent spacetime of Recognition Science. A physicist deriving Lorentzian geometry from J-cost minimization would cite it when computing proper times or light cones. The definition is a direct sum over the diagonal entries of the forced metric eta = diag(-1,+1,+1,+1).
Claim. For a spacetime displacement 4-vector $v = (v_0, v_1, v_2, v_3)$, the interval is given by $I(v) = -v_0^2 + v_1^2 + v_2^2 + v_3^2$.
background
In the Spacetime Emergence module, spacetime geometry is derived rather than postulated from the J-cost functional and the forcing chain T0-T8. Displacement is the type of 4-vectors representing increments (Delta t, Delta x1, Delta x2, Delta x3). The module states that the complete structure of 4D Lorentzian spacetime, metric signature (-,+,+,+), is forced by J-cost minimization with no background postulate.
proof idea
This is a one-line wrapper that applies the summation over the four components weighted by the diagonal metric coefficients eta_ii.
why it matters
This definition supplies the quadratic form used throughout the unification layer, including in admissible paths and continuum limits. It realizes the central theorem of the module: spacetime is a theorem of cost minimization, with eta forced by RCL to J-uniqueness (T5) to 8-tick octave (T7) plus D=3 (T8). It closes the derivation of the light cone and proper time without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.