def definition def or abbrev

`spatial_norm_sq`

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

formal statement (Lean)

 188def spatial_norm_sq (v : Displacement) : ℝ :=

Definition body.

 189  v (1 : Fin 4) ^ 2 + v (2 : Fin 4) ^ 2 + v (3 : Fin 4) ^ 2
 190
 191/-- The temporal component squared. -/

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

Lean names referenced from this declaration's body.

Displacement in IndisputableMonolith.Unification.SpacetimeEmergence decl_use