theorem proved term proof

`proper_time_sq_pos_of_timelike`

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

formal statement (Lean)

 259theorem proper_time_sq_pos_of_timelike (v : Displacement) (h : interval v < 0) :
 260    0 < proper_time_sq v := by

Term-mode proof.

 261  rw [proper_time_sq_eq_neg_interval]; linarith
 262
 263/-- **The velocity parameter**: v² = |Δx|²/(Δt)². -/

Lean names referenced from this declaration's body.

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