Displacement
Displacement supplies the type of 4-vectors used throughout the derivation of Lorentzian geometry from the J-cost functional. Workers on spacetime emergence in Recognition Science cite it when building intervals, proper times, and light-cone conditions. The declaration is a direct type abbreviation with no further structure or proof obligations.
claimA spacetime displacement is a map assigning a real number to each of four indices, written $v : [4] → ℝ$.
background
The SpacetimeEmergence module derives the complete 4D Lorentzian structure (signature (−,+,+,+), light cones, proper time) as a theorem of J-cost minimization under the T0–T8 forcing chain. J-cost is the functional J(x) = (x + x⁻¹)/2 − 1 whose second derivative at unity fixes the spatial metric coefficient +1 while the 8-tick recognition operator supplies the opposite sign for the temporal direction. The upstream 'for' structure records the meta-realization axioms needed for self-reference, and the sibling interval definition immediately consumes Displacement to form ds² = ∑ η_{ii} v_i².
proof idea
Direct abbreviation to the function type Fin 4 → ℝ; no tactics or lemmas are applied.
why it matters in Recognition Science
Displacement is the carrier type for every subsequent result in the module, including interval, interval_eq_spatial_minus_temporal, lightlike_iff_speed_c, and proper_time_sq. These feed RealityCertificate in RealityFromDistinction, closing the loop from one distinction to emergent spacetime. The construction realizes the module claim that η = diag(−1,+1,+1,+1) follows from RCL, T5–T8, D = 3, and the eight-tick octave with zero free parameters.
scope and limits
- Does not equip the four components with any metric or inner product.
- Does not restrict values to timelike, spacelike, or lightlike vectors.
- Does not encode units, scaling, or connection to the phi-ladder.
- Does not enforce the J-cost functional or any minimization condition.
formal statement (Lean)
182abbrev Displacement := Fin 4 → ℝ
proof body
Definition body.
183
184/-- The spacetime interval for a displacement vector. -/
used by (15)
-
RealityCertificate -
interval -
interval_eq_spatial_minus_temporal -
lightlike_iff_speed_c -
proper_time_from_velocity -
proper_time_sq -
proper_time_sq_eq_neg_interval -
proper_time_sq_pos_of_timelike -
spacelike_iff_superluminal -
SpacetimeEmergenceCert -
spatial_norm_sq -
temporal_sq -
timelike_iff_subluminal -
timelike_iff_subluminal_velocity -
velocity_sq