def definition def or abbrev

`temporal_sq`

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

formal statement (Lean)

 192def temporal_sq (v : Displacement) : ℝ := v (0 : Fin 4) ^ 2

Definition body.

 193
 194/-- **Interval = spatial − temporal** (in signature −,+,+,+). -/

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

RealityCertificate in IndisputableMonolith.Foundation.RealityFromDistinction 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
spacelike_iff_superluminal in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
SpacetimeEmergenceCert 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.

Interval in IndisputableMonolith.Numerics.Interval.Basic decl_use
Interval in IndisputableMonolith.Recognition.Certification decl_use
Displacement in IndisputableMonolith.Unification.SpacetimeEmergence decl_use