abbrev definition def or abbrev

`Displacement`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 182abbrev Displacement := Fin 4 → ℝ

Definition body.

 183
 184/-- The spacetime interval for a displacement vector. -/

From the project-wide theorem graph. These declarations reference this one in their body.

RealityCertificate in IndisputableMonolith.Foundation.RealityFromDistinction decl_use
interval in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
interval_eq_spatial_minus_temporal in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
lightlike_iff_speed_c in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
proper_time_from_velocity in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
proper_time_sq in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
proper_time_sq_eq_neg_interval in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
proper_time_sq_pos_of_timelike in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
spacelike_iff_superluminal in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
SpacetimeEmergenceCert in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
spatial_norm_sq in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
temporal_sq in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
timelike_iff_subluminal in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
timelike_iff_subluminal_velocity in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
velocity_sq in IndisputableMonolith.Unification.SpacetimeEmergence decl_use

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
interval in IndisputableMonolith.Unification.SpacetimeEmergence decl_use