def
definition
to_seconds
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 307.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
304 speed_consistent : meters_per_voxel / seconds_per_tick = 299792458
305
306/-- Convert time (in ticks) to seconds. -/
307@[simp] noncomputable def to_seconds (cal : ExternalCalibration) (t : Time) : ℝ :=
308 t * cal.seconds_per_tick
309
310/-- Convert length (in voxels) to meters. -/
311@[simp] noncomputable def to_meters (cal : ExternalCalibration) (L : Length) : ℝ :=
312 L * cal.meters_per_voxel
313
314/-- Convert velocity (in voxels/tick) to m/s. -/
315@[simp] noncomputable def to_m_per_s (cal : ExternalCalibration) (v : Velocity) : ℝ :=
316 v * (cal.meters_per_voxel / cal.seconds_per_tick)
317
318/-- Convert energy (in coh) to Joules. -/
319@[simp] noncomputable def to_joules (cal : ExternalCalibration) (E : Energy) : ℝ :=
320 E * cal.joules_per_coh
321
322/-- Convert mass (in coh/c²) to kg. -/
323@[simp] noncomputable def to_kg (cal : ExternalCalibration) (m : Mass) : ℝ :=
324 m * cal.joules_per_coh / (299792458 ^ 2)
325
326/-- Convert frequency (in 1/tick) to Hz. -/
327@[simp] noncomputable def to_hertz (cal : ExternalCalibration) (f : Frequency) : ℝ :=
328 f / cal.seconds_per_tick
329
330/-- The speed of light in SI is exactly 299792458 m/s. -/
331theorem c_in_si (cal : ExternalCalibration) :
332 to_m_per_s cal c = 299792458 := by
333 simp [to_m_per_s, c, cal.speed_consistent]
334
335/-! ## Summary Status -/
336
337/-- RS Native Units module status. -/