def definition def or abbrev

`proper_time_sq`

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

formal statement (Lean)

 251def proper_time_sq (v : Displacement) : ℝ := temporal_sq v - spatial_norm_sq v

Definition body.

 252
 253/-- Proper time squared = −interval. -/

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

proper_time_from_velocity 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
timelike_iff_subluminal_velocity in IndisputableMonolith.Unification.SpacetimeEmergence decl_use

Lean names referenced from this declaration's body.

Displacement in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
interval in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
spatial_norm_sq in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
temporal_sq in IndisputableMonolith.Unification.SpacetimeEmergence decl_use