pith. machine review for the scientific record. sign in
theorem proved term proof

equal_displacement_is_lightlike

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 239theorem equal_displacement_is_lightlike (a : ℝ) :
 240    interval (fun i : Fin 4 => if i.val = 0 ∨ i.val = 1 then a else 0) = 0 := by

proof body

Term-mode proof.

 241  rw [interval_eq_spatial_minus_temporal]
 242  show (fun i : Fin 4 => if i.val = 0 ∨ i.val = 1 then a else 0) (1 : Fin 4) ^ 2 +
 243       (fun i : Fin 4 => if i.val = 0 ∨ i.val = 1 then a else 0) (2 : Fin 4) ^ 2 +
 244       (fun i : Fin 4 => if i.val = 0 ∨ i.val = 1 then a else 0) (3 : Fin 4) ^ 2 -
 245       (fun i : Fin 4 => if i.val = 0 ∨ i.val = 1 then a else 0) (0 : Fin 4) ^ 2 = 0
 246  norm_num
 247
 248/-! ## §7  Proper Time and the Lorentz Factor -/
 249
 250/-- **Proper time squared**: τ² = −ds² = (Δt)² − |Δx|². -/

depends on (4)

Lean names referenced from this declaration's body.