Displacement
plain-language theorem explainer
Spacetime displacement is the type of real 4-vectors used as the domain for the interval functional in the derivation of Lorentzian geometry from J-cost minimization. Researchers reconstructing the metric signature and causal structure from the T0-T8 forcing chain cite this type when building proper-time and light-cone statements. The declaration is a direct type abbreviation with no further content.
Claim. A spacetime displacement is a function $v : Fin(4) → ℝ$.
background
The module SpacetimeEmergence derives the full 4D Lorentzian structure (signature (−,+,+,+), light cone, proper time) from the Recognition Composition Law and the forcing chain T0–T8. J-cost is the unique functional satisfying J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), with J''(1) = 1 fixing the spatial curvature sign and the 8-tick operator fixing the temporal direction. The upstream structure for supplies the meta-realization axioms that underwrite the self-reference step preceding the emergence of the carrier type. The sibling interval definition immediately applies this type: interval(v) := ∑{i:Fin 4} η{ii} v_i².
proof idea
Direct abbreviation of the 4-dimensional real vector space; no lemmas or tactics are invoked.
why it matters
Displacement supplies the domain for interval and all its downstream theorems (interval_eq_spatial_minus_temporal, lightlike_iff_speed_c, proper_time_sq, proper_time_from_velocity). These realize the central claim that η = diag(−1,+1,+1,+1) is forced by J-cost together with T7 (octave) and T8 (D=3). The type also appears in RealityCertificate, packaging the entire distinction-to-spacetime chain. It closes the step from abstract cost functional to concrete 4-vector geometry with zero free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.